Metamath Proof Explorer


Theorem frege54cor0a

Description: Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege54cor0a ψ φ if- ψ φ ¬ φ

Proof

Step Hyp Ref Expression
1 ax-frege28 φ ψ ¬ ψ ¬ φ
2 1 anim2i ψ φ φ ψ ψ φ ¬ ψ ¬ φ
3 con4 ¬ ψ ¬ φ φ ψ
4 3 anim2i ψ φ ¬ ψ ¬ φ ψ φ φ ψ
5 2 4 impbii ψ φ φ ψ ψ φ ¬ ψ ¬ φ
6 dfbi2 ψ φ ψ φ φ ψ
7 dfifp2 if- ψ φ ¬ φ ψ φ ¬ ψ ¬ φ
8 5 6 7 3bitr4i ψ φ if- ψ φ ¬ φ