Metamath Proof Explorer


Theorem pm4.71

Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of WhiteheadRussell p. 120. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 2-Dec-2012)

Ref Expression
Assertion pm4.71 φ ψ φ φ ψ

Proof

Step Hyp Ref Expression
1 simpl φ ψ φ
2 1 biantru φ φ ψ φ φ ψ φ ψ φ
3 anclb φ ψ φ φ ψ
4 dfbi2 φ φ ψ φ φ ψ φ ψ φ
5 2 3 4 3bitr4i φ ψ φ φ ψ