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

State before:
Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ Q
⊢ ∀ (Γ : Set Formula), IsDeduct (Γ ∪ Δ) Q
Tactic:
simp only [Set.union_comm]
State after:
Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ Q
⊢ ∀ (Γ : Set Formula), IsDeduct (Δ ∪ Γ) Q

State before:
Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ Q
⊢ ∀ (Γ : Set Formula), IsDeduct (Δ ∪ Γ) Q
Tactic:
exact T_14_10 Q Δ h1
State after:
no goals