Theorem orim12i 760

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

Syntax hints:   → wi 4   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  761  orim2i  762  dcim  842  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  pm5.54dc  919  prlem2  976  xordc1  1404  19.43  1642  eueq3dc  2938  inssun  3404  abvor0dc  3475  ifmdc  3602  undifexmid  4227  pwssunim  4320  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  ordsoexmid  4599  0elsucexmid  4602  ordpwsucexmid  4607  ordtri2or2exmid  4608  ontri2orexmidim  4609  funcnvuni  5328  oprabidlem  5956  2oconcl  6506  inffiexmid  6976  unfiexmid  6988  ctssexmid  7225  exmidonfinlem  7272  sup3exmid  9001  zeo  9448  ef0lem  11842