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

This theorem is referenced by:  orim1i  906  orim2i  907  prlem2  1050  ifpor  1066  eueq3  3702  pwssun  5456  xpima  6039  0mpo0  7237  funcnvuni  7636  2oconcl  8128  djur  9348  djuun  9355  fin23lem23  9748  fin23lem19  9758  fin1a2lem13  9834  fin1a2s  9836  nn0ge0  11923  elfzlmr  13152  hash2pwpr  13835  trclfvg  14375  xpcbas  17428  odcl  18664  gexcl  18705  ang180lem4  25390  elim2ifim  30300  locfinref  31105  volmeas  31490  nepss  32948  funpsstri  33008  fvresval  33010  bj-prmoore  34410  dvasin  34993  dvacos  34994  disjorimxrn  35993  relexpxpmin  40082  clsk1indlem3  40413  elsprel  43657  resolution  44920