This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ph /\ ps ) -> ph )
2 1 biantru 
 |-  ( ( ph -> ( ph /\ ps ) ) <-> ( ( ph -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> ph ) ) )
3 anclb 
 |-  ( ( ph -> ps ) <-> ( ph -> ( ph /\ ps ) ) )
4 dfbi2 
 |-  ( ( ph <-> ( ph /\ ps ) ) <-> ( ( ph -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> ph ) ) )
5 2 3 4 3bitr4i 
 |-  ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )