Metamath Proof Explorer

Theorem pm4.79

Description: Theorem *4.79 of WhiteheadRussell p. 121. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 27-Jun-2013)

Ref Expression
Assertion pm4.79 
|- ( ( ( ps -> ph ) \/ ( ch -> ph ) ) <-> ( ( ps /\ ch ) -> ph ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( ps -> ph ) -> ( ps -> ph ) )
2 id 
 |-  ( ( ch -> ph ) -> ( ch -> ph ) )
3 1 2 jaoa 
 |-  ( ( ( ps -> ph ) \/ ( ch -> ph ) ) -> ( ( ps /\ ch ) -> ph ) )
4 simplim 
 |-  ( -. ( ps -> ph ) -> ps )
5 pm3.3 
 |-  ( ( ( ps /\ ch ) -> ph ) -> ( ps -> ( ch -> ph ) ) )
6 4 5 syl5 
 |-  ( ( ( ps /\ ch ) -> ph ) -> ( -. ( ps -> ph ) -> ( ch -> ph ) ) )
7 6 orrd 
 |-  ( ( ( ps /\ ch ) -> ph ) -> ( ( ps -> ph ) \/ ( ch -> ph ) ) )
8 3 7 impbii 
 |-  ( ( ( ps -> ph ) \/ ( ch -> ph ) ) <-> ( ( ps /\ ch ) -> ph ) )