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  3685  pwssun  5533  xpima  6158  fvresval  7336  0mpo0  7475  funcnvuni  7911  2oconcl  8470  djur  9879  djuun  9886  fin23lem23  10286  fin23lem19  10296  fin1a2lem13  10372  fin1a2s  10374  nn0ge0  12474  elfzlmr  13749  hash2pwpr  14448  trclfvg  14988  xpcbas  18146  odcl  19473  gexcl  19517  ang180lem4  26729  sltn0  27824  n0seo  28314  elim2ifim  32481  locfinref  33838  volmeas  34228  nepss  35712  funpsstri  35760  bj-prmoore  37110  bj-imdirco  37185  dvasin  37705  dvacos  37706  disjorimxrn  38747  relexpxpmin  43713  clsk1indlem3  44039  elsprel  47480  resolution  49792