Theorem orim12i 906

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

Syntax hints:   → wi 4   ∨ wo 844

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 845

This theorem is referenced by:  orim1i  907  orim2i  908  prlem2  1053  ifpor  1070  eueq3  3646  pwssun  5485  xpima  6085  0mpo0  7358  funcnvuni  7778  2oconcl  8333  djur  9677  djuun  9684  fin23lem23  10082  fin23lem19  10092  fin1a2lem13  10168  fin1a2s  10170  nn0ge0  12258  elfzlmr  13501  hash2pwpr  14190  trclfvg  14726  xpcbas  17895  odcl  19144  gexcl  19185  ang180lem4  25962  elim2ifim  30888  locfinref  31791  volmeas  32199  nepss  33662  funpsstri  33739  fvresval  33741  sltn0  34085  bj-prmoore  35286  bj-imdirco  35361  dvasin  35861  dvacos  35862  disjorimxrn  36856  relexpxpmin  41325  clsk1indlem3  41653  elsprel  44927  resolution  46503