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  1639  eueq3dc  2935  inssun  3400  abvor0dc  3471  ifmdc  3598  undifexmid  4223  pwssunim  4316  ordtriexmid  4554  ontriexmidim  4555  ordtri2orexmid  4556  ontr2exmid  4558  onsucsssucexmid  4560  onsucelsucexmid  4563  ordsoexmid  4595  0elsucexmid  4598  ordpwsucexmid  4603  ordtri2or2exmid  4604  ontri2orexmidim  4605  funcnvuni  5324  oprabidlem  5950  2oconcl  6494  inffiexmid  6964  unfiexmid  6976  ctssexmid  7211  exmidonfinlem  7255  sup3exmid  8978  zeo  9425  ef0lem  11806