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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  orim1i  909  orim2i  910  prlem2  1055  ifpor  1072  eueq3  3708  pwssun  5572  xpima  6182  fvresval  7355  0mpo0  7492  funcnvuni  7922  2oconcl  8503  djur  9914  djuun  9921  fin23lem23  10321  fin23lem19  10331  fin1a2lem13  10407  fin1a2s  10409  nn0ge0  12497  elfzlmr  13746  hash2pwpr  14437  trclfvg  14962  xpcbas  18130  odcl  19404  gexcl  19448  ang180lem4  26317  sltn0  27399  elim2ifim  31777  locfinref  32821  volmeas  33229  nepss  34687  funpsstri  34737  bj-prmoore  35996  bj-imdirco  36071  dvasin  36572  dvacos  36573  disjorimxrn  37618  relexpxpmin  42468  clsk1indlem3  42794  elsprel  46143  resolution  47846