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  2926  inssun  3390  abvor0dc  3461  ifmdc  3589  undifexmid  4211  pwssunim  4302  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  ontr2exmid  4542  onsucsssucexmid  4544  onsucelsucexmid  4547  ordsoexmid  4579  0elsucexmid  4582  ordpwsucexmid  4587  ordtri2or2exmid  4588  ontri2orexmidim  4589  funcnvuni  5304  oprabidlem  5926  2oconcl  6463  inffiexmid  6933  unfiexmid  6945  ctssexmid  7177  exmidonfinlem  7221  sup3exmid  8943  zeo  9387  ef0lem  11699