Theorem orim12i 908

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orim1i  909  orim2i  910  prlem2  1055  ifpor  1072  eueq3  3673  pwssun  5515  xpima  6135  fvresval  7299  0mpo0  7436  funcnvuni  7872  2oconcl  8428  djur  9834  djuun  9841  fin23lem23  10239  fin23lem19  10249  fin1a2lem13  10325  fin1a2s  10327  nn0ge0  12427  elfzlmr  13702  hash2pwpr  14401  trclfvg  14940  xpcbas  18102  odcl  19433  gexcl  19477  ang180lem4  26738  sltn0  27838  n0seo  28331  elim2ifim  32507  locfinref  33810  volmeas  34200  nepss  35693  funpsstri  35741  bj-prmoore  37091  bj-imdirco  37166  dvasin  37686  dvacos  37687  disjorimxrn  38728  relexpxpmin  43693  clsk1indlem3  44019  elsprel  47463  resolution  49788