Metamath Proof Explorer


Theorem bj-dfbi5

Description: Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019)

Ref Expression
Assertion bj-dfbi5 φ ψ φ ψ φ ψ

Proof

Step Hyp Ref Expression
1 orcom φ ψ ¬ φ ψ ¬ φ ψ φ ψ
2 bj-dfbi4 φ ψ φ ψ ¬ φ ψ
3 imor φ ψ φ ψ ¬ φ ψ φ ψ
4 1 2 3 3bitr4i φ ψ φ ψ φ ψ