Theorem: FOL.NV.T_14_16 (FOL/NV/Margaris/Prop.lean)

State before:
F : Formula
Δ Γ : Set Formula
h1 : IsDeduct Γ F
h2 : ∀ H ∈ Γ, IsDeduct Δ H
⊢ IsDeduct Δ F
Tactic:
induction h1
State after:
case axiom_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ phi✝

case assume_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ : Formula
a✝ : phi✝ ∈ Γ
⊢ IsDeduct Δ phi✝

case mp_
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Γ (phi✝.imp_ psi✝)
a✝ : IsDeduct Γ phi✝
a_ih✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a_ih✝ : IsDeduct Δ phi✝
⊢ IsDeduct Δ psi✝

State before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
Tactic:
case axiom_ h1_phi h1_1 =>
  apply IsDeduct.axiom_
  exact h1_1
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : h1_phi ∈ Γ
⊢ IsDeduct Δ h1_phi
Tactic:
case assume_ h1_phi h1_1 => exact h2 h1_phi h1_1
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Γ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Γ h1_phi
h1_ih_1 : IsDeduct Δ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct Δ h1_phi
⊢ IsDeduct Δ h1_psi
Tactic:
case mp_ h1_phi h1_psi _ _ h1_ih_1 h1_ih_2 =>
  exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi

State before:
case a
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Tactic:
exact h1_1
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi : Formula
h1_1 : h1_phi ∈ Γ
⊢ IsDeduct Δ h1_phi
Tactic:
exact h2 h1_phi h1_1
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Γ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Γ h1_phi
h1_ih_1 : IsDeduct Δ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct Δ h1_phi
⊢ IsDeduct Δ h1_psi
Tactic:
exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
State after:
no goals