Theorem orim12i 921

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orim1i  922  orim2i  923  prlem2  1071  ifpor  1089  eueq3  3675  pwssun  5555  xpima  6182  fvresval  7358  0mpo0  7495  funcnvuni  7930  2oconcl  8489  djur  9906  djuun  9913  fin23lem23  10311  fin23lem19  10321  fin1a2lem13  10397  fin1a2s  10399  nn0ge0  12530  elfzlmr  13813  hash2pwpr  14515  trclfvg  15054  xpcbas  18235  odcl  19607  gexcl  19651  ang180lem4  26958  ltsn0  28080  n0seo  28595  elim2ifim  32872  locfinref  34212  volmeas  34602  nepss  36191  funpsstri  36239  bj-prmoore  37738  bj-imdirco  37815  dvasin  38336  dvacos  38337  disjorimxrn  39478  relexpxpmin  44426  clsk1indlem3  44752  elsprel  48207  resolution  50582