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  2934  inssun  3399  abvor0dc  3470  ifmdc  3597  undifexmid  4222  pwssunim  4315  ordtriexmid  4553  ontriexmidim  4554  ordtri2orexmid  4555  ontr2exmid  4557  onsucsssucexmid  4559  onsucelsucexmid  4562  ordsoexmid  4594  0elsucexmid  4597  ordpwsucexmid  4602  ordtri2or2exmid  4603  ontri2orexmidim  4604  funcnvuni  5323  oprabidlem  5949  2oconcl  6492  inffiexmid  6962  unfiexmid  6974  ctssexmid  7209  exmidonfinlem  7253  sup3exmid  8976  zeo  9422  ef0lem  11803