Theorem orim12i 907

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

Syntax hints:   → wi 4   ∨ wo 845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-or 846

This theorem is referenced by:  orim1i  908  orim2i  909  prlem2  1054  ifpor  1071  eueq3  3660  pwssun  5519  xpima  6124  fvresval  7289  0mpo0  7424  funcnvuni  7850  2oconcl  8408  djur  9780  djuun  9787  fin23lem23  10187  fin23lem19  10197  fin1a2lem13  10273  fin1a2s  10275  nn0ge0  12363  elfzlmr  13606  hash2pwpr  14294  trclfvg  14825  xpcbas  17992  odcl  19240  gexcl  19281  ang180lem4  26067  elim2ifim  31173  locfinref  32087  volmeas  32495  nepss  33957  funpsstri  34023  sltn0  34193  bj-prmoore  35440  bj-imdirco  35515  dvasin  36017  dvacos  36018  disjorimxrn  37066  relexpxpmin  41698  clsk1indlem3  42026  elsprel  45345  resolution  46921