Theorem orim12i 749

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	⊢ (𝜑 → 𝜓)
orim12i.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
orim12i	⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))

Proof of Theorem orim12i

Step	Hyp	Ref	Expression
1		orim12i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	orcd 723	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
3		orim12i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	olcd 724	. 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃))
5	2, 4	jaoi 706	1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  750  orim2i  751  dcim  827  pm5.12dc  896  pm5.14dc  897  pm5.55dc  899  pm5.54dc  904  prlem2  959  xordc1  1375  19.43  1608  eueq3dc  2886  inssun  3348  abvor0dc  3418  ifmdc  3543  undifexmid  4156  pwssunim  4246  ordtriexmid  4482  ontriexmidim  4483  ordtri2orexmid  4484  ontr2exmid  4486  onsucsssucexmid  4488  onsucelsucexmid  4491  ordsoexmid  4523  0elsucexmid  4526  ordpwsucexmid  4531  ordtri2or2exmid  4532  ontri2orexmidim  4533  funcnvuni  5241  oprabidlem  5854  2oconcl  6388  inffiexmid  6853  unfiexmid  6864  ctssexmid  7095  exmidonfinlem  7130  sup3exmid  8833  zeo  9274  ef0lem  11568