Theorem orim12i 676

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

Syntax hints:   → wi 4   ∨ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orim1i  677  orim2i  678  dcim  784  pm5.12dc  816  pm5.14dc  817  pm5.55dc  819  pm5.54dc  827  prlem2  881  xordc1  1284  19.43  1519  eueq3dc  2715  inssun  3177  abvor0dc  3242  pwssunim  4021  ordtriexmid  4247  ordtri2orexmid  4248  ontr2exmid  4250  onsucsssucexmid  4252  onsucelsucexmid  4255  ordsoexmid  4286  0elsucexmid  4289  ordpwsucexmid  4294  ordtri2or2exmid  4296  funcnvuni  4968  oprabidlem  5536  2oconcl  6022  zeo  8343