Theorem orim12i 714

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

Syntax hints:   -> wi 4   \/ wo 667

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  715  orim2i  716  dcim  825  pm5.12dc  857  pm5.14dc  858  pm5.55dc  860  pm5.54dc  868  prlem2  923  xordc1  1336  19.43  1571  eueq3dc  2803  inssun  3255  abvor0dc  3325  ifmdc  3448  undifexmid  4049  pwssunim  4135  ordtriexmid  4366  ordtri2orexmid  4367  ontr2exmid  4369  onsucsssucexmid  4371  onsucelsucexmid  4374  ordsoexmid  4406  0elsucexmid  4409  ordpwsucexmid  4414  ordtri2or2exmid  4415  funcnvuni  5117  oprabidlem  5718  2oconcl  6241  inffiexmid  6702  unfiexmid  6708  djur  6837  djuun  6840  sup3exmid  8515  zeo  8950  ef0lem  11099