Theorem orim12i 764

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  765  orim2i  766  dcim  846  pm5.12dc  915  pm5.14dc  916  pm5.55dc  918  pm5.54dc  923  prlem2  980  ifpdc  985  ifpor  993  xordc1  1435  19.43  1674  eueq3dc  2977  inssun  3444  abvor0dc  3515  ifmdc  3645  undifexmid  4276  pwssunim  4372  ordtriexmid  4610  ontriexmidim  4611  ordtri2orexmid  4612  ontr2exmid  4614  onsucsssucexmid  4616  onsucelsucexmid  4619  ordsoexmid  4651  0elsucexmid  4654  ordpwsucexmid  4659  ordtri2or2exmid  4660  ontri2orexmidim  4661  funcnvuni  5386  oprabidlem  6025  2oconcl  6575  inffiexmid  7056  unfiexmid  7068  ctssexmid  7305  exmidonfinlem  7359  sup3exmid  9092  zeo  9540  ef0lem  12157