Theorem orim12i 759

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

Syntax hints:   -> wi 4   \/ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  760  orim2i  761  dcim  841  pm5.12dc  910  pm5.14dc  911  pm5.55dc  913  pm5.54dc  918  prlem2  974  xordc1  1393  19.43  1628  eueq3dc  2911  inssun  3375  abvor0dc  3446  ifmdc  3574  undifexmid  4193  pwssunim  4284  ordtriexmid  4520  ontriexmidim  4521  ordtri2orexmid  4522  ontr2exmid  4524  onsucsssucexmid  4526  onsucelsucexmid  4529  ordsoexmid  4561  0elsucexmid  4564  ordpwsucexmid  4569  ordtri2or2exmid  4570  ontri2orexmidim  4571  funcnvuni  5285  oprabidlem  5905  2oconcl  6439  inffiexmid  6905  unfiexmid  6916  ctssexmid  7147  exmidonfinlem  7191  sup3exmid  8913  zeo  9357  ef0lem  11667