Theorem orim2i 762

Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)

Hypothesis

Ref	Expression
orim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
orim2i	⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Proof of Theorem orim2i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜒 → 𝜒)
2		orim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	orim12i 760	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  763  pm1.5  766  pm2.3  776  ordi  817  dcn  843  pm2.25dc  894  dcand  934  axi12  1525  dveeq2or  1827  equs5or  1841  sb4or  1844  sb4bor  1846  nfsb2or  1848  sbequilem  1849  sbequi  1850  sbal1yz  2017  dvelimor  2034  exmodc  2092  r19.44av  2653  exmidundif  4235  exmidundifim  4236  exmid1stab  4237  elsuci  4434  acexmidlemcase  5913  undifdcss  6979  updjudhf  7138  ctssdccl  7170  zindd  9435  fiubm  10899  fsumsplitsn  11553  fprodcllem  11749  fprodsplitsn  11776  gsumwsubmcl  13068  gsumwmhm  13070  subctctexmid  15491