Theorem orim12i 760

Description: Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)

Hypotheses

Ref	Expression
orim12i.1	|- ( ph -> ps )
orim12i.2	|- ( ch -> th )

Assertion

Ref	Expression
orim12i	|- ( ( ph \/ ch ) -> ( ps \/ th ) )

Proof of Theorem orim12i

Step	Hyp	Ref	Expression
1		orim12i.1	. . 3 |- ( ph -> ps )
2	1	orcd 734	. 2 |- ( ph -> ( ps \/ th ) )
3		orim12i.2	. . 3 |- ( ch -> th )
4	3	olcd 735	. 2 |- ( ch -> ( ps \/ th ) )
5	2, 4	jaoi 717	1 |- ( ( ph \/ ch ) -> ( ps \/ th ) )

Syntax hints:   -> wi 4   \/ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  761  orim2i  762  dcim  842  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  pm5.54dc  919  prlem2  976  xordc1  1404  19.43  1642  eueq3dc  2938  inssun  3403  abvor0dc  3474  ifmdc  3601  undifexmid  4226  pwssunim  4319  ordtriexmid  4557  ontriexmidim  4558  ordtri2orexmid  4559  ontr2exmid  4561  onsucsssucexmid  4563  onsucelsucexmid  4566  ordsoexmid  4598  0elsucexmid  4601  ordpwsucexmid  4606  ordtri2or2exmid  4607  ontri2orexmidim  4608  funcnvuni  5327  oprabidlem  5953  2oconcl  6497  inffiexmid  6967  unfiexmid  6979  ctssexmid  7216  exmidonfinlem  7260  sup3exmid  8984  zeo  9431  ef0lem  11825