Theorem orim12i 754

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

Syntax hints:   -> wi 4   \/ wo 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  755  orim2i  756  dcim  836  pm5.12dc  905  pm5.14dc  906  pm5.55dc  908  pm5.54dc  913  prlem2  969  xordc1  1388  19.43  1621  eueq3dc  2904  inssun  3367  abvor0dc  3437  ifmdc  3563  undifexmid  4177  pwssunim  4267  ordtriexmid  4503  ontriexmidim  4504  ordtri2orexmid  4505  ontr2exmid  4507  onsucsssucexmid  4509  onsucelsucexmid  4512  ordsoexmid  4544  0elsucexmid  4547  ordpwsucexmid  4552  ordtri2or2exmid  4553  ontri2orexmidim  4554  funcnvuni  5265  oprabidlem  5882  2oconcl  6416  inffiexmid  6881  unfiexmid  6892  ctssexmid  7123  exmidonfinlem  7159  sup3exmid  8862  zeo  9306  ef0lem  11612