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

Metamath Proof Explorer

Theorem pm5.53

Description: Theorem *5.53 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)

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

Proof

Step Hyp Ref Expression
1 jaob 
 |-  ( ( ( ( ph \/ ps ) \/ ch ) -> th ) <-> ( ( ( ph \/ ps ) -> th ) /\ ( ch -> th ) ) )
2 jaob 
 |-  ( ( ( ph \/ ps ) -> th ) <-> ( ( ph -> th ) /\ ( ps -> th ) ) )
3 1 2 bianbi 
 |-  ( ( ( ( ph \/ ps ) \/ ch ) -> th ) <-> ( ( ( ph -> th ) /\ ( ps -> th ) ) /\ ( ch -> th ) ) )