Metamath Proof Explorer

Theorem 3jao

Description: Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994)

Ref Expression
Assertion 3jao 
|- ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )

Proof

Step Hyp Ref Expression
1 jao 
 |-  ( ( ph -> ps ) -> ( ( ch -> ps ) -> ( ( ph \/ ch ) -> ps ) ) )
2 df-3or 
 |-  ( ( ph \/ ch \/ th ) <-> ( ( ph \/ ch ) \/ th ) )
3 jao 
 |-  ( ( ( ph \/ ch ) -> ps ) -> ( ( th -> ps ) -> ( ( ( ph \/ ch ) \/ th ) -> ps ) ) )
4 2 3 syl7bi 
 |-  ( ( ( ph \/ ch ) -> ps ) -> ( ( th -> ps ) -> ( ( ph \/ ch \/ th ) -> ps ) ) )
5 1 4 syl6 
 |-  ( ( ph -> ps ) -> ( ( ch -> ps ) -> ( ( th -> ps ) -> ( ( ph \/ ch \/ th ) -> ps ) ) ) )
6 5 3imp 
 |-  ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )