Theorem orim2i 769

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 767	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  770  pm1.5  773  pm2.3  783  ordi  824  dcn  850  pm2.25dc  901  dcand  941  axi12  1563  dveeq2or  1865  equs5or  1879  sb4or  1882  sb4bor  1884  nfsb2or  1886  sbequilem  1887  sbequi  1888  sbal1yz  2057  dvelimor  2074  exmodc  2133  r19.44av  2704  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  elsuci  4529  acexmidlemcase  6053  undifdcss  7196  updjudhf  7383  ctssdccl  7415  zindd  9714  fiubm  11220  lswex  11301  fsumsplitsn  12121  fprodcllem  12317  fprodsplitsn  12344  gsumwsubmcl  13793  gsumwmhm  13795  subctctexmid  16886