Theorem orim12i 759

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

Syntax hints:   -> wi 4   \/ wo 708

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  760  orim2i  761  dcim  841  pm5.12dc  910  pm5.14dc  911  pm5.55dc  913  pm5.54dc  918  prlem2  974  xordc1  1393  19.43  1628  eueq3dc  2912  inssun  3376  abvor0dc  3447  ifmdc  3575  undifexmid  4194  pwssunim  4285  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  onsucelsucexmid  4530  ordsoexmid  4562  0elsucexmid  4565  ordpwsucexmid  4570  ordtri2or2exmid  4571  ontri2orexmidim  4572  funcnvuni  5286  oprabidlem  5906  2oconcl  6440  inffiexmid  6906  unfiexmid  6917  ctssexmid  7148  exmidonfinlem  7192  sup3exmid  8914  zeo  9358  ef0lem  11668