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  3719  pwssun  5579  xpima  6203  fvresval  7377  0mpo0  7515  funcnvuni  7954  2oconcl  8539  djur  9956  djuun  9963  fin23lem23  10363  fin23lem19  10373  fin1a2lem13  10449  fin1a2s  10451  nn0ge0  12548  elfzlmr  13816  hash2pwpr  14511  trclfvg  15050  xpcbas  18233  odcl  19568  gexcl  19612  ang180lem4  26869  sltn0  27957  n0seo  28419  elim2ifim  32565  locfinref  33801  volmeas  34211  nepss  35697  funpsstri  35746  bj-prmoore  37097  bj-imdirco  37172  dvasin  37690  dvacos  37691  disjorimxrn  38729  relexpxpmin  43706  clsk1indlem3  44032  elsprel  47399  resolution  49029