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  3717  pwssun  5575  xpima  6202  fvresval  7378  0mpo0  7516  funcnvuni  7954  2oconcl  8541  djur  9959  djuun  9966  fin23lem23  10366  fin23lem19  10376  fin1a2lem13  10452  fin1a2s  10454  nn0ge0  12551  elfzlmr  13820  hash2pwpr  14515  trclfvg  15054  xpcbas  18223  odcl  19554  gexcl  19598  ang180lem4  26855  sltn0  27943  n0seo  28405  elim2ifim  32558  locfinref  33840  volmeas  34232  nepss  35718  funpsstri  35766  bj-prmoore  37116  bj-imdirco  37191  dvasin  37711  dvacos  37712  disjorimxrn  38749  relexpxpmin  43730  clsk1indlem3  44056  elsprel  47462  resolution  49318