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  3682  pwssun  5530  xpima  6155  fvresval  7333  0mpo0  7472  funcnvuni  7908  2oconcl  8467  djur  9872  djuun  9879  fin23lem23  10279  fin23lem19  10289  fin1a2lem13  10365  fin1a2s  10367  nn0ge0  12467  elfzlmr  13742  hash2pwpr  14441  trclfvg  14981  xpcbas  18139  odcl  19466  gexcl  19510  ang180lem4  26722  sltn0  27817  n0seo  28307  elim2ifim  32474  locfinref  33831  volmeas  34221  nepss  35705  funpsstri  35753  bj-prmoore  37103  bj-imdirco  37178  dvasin  37698  dvacos  37699  disjorimxrn  38740  relexpxpmin  43706  clsk1indlem3  44032  elsprel  47476  resolution  49788