Metamath Proof Explorer

Theorem dfbi2

Description: A theorem similar to the standard definition of the biconditional. Definition of Margaris p. 49. (Contributed by NM, 24-Jan-1993)

Ref Expression
Assertion dfbi2 φ ψ φ ψ ψ φ


Step Hyp Ref Expression
1 dfbi1 φ ψ ¬ φ ψ ¬ ψ φ
2 df-an φ ψ ψ φ ¬ φ ψ ¬ ψ φ
3 1 2 bitr4i φ ψ φ ψ ψ φ