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 ) )

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used 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  4332  pwssunim  4431  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  ordsoexmid  4711  0elsucexmid  4714  ordpwsucexmid  4719  ordtri2or2exmid  4720  ontri2orexmidim  4721  funcnvuni  5453  oprabidlem  6119  2oconcl  6716  inffiexmid  7218  unfiexmid  7230  ctssexmid  7497  exmidonfinlem  7552  sup3exmid  9296  zeo  9763  ef0lem  12453  wexmiddiffilem  17260  wexmiddifxylem  17262