Theorem orim12i 537

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

Syntax hints:   → wi 4   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  orim1i  538  orim2i  539  prlem2  998  ifpor  1015  eueq3  3348  pwssun  4944  xpima  5495  funcnvuni  7012  2oconcl  7470  fin23lem23  9031  fin23lem19  9041  fin1a2lem13  9117  fin1a2s  9119  nn0ge0  11195  hash2pwpr  13115  trclfvg  13604  mreexexdOLD  16132  xpcbas  16641  odcl  17778  gexcl  17818  ang180lem4  24342  cusgrares  26001  2pthlem2  26126  elim2ifim  28748  locfinref  29236  volmeas  29621  nepss  30854  funpsstri  30909  fvresval  30911  dvasin  32666  dvacos  32667  relexpxpmin  37028  clsk1indlem3  37361  elfzlmr  40366  resolution  42354