Theorem orim12i 907

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  orim1i  908  orim2i  909  prlem2  1056  ifpor  1073  eueq3  3733  pwssun  5590  xpima  6213  fvresval  7394  0mpo0  7533  funcnvuni  7972  2oconcl  8559  djur  9988  djuun  9995  fin23lem23  10395  fin23lem19  10405  fin1a2lem13  10481  fin1a2s  10483  nn0ge0  12578  elfzlmr  13831  hash2pwpr  14525  trclfvg  15064  xpcbas  18247  odcl  19578  gexcl  19622  ang180lem4  26873  sltn0  27961  n0seo  28423  elim2ifim  32568  locfinref  33787  volmeas  34195  nepss  35680  funpsstri  35729  bj-prmoore  37081  bj-imdirco  37156  dvasin  37664  dvacos  37665  disjorimxrn  38704  relexpxpmin  43679  clsk1indlem3  44005  elsprel  47349  resolution  48893