Theorem orim12i 914

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

Syntax hints:   → wi 4   ∨ wo 853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-or 854

This theorem is referenced by:  orim1i  915  orim2i  916  prlem2  1061  ifpor  1078  eueq3  3659  pwssun  5517  xpima  6140  fvresval  7309  0mpo0  7446  funcnvuni  7879  2oconcl  8435  djur  9841  djuun  9848  fin23lem23  10246  fin23lem19  10256  fin1a2lem13  10332  fin1a2s  10334  nn0ge0  12460  elfzlmr  13735  hash2pwpr  14436  trclfvg  14975  xpcbas  18142  odcl  19509  gexcl  19553  ang180lem4  26801  ltsn0  27923  n0seo  28438  elim2ifim  32640  locfinref  34032  volmeas  34422  nepss  35953  funpsstri  36001  bj-prmoore  37480  bj-imdirco  37557  dvasin  38078  dvacos  38079  disjorimxrn  39222  relexpxpmin  44168  clsk1indlem3  44494  elsprel  47957  resolution  50296