Metamath Proof Explorer

Theorem pm3.48

Description: Theorem *3.48 of WhiteheadRussell p. 114. (Contributed by NM, 28-Jan-1997)

Ref Expression
Assertion pm3.48 
|- ( ( ( ph -> ps ) /\ ( ch -> th ) ) -> ( ( ph \/ ch ) -> ( ps \/ th ) ) )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( ps -> ( ps \/ th ) )
2 1 imim2i 
 |-  ( ( ph -> ps ) -> ( ph -> ( ps \/ th ) ) )
3 olc 
 |-  ( th -> ( ps \/ th ) )
4 3 imim2i 
 |-  ( ( ch -> th ) -> ( ch -> ( ps \/ th ) ) )
5 2 4 jaao 
 |-  ( ( ( ph -> ps ) /\ ( ch -> th ) ) -> ( ( ph \/ ch ) -> ( ps \/ th ) ) )