Theorem orim12i 771

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 745	. 2 |- ( ph -> ( ps \/ th ) )
3		orim12i.2	. . 3 |- ( ch -> th )
4	3	olcd 746	. 2 |- ( ch -> ( ps \/ th ) )
5	2, 4	jaoi 728	1 |- ( ( ph \/ ch ) -> ( ps \/ th ) )

Syntax hints:   -> wi 4   \/ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  772  orim2i  773  dcim  853  pm5.12dc  922  pm5.14dc  923  pm5.55dc  925  pm5.54dc  930  prlem2  987  ifpdc  992  ifpor  1000  xordc1  1442  19.43  1681  eueq3dc  3000  inssun  3471  abvor0dc  3545  ifmdc  3683  undifexmid  4328  pwssunim  4427  ordtriexmid  4666  ontriexmidim  4667  ordtri2orexmid  4668  ontr2exmid  4670  onsucsssucexmid  4672  onsucelsucexmid  4675  ordsoexmid  4707  0elsucexmid  4710  ordpwsucexmid  4715  ordtri2or2exmid  4716  ontri2orexmidim  4717  funcnvuni  5448  oprabidlem  6110  2oconcl  6706  inffiexmid  7207  unfiexmid  7219  ctssexmid  7484  exmidonfinlem  7539  sup3exmid  9281  zeo  9734  ef0lem  12410