Metamath Proof Explorer

Theorem 3jaob

Description: Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011)

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

Proof

Step Hyp Ref Expression
1 3mix1 
 |-  ( ph -> ( ph \/ ch \/ th ) )
2 1 imim1i 
 |-  ( ( ( ph \/ ch \/ th ) -> ps ) -> ( ph -> ps ) )
3 3mix2 
 |-  ( ch -> ( ph \/ ch \/ th ) )
4 3 imim1i 
 |-  ( ( ( ph \/ ch \/ th ) -> ps ) -> ( ch -> ps ) )
5 3mix3 
 |-  ( th -> ( ph \/ ch \/ th ) )
6 5 imim1i 
 |-  ( ( ( ph \/ ch \/ th ) -> ps ) -> ( th -> ps ) )
7 2 4 6 3jca 
 |-  ( ( ( ph \/ ch \/ th ) -> ps ) -> ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) )
8 3jao 
 |-  ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )
9 7 8 impbii 
 |-  ( ( ( ph \/ ch \/ th ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) )