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  3666  pwssun  5513  xpima  6136  fvresval  7300  0mpo0  7437  funcnvuni  7870  2oconcl  8426  djur  9821  djuun  9828  fin23lem23  10226  fin23lem19  10236  fin1a2lem13  10312  fin1a2s  10314  nn0ge0  12415  elfzlmr  13686  hash2pwpr  14387  trclfvg  14926  xpcbas  18088  odcl  19452  gexcl  19496  ang180lem4  26752  sltn0  27854  n0seo  28347  elim2ifim  32529  locfinref  33877  volmeas  34267  nepss  35785  funpsstri  35833  bj-prmoore  37182  bj-imdirco  37257  dvasin  37767  dvacos  37768  disjorimxrn  38869  relexpxpmin  43837  clsk1indlem3  44163  elsprel  47602  resolution  49927