Theorem orim12i 755

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

Syntax hints:   → wi 4   ∨ wo 704

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 705

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  756  orim2i  757  dcim  837  pm5.12dc  906  pm5.14dc  907  pm5.55dc  909  pm5.54dc  914  prlem2  970  xordc1  1389  19.43  1622  eueq3dc  2905  inssun  3368  abvor0dc  3439  ifmdc  3566  undifexmid  4180  pwssunim  4270  ordtriexmid  4506  ontriexmidim  4507  ordtri2orexmid  4508  ontr2exmid  4510  onsucsssucexmid  4512  onsucelsucexmid  4515  ordsoexmid  4547  0elsucexmid  4550  ordpwsucexmid  4555  ordtri2or2exmid  4556  ontri2orexmidim  4557  funcnvuni  5269  oprabidlem  5888  2oconcl  6422  inffiexmid  6888  unfiexmid  6899  ctssexmid  7130  exmidonfinlem  7174  sup3exmid  8877  zeo  9321  ef0lem  11627