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 ) ) )