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

State before:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsProof P
⊢ IsProof Q
Tactic:
simp only [IsProof] at h2
State after:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsProof Q

State before:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsProof Q
Tactic:
simp only [IsProof]
State after:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsDeduct ∅ Q

State before:
Q : Formula
Γ : Set Formula
h1 : IsDeduct Γ Q
h2 : ∀ P ∈ Γ, IsDeduct ∅ P
⊢ IsDeduct ∅ Q
Tactic:
exact T_14_16 Q ∅ Γ h1 h2
State after:
no goals