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

Syntax hints:   → wi 4   ∨ wo 845

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 846

This theorem is referenced by:  orim1i  907  orim2i  908  prlem2  1053  ifpor  1070  eueq3  3703  pwssun  5573  xpima  6188  fvresval  7365  0mpo0  7503  funcnvuni  7940  2oconcl  8524  djur  9944  djuun  9951  fin23lem23  10351  fin23lem19  10361  fin1a2lem13  10437  fin1a2s  10439  nn0ge0  12530  elfzlmr  13782  hash2pwpr  14473  trclfvg  14998  xpcbas  18172  odcl  19503  gexcl  19547  ang180lem4  26789  sltn0  27877  elim2ifim  32415  locfinref  33573  volmeas  33981  nepss  35443  funpsstri  35492  bj-prmoore  36725  bj-imdirco  36800  dvasin  37308  dvacos  37309  disjorimxrn  38350  relexpxpmin  43289  clsk1indlem3  43615  elsprel  46952  resolution  48418