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  4330  pwssunim  4429  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  ordsoexmid  4709  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  ontri2orexmidim  4719  funcnvuni  5450  oprabidlem  6116  2oconcl  6712  inffiexmid  7213  unfiexmid  7225  ctssexmid  7490  exmidonfinlem  7545  sup3exmid  9288  zeo  9753  ef0lem  12429  wexmiddiffilem  17055  wexmiddifxylem  17057