Theorem orim12i 908

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orim1i  909  orim2i  910  prlem2  1055  ifpor  1072  eueq3  3669  pwssun  5516  xpima  6140  fvresval  7304  0mpo0  7441  funcnvuni  7874  2oconcl  8430  djur  9831  djuun  9838  fin23lem23  10236  fin23lem19  10246  fin1a2lem13  10322  fin1a2s  10324  nn0ge0  12426  elfzlmr  13698  hash2pwpr  14399  trclfvg  14938  xpcbas  18101  odcl  19465  gexcl  19509  ang180lem4  26778  ltsn0  27902  n0seo  28417  elim2ifim  32620  locfinref  33998  volmeas  34388  nepss  35912  funpsstri  35960  bj-prmoore  37320  bj-imdirco  37395  dvasin  37905  dvacos  37906  disjorimxrn  39007  relexpxpmin  43958  clsk1indlem3  44284  elsprel  47721  resolution  50044