Theorem orim12i 749

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

Syntax hints:   → wi 4   ∨ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1i  750  orim2i  751  dcim  827  pm5.12dc  896  pm5.14dc  897  pm5.55dc  899  pm5.54dc  904  prlem2  959  xordc1  1372  19.43  1608  eueq3dc  2862  inssun  3321  abvor0dc  3391  ifmdc  3514  undifexmid  4125  pwssunim  4214  ordtriexmid  4445  ordtri2orexmid  4446  ontr2exmid  4448  onsucsssucexmid  4450  onsucelsucexmid  4453  ordsoexmid  4485  0elsucexmid  4488  ordpwsucexmid  4493  ordtri2or2exmid  4494  funcnvuni  5200  oprabidlem  5810  2oconcl  6344  inffiexmid  6808  unfiexmid  6814  ctssexmid  7032  exmidonfinlem  7066  sup3exmid  8739  zeo  9180  ef0lem  11403