Metamath Proof Explorer


Theorem bj-dfbi4

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

Ref Expression
Assertion bj-dfbi4 φ ψ φ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 dfbi3 φ ψ φ ψ ¬ φ ¬ ψ
2 pm4.56 ¬ φ ¬ ψ ¬ φ ψ
3 2 orbi2i φ ψ ¬ φ ¬ ψ φ ψ ¬ φ ψ
4 1 3 bitri φ ψ φ ψ ¬ φ ψ