Theorem orim12i 905

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 869	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
3		orim12i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	olcd 870	. 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃))
5	2, 4	jaoi 853	1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  orim1i  906  orim2i  907  prlem2  1052  ifpor  1069  eueq3  3706  pwssun  5570  xpima  6180  fvresval  7357  0mpo0  7494  funcnvuni  7924  2oconcl  8505  djur  9916  djuun  9923  fin23lem23  10323  fin23lem19  10333  fin1a2lem13  10409  fin1a2s  10411  nn0ge0  12501  elfzlmr  13750  hash2pwpr  14441  trclfvg  14966  xpcbas  18134  odcl  19445  gexcl  19489  ang180lem4  26553  sltn0  27636  elim2ifim  32044  locfinref  33119  volmeas  33527  nepss  34991  funpsstri  35041  bj-prmoore  36299  bj-imdirco  36374  dvasin  36875  dvacos  36876  disjorimxrn  37921  relexpxpmin  42770  clsk1indlem3  43096  elsprel  46441  resolution  47933