Theorem orim12i 712

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 688	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
3		orim12i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	olcd 689	. 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃))
5	2, 4	jaoi 672	1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ wo 665

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  713  orim2i  714  dcim  823  pm5.12dc  855  pm5.14dc  856  pm5.55dc  858  pm5.54dc  866  prlem2  921  xordc1  1330  19.43  1565  eueq3dc  2790  inssun  3240  abvor0dc  3310  ifmdc  3432  undifexmid  4034  pwssunim  4120  ordtriexmid  4351  ordtri2orexmid  4352  ontr2exmid  4354  onsucsssucexmid  4356  onsucelsucexmid  4359  ordsoexmid  4391  0elsucexmid  4394  ordpwsucexmid  4399  ordtri2or2exmid  4400  funcnvuni  5096  oprabidlem  5694  2oconcl  6217  inffiexmid  6676  unfiexmid  6682  djur  6811  djuun  6814  zeo  8912  ef0lem  11011