Theorem orim12i 919

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  orim1i  920  orim2i  921  prlem2  1066  ifpor  1083  eueq3  3672  pwssun  5535  xpima  6162  fvresval  7336  0mpo0  7473  funcnvuni  7907  2oconcl  8465  djur  9870  djuun  9877  fin23lem23  10276  fin23lem19  10286  fin1a2lem13  10362  fin1a2s  10364  nn0ge0  12499  elfzlmr  13781  hash2pwpr  14482  trclfvg  15021  xpcbas  18200  odcl  19566  gexcl  19610  ang180lem4  26864  ltsn0  27986  n0seo  28501  elim2ifim  32703  locfinref  34098  volmeas  34488  nepss  36028  funpsstri  36076  bj-prmoore  37565  bj-imdirco  37642  dvasin  38163  dvacos  38164  disjorimxrn  39307  relexpxpmin  44253  clsk1indlem3  44579  elsprel  48041  resolution  50380