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  3669  pwssun  5543  xpima  6173  fvresval  7360  0mpo0  7495  funcnvuni  7933  2oconcl  8495  djur  9981  djuun  9988  fin23lem23  10385  fin23lem19  10395  fin1a2lem13  10471  fin1a2s  10473  nn0ge0  12612  elfzlmr  13897  hash2pwpr  14601  trclfvg  15148  xpcbas  18332  odcl  19730  gexcl  19774  ang180lem4  27122  ltsn0  28274  n0seo  28789  elim2ifim  33123  locfinref  34455  volmeas  34846  nepss  36452  funpsstri  36500  bj-prmoore  38004  bj-imdirco  38079  dvasin  38590  dvacos  38591  disjorimxrn  39748  relexpxpmin  44676  clsk1indlem3  45002  elsprel  48501  resolution  50881