Theorem orim12i 708

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

Syntax hints:   → wi 4   ∨ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orim1i  709  orim2i  710  dcim  817  pm5.12dc  849  pm5.14dc  850  pm5.55dc  852  pm5.54dc  860  prlem2  915  xordc1  1324  19.43  1559  eueq3dc  2766  inssun  3204  abvor0dc  3269  pwssunim  4039  ordtriexmid  4265  ordtri2orexmid  4266  ontr2exmid  4268  onsucsssucexmid  4270  onsucelsucexmid  4273  ordsoexmid  4305  0elsucexmid  4308  ordpwsucexmid  4313  ordtri2or2exmid  4314  funcnvuni  4988  oprabidlem  5556  2oconcl  6045  zeo  8452