Metamath Proof Explorer

Theorem pm4.71r

Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of WhiteheadRussell p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999)

Ref Expression
Assertion pm4.71r φ ψ φ ψ φ


Step Hyp Ref Expression
1 pm4.71 φ ψ φ φ ψ
2 ancom φ ψ ψ φ
3 2 bibi2i φ φ ψ φ ψ φ
4 1 3 bitri φ ψ φ ψ φ