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

Metamath Proof Explorer

Theorem 3jaob

Description: Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011) (Proof shortened by Hongxiu Chen, 29-Jun-2025)

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

Proof

Step Hyp Ref Expression
1 pm5.53 
 |-  ( ( ( ( ph \/ ch ) \/ th ) -> ps ) <-> ( ( ( ph -> ps ) /\ ( ch -> ps ) ) /\ ( th -> ps ) ) )
2 df-3or 
 |-  ( ( ph \/ ch \/ th ) <-> ( ( ph \/ ch ) \/ th ) )
3 2 imbi1i 
 |-  ( ( ( ph \/ ch \/ th ) -> ps ) <-> ( ( ( ph \/ ch ) \/ th ) -> ps ) )
4 df-3an 
 |-  ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) <-> ( ( ( ph -> ps ) /\ ( ch -> ps ) ) /\ ( th -> ps ) ) )
5 1 3 4 3bitr4i 
 |-  ( ( ( ph \/ ch \/ th ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) )