Theorem jaob 758

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

Assertion

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

Proof of Theorem jaob

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

Syntax hints:   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360

This theorem is referenced by:  pm4.77  762  pm5.53  771  pm4.83  895  unss  3437  ralunb  3444  intun  3958  intpr  3959