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

This theorem is referenced by:  orim1i  538  orim2i  539  prlem2  1026  ifpor  1041  eueq3  3414  pwssun  5049  xpima  5611  funcnvuni  7161  2oconcl  7628  fin23lem23  9186  fin23lem19  9196  fin1a2lem13  9272  fin1a2s  9274  nn0ge0  11356  elfzlmr  12622  hash2pwpr  13296  trclfvg  13800  mreexexdOLD  16356  xpcbas  16865  odcl  18001  gexcl  18041  ang180lem4  24587  elim2ifim  29490  locfinref  30036  volmeas  30422  nepss  31725  funpsstri  31789  fvresval  31791  dvasin  33626  dvacos  33627  relexpxpmin  38326  clsk1indlem3  38658  elsprel  42050  resolution  42873