Theorem orim12i 761

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

Syntax hints:   → wi 4   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1i  762  orim2i  763  dcim  843  pm5.12dc  912  pm5.14dc  913  pm5.55dc  915  pm5.54dc  920  prlem2  977  xordc1  1413  19.43  1652  eueq3dc  2951  inssun  3417  abvor0dc  3488  ifmdc  3616  undifexmid  4244  pwssunim  4338  ordtriexmid  4576  ontriexmidim  4577  ordtri2orexmid  4578  ontr2exmid  4580  onsucsssucexmid  4582  onsucelsucexmid  4585  ordsoexmid  4617  0elsucexmid  4620  ordpwsucexmid  4625  ordtri2or2exmid  4626  ontri2orexmidim  4627  funcnvuni  5351  oprabidlem  5987  2oconcl  6537  inffiexmid  7017  unfiexmid  7029  ctssexmid  7266  exmidonfinlem  7316  sup3exmid  9045  zeo  9493  ef0lem  12041