Theorem orim12i 909

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  orim1i  910  orim2i  911  prlem2  1056  ifpor  1073  eueq3  3658  pwssun  5516  xpima  6140  fvresval  7306  0mpo0  7443  funcnvuni  7876  2oconcl  8431  djur  9834  djuun  9841  fin23lem23  10239  fin23lem19  10249  fin1a2lem13  10325  fin1a2s  10327  nn0ge0  12453  elfzlmr  13728  hash2pwpr  14429  trclfvg  14968  xpcbas  18135  odcl  19502  gexcl  19546  ang180lem4  26789  ltsn0  27912  n0seo  28427  elim2ifim  32630  locfinref  34001  volmeas  34391  nepss  35916  funpsstri  35964  bj-prmoore  37443  bj-imdirco  37520  dvasin  38039  dvacos  38040  disjorimxrn  39183  relexpxpmin  44162  clsk1indlem3  44488  elsprel  47947  resolution  50286