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  2980  inssun  3447  abvor0dc  3518  ifmdc  3648  undifexmid  4283  pwssunim  4381  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsoexmid  4660  0elsucexmid  4663  ordpwsucexmid  4668  ordtri2or2exmid  4669  ontri2orexmidim  4670  funcnvuni  5399  oprabidlem  6049  2oconcl  6607  inffiexmid  7098  unfiexmid  7110  ctssexmid  7349  exmidonfinlem  7404  sup3exmid  9137  zeo  9585  ef0lem  12223