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

Metamath Proof Explorer

Theorem pm5.32

Description: Distribution of implication over biconditional. Theorem *5.32 of WhiteheadRussell p. 125. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion pm5.32 
|- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 notbi 
 |-  ( ( ps <-> ch ) <-> ( -. ps <-> -. ch ) )
2 1 imbi2i 
 |-  ( ( ph -> ( ps <-> ch ) ) <-> ( ph -> ( -. ps <-> -. ch ) ) )
3 pm5.74 
 |-  ( ( ph -> ( -. ps <-> -. ch ) ) <-> ( ( ph -> -. ps ) <-> ( ph -> -. ch ) ) )
4 notbi 
 |-  ( ( ( ph -> -. ps ) <-> ( ph -> -. ch ) ) <-> ( -. ( ph -> -. ps ) <-> -. ( ph -> -. ch ) ) )
5 2 3 4 3bitri 
 |-  ( ( ph -> ( ps <-> ch ) ) <-> ( -. ( ph -> -. ps ) <-> -. ( ph -> -. ch ) ) )
6 df-an 
 |-  ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) )
7 df-an 
 |-  ( ( ph /\ ch ) <-> -. ( ph -> -. ch ) )
8 6 7 bibi12i 
 |-  ( ( ( ph /\ ps ) <-> ( ph /\ ch ) ) <-> ( -. ( ph -> -. ps ) <-> -. ( ph -> -. ch ) ) )
9 5 8 bitr4i 
 |-  ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )