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  5548  xpima  6187  fvresval  7394  0mpo0  7529  funcnvuni  7971  2oconcl  8542  djur  10030  djuun  10037  fin23lem23  10434  fin23lem19  10444  fin1a2lem13  10520  fin1a2s  10522  nn0ge0  12661  elfzlmr  13947  hash2pwpr  14651  trclfvg  15200  xpcbas  18384  odcl  19783  gexcl  19827  ang180lem4  27173  ltsn0  28325  n0seo  28840  elim2ifim  33216  locfinref  34556  volmeas  34947  nepss  36674  funpsstri  36722  bj-prmoore  38240  bj-imdirco  38316  dvasin  38827  dvacos  38828  disjorimxrn  39983  relexpxpmin  44920  clsk1indlem3  45246  elsprel  48772  resolution  51249