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  3677  pwssun  5558  xpima  6185  fvresval  7369  0mpo0  7506  funcnvuni  7938  2oconcl  8497  djur  9924  djuun  9931  fin23lem23  10328  fin23lem19  10338  fin1a2lem13  10414  fin1a2s  10416  nn0ge0  12547  elfzlmr  13830  hash2pwpr  14533  trclfvg  15078  xpcbas  18259  odcl  19637  gexcl  19681  ang180lem4  27014  ltsn0  28136  n0seo  28651  elim2ifim  32928  locfinref  34262  volmeas  34653  nepss  36231  funpsstri  36279  bj-prmoore  37798  bj-imdirco  37875  dvasin  38396  dvacos  38397  disjorimxrn  39538  relexpxpmin  44484  clsk1indlem3  44810  elsprel  48265  resolution  50660