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  3668  pwssun  5542  xpima  6173  fvresval  7369  0mpo0  7504  funcnvuni  7945  2oconcl  8515  djur  10004  djuun  10011  fin23lem23  10408  fin23lem19  10418  fin1a2lem13  10494  fin1a2s  10496  nn0ge0  12635  elfzlmr  13921  hash2pwpr  14625  trclfvg  15174  xpcbas  18358  odcl  19756  gexcl  19800  ang180lem4  27146  ltsn0  28298  n0seo  28813  elim2ifim  33189  locfinref  34520  volmeas  34911  nepss  36576  funpsstri  36624  bj-prmoore  38129  bj-imdirco  38205  dvasin  38716  dvacos  38717  disjorimxrn  39874  relexpxpmin  44811  clsk1indlem3  45137  elsprel  48651  resolution  51106