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  3670  pwssun  5508  xpima  6129  fvresval  7292  0mpo0  7429  funcnvuni  7862  2oconcl  8418  djur  9812  djuun  9819  fin23lem23  10217  fin23lem19  10227  fin1a2lem13  10303  fin1a2s  10305  nn0ge0  12406  elfzlmr  13682  hash2pwpr  14383  trclfvg  14922  xpcbas  18084  odcl  19449  gexcl  19493  ang180lem4  26750  sltn0  27852  n0seo  28345  elim2ifim  32523  locfinref  33852  volmeas  34242  nepss  35760  funpsstri  35808  bj-prmoore  37155  bj-imdirco  37230  dvasin  37750  dvacos  37751  disjorimxrn  38792  relexpxpmin  43756  clsk1indlem3  44082  elsprel  47512  resolution  49837