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

State before:
P : Formula
h1 : IsProof P
⊢ ∀ (Δ : Set Formula), IsDeduct Δ P
Tactic:
intro Δ
State after:
P : Formula
h1 : IsProof P
Δ : Set Formula
⊢ IsDeduct Δ P

State before:
P : Formula
h1 : IsProof P
Δ : Set Formula
⊢ IsDeduct Δ P
Tactic:
obtain s1 := T_14_10 P ∅ h1 Δ
State after:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct (∅ ∪ Δ) P
⊢ IsDeduct Δ P

State before:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct (∅ ∪ Δ) P
⊢ IsDeduct Δ P
Tactic:
simp at s1
State after:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct Δ P
⊢ IsDeduct Δ P

State before:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Tactic:
exact s1
State after:
no goals