Theorem orim12i 921

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orim1i  922  orim2i  923  prlem2  1069  ifpor  1087  eueq3  3677  pwssun  5543  xpima  6171  fvresval  7346  0mpo0  7483  funcnvuni  7917  2oconcl  8476  djur  9893  djuun  9900  fin23lem23  10298  fin23lem19  10308  fin1a2lem13  10384  fin1a2s  10386  nn0ge0  12517  elfzlmr  13799  hash2pwpr  14501  trclfvg  15040  xpcbas  18222  odcl  19594  gexcl  19638  ang180lem4  26931  ltsn0  28053  n0seo  28568  elim2ifim  32797  locfinref  34143  volmeas  34533  nepss  36076  funpsstri  36124  bj-prmoore  37612  bj-imdirco  37689  dvasin  38210  dvacos  38211  disjorimxrn  39354  relexpxpmin  44300  clsk1indlem3  44626  elsprel  48080  resolution  50429