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  3657  pwssun  5523  xpima  6146  fvresval  7313  0mpo0  7450  funcnvuni  7883  2oconcl  8438  djur  9843  djuun  9850  fin23lem23  10248  fin23lem19  10258  fin1a2lem13  10334  fin1a2s  10336  nn0ge0  12462  elfzlmr  13737  hash2pwpr  14438  trclfvg  14977  xpcbas  18144  odcl  19511  gexcl  19555  ang180lem4  26776  ltsn0  27898  n0seo  28413  elim2ifim  32615  locfinref  33985  volmeas  34375  nepss  35900  funpsstri  35948  bj-prmoore  37427  bj-imdirco  37504  dvasin  38025  dvacos  38026  disjorimxrn  39169  relexpxpmin  44144  clsk1indlem3  44470  elsprel  47935  resolution  50274