Theorem jaob

Description: Disjunction of antecedents. Compare Theorem *4.77 of WhiteheadRussell p. 121. (Contributed by NM, 30-May-1994) (Proof shortened by Wolf Lammen, 9-Dec-2012)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.67-2	|- ( ( ( ph \/ ch ) -> ps ) -> ( ph -> ps ) )
2		olc	|- ( ch -> ( ph \/ ch ) )
3	2	imim1i	|- ( ( ( ph \/ ch ) -> ps ) -> ( ch -> ps ) )
4	1 3	jca	|- ( ( ( ph \/ ch ) -> ps ) -> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
5		pm3.44	|- ( ( ( ph -> ps ) /\ ( ch -> ps ) ) -> ( ( ph \/ ch ) -> ps ) )
6	4 5	impbii	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )