Theorem orim12i 766

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

Syntax hints:   -> wi 4   \/ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  767  orim2i  768  dcim  848  pm5.12dc  917  pm5.14dc  918  pm5.55dc  920  pm5.54dc  925  prlem2  982  ifpdc  987  ifpor  995  xordc1  1437  19.43  1676  eueq3dc  2979  inssun  3446  abvor0dc  3517  ifmdc  3649  undifexmid  4285  pwssunim  4383  ordtriexmid  4621  ontriexmidim  4622  ordtri2orexmid  4623  ontr2exmid  4625  onsucsssucexmid  4627  onsucelsucexmid  4630  ordsoexmid  4662  0elsucexmid  4665  ordpwsucexmid  4670  ordtri2or2exmid  4671  ontri2orexmidim  4672  funcnvuni  5401  oprabidlem  6054  2oconcl  6612  inffiexmid  7103  unfiexmid  7115  ctssexmid  7354  exmidonfinlem  7409  sup3exmid  9142  zeo  9590  ef0lem  12244