Theorem orim12i 748

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

Syntax hints:   → wi 4   ∨ wo 697

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 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  749  orim2i  750  dcim  826  pm5.12dc  895  pm5.14dc  896  pm5.55dc  898  pm5.54dc  903  prlem2  958  xordc1  1371  19.43  1607  eueq3dc  2853  inssun  3311  abvor0dc  3381  ifmdc  3504  undifexmid  4112  pwssunim  4201  ordtriexmid  4432  ordtri2orexmid  4433  ontr2exmid  4435  onsucsssucexmid  4437  onsucelsucexmid  4440  ordsoexmid  4472  0elsucexmid  4475  ordpwsucexmid  4480  ordtri2or2exmid  4481  funcnvuni  5187  oprabidlem  5795  2oconcl  6329  inffiexmid  6793  unfiexmid  6799  ctssexmid  7017  exmidonfinlem  7042  sup3exmid  8708  zeo  9149  ef0lem  11355