Theorem: FOL.NV.T_19_2 (FOL/NV/Margaris/Fol.lean)

State before:
P : Formula
u v : VarName
⊢ IsProof ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P)))
Tactic:
apply IsDeduct.mp_ ((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P)))
State after:
case a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
      ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P))))

case a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P)))

State before:
case a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
      ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P))))
Tactic:
apply IsDeduct.mp_ ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P)))
State after:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P)))))

case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P)))

State before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        ((forall_ u (forall_ v P)).iff_ (forall_ v (forall_ u P)))))
Tactic:
simp only [def_iff_]
State after:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).and_
          ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))))))

State before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).and_
          ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))))))
Tactic:
simp only [def_and_]
State after:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
            ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).not_).not_))

State before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
            ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).not_).not_))
Tactic:
SC
State after:
no goals

State before:
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P)))
Tactic:
apply T_17_10
State after:
no goals

State before:
case a
P : Formula
u v : VarName
⊢ IsDeduct ∅ ((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P)))
Tactic:
apply T_17_10
State after:
no goals