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  3694  pwssun  5545  xpima  6171  fvresval  7351  0mpo0  7490  funcnvuni  7928  2oconcl  8515  djur  9933  djuun  9940  fin23lem23  10340  fin23lem19  10350  fin1a2lem13  10426  fin1a2s  10428  nn0ge0  12526  elfzlmr  13797  hash2pwpr  14494  trclfvg  15034  xpcbas  18190  odcl  19517  gexcl  19561  ang180lem4  26774  sltn0  27869  n0seo  28359  elim2ifim  32526  locfinref  33872  volmeas  34262  nepss  35735  funpsstri  35783  bj-prmoore  37133  bj-imdirco  37208  dvasin  37728  dvacos  37729  disjorimxrn  38766  relexpxpmin  43741  clsk1indlem3  44067  elsprel  47489  resolution  49663