Theorem orim12i 909

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

This theorem is referenced by:  orim1i  910  orim2i  911  prlem2  1056  ifpor  1073  eueq3  3624  pwssun  5451  xpima  6045  0mpo0  7294  funcnvuni  7709  2oconcl  8230  djur  9535  djuun  9542  fin23lem23  9940  fin23lem19  9950  fin1a2lem13  10026  fin1a2s  10028  nn0ge0  12115  elfzlmr  13356  hash2pwpr  14042  trclfvg  14578  xpcbas  17685  odcl  18928  gexcl  18969  ang180lem4  25695  elim2ifim  30607  locfinref  31505  volmeas  31911  nepss  33377  funpsstri  33458  fvresval  33460  sltn0  33822  bj-prmoore  35021  bj-imdirco  35096  dvasin  35598  dvacos  35599  disjorimxrn  36593  relexpxpmin  41002  clsk1indlem3  41330  elsprel  44600  resolution  46174