Theorem orim12i 749

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

Syntax hints:   -> wi 4   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  750  orim2i  751  dcim  831  pm5.12dc  900  pm5.14dc  901  pm5.55dc  903  pm5.54dc  908  prlem2  964  xordc1  1383  19.43  1616  eueq3dc  2900  inssun  3362  abvor0dc  3432  ifmdc  3558  undifexmid  4172  pwssunim  4262  ordtriexmid  4498  ontriexmidim  4499  ordtri2orexmid  4500  ontr2exmid  4502  onsucsssucexmid  4504  onsucelsucexmid  4507  ordsoexmid  4539  0elsucexmid  4542  ordpwsucexmid  4547  ordtri2or2exmid  4548  ontri2orexmidim  4549  funcnvuni  5257  oprabidlem  5873  2oconcl  6407  inffiexmid  6872  unfiexmid  6883  ctssexmid  7114  exmidonfinlem  7149  sup3exmid  8852  zeo  9296  ef0lem  11601