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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  orim1i  910  orim2i  911  prlem2  1056  ifpor  1073  eueq3  3671  pwssun  5524  xpima  6148  fvresval  7314  0mpo0  7451  funcnvuni  7884  2oconcl  8440  djur  9843  djuun  9850  fin23lem23  10248  fin23lem19  10258  fin1a2lem13  10334  fin1a2s  10336  nn0ge0  12438  elfzlmr  13710  hash2pwpr  14411  trclfvg  14950  xpcbas  18113  odcl  19477  gexcl  19521  ang180lem4  26790  ltsn0  27914  n0seo  28429  elim2ifim  32631  locfinref  34018  volmeas  34408  nepss  35931  funpsstri  35979  bj-prmoore  37365  bj-imdirco  37442  dvasin  37952  dvacos  37953  disjorimxrn  39096  relexpxpmin  44070  clsk1indlem3  44396  elsprel  47832  resolution  50155