Theorem orim12i 905

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

Syntax hints:   → wi 4   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  orim1i  906  orim2i  907  prlem2  1052  ifpor  1069  eueq3  3641  pwssun  5476  xpima  6074  0mpo0  7336  funcnvuni  7752  2oconcl  8295  djur  9608  djuun  9615  fin23lem23  10013  fin23lem19  10023  fin1a2lem13  10099  fin1a2s  10101  nn0ge0  12188  elfzlmr  13429  hash2pwpr  14118  trclfvg  14654  xpcbas  17811  odcl  19059  gexcl  19100  ang180lem4  25867  elim2ifim  30789  locfinref  31693  volmeas  32099  nepss  33564  funpsstri  33645  fvresval  33647  sltn0  34012  bj-prmoore  35213  bj-imdirco  35288  dvasin  35788  dvacos  35789  disjorimxrn  36783  relexpxpmin  41214  clsk1indlem3  41542  elsprel  44815  resolution  46389