Theorem orim12i 922

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orim1i  923  orim2i  924  prlem2  1071  ifpor  1089  eueq3  3672  pwssun  5551  xpima  6179  fvresval  7365  0mpo0  7500  funcnvuni  7933  2oconcl  8494  djur  9928  djuun  9935  fin23lem23  10332  fin23lem19  10342  fin1a2lem13  10418  fin1a2s  10420  nn0ge0  12557  elfzlmr  13842  hash2pwpr  14545  trclfvg  15092  xpcbas  18272  odcl  19669  gexcl  19713  ang180lem4  27057  ltsn0  28179  n0seo  28694  elim2ifim  33028  locfinref  34359  volmeas  34750  nepss  36305  funpsstri  36353  bj-prmoore  37873  bj-imdirco  37950  dvasin  38461  dvacos  38462  disjorimxrn  39604  relexpxpmin  44565  clsk1indlem3  44891  elsprel  48383  resolution  50778