Theorem orim2i 766

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  767  pm1.5  770  pm2.3  780  ordi  821  dcn  847  pm2.25dc  898  dcand  938  axi12  1560  dveeq2or  1862  equs5or  1876  sb4or  1879  sb4bor  1881  nfsb2or  1883  sbequilem  1884  sbequi  1885  sbal1yz  2052  dvelimor  2069  exmodc  2128  r19.44av  2690  exmidundif  4289  exmidundifim  4290  exmid1stab  4291  elsuci  4491  acexmidlemcase  5989  undifdcss  7073  updjudhf  7234  ctssdccl  7266  zindd  9553  fiubm  11037  lswex  11109  fsumsplitsn  11907  fprodcllem  12103  fprodsplitsn  12130  gsumwsubmcl  13515  gsumwmhm  13517  subctctexmid  16297