Theorem orim12i 767

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

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  768  orim2i  769  dcim  849  pm5.12dc  918  pm5.14dc  919  pm5.55dc  921  pm5.54dc  926  prlem2  983  ifpdc  988  ifpor  996  xordc1  1438  19.43  1677  eueq3dc  2981  inssun  3449  abvor0dc  3520  ifmdc  3652  undifexmid  4289  pwssunim  4387  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  ordsoexmid  4666  0elsucexmid  4669  ordpwsucexmid  4674  ordtri2or2exmid  4675  ontri2orexmidim  4676  funcnvuni  5406  oprabidlem  6059  2oconcl  6650  inffiexmid  7141  unfiexmid  7153  ctssexmid  7392  exmidonfinlem  7447  sup3exmid  9180  zeo  9628  ef0lem  12282