Theorem orim2i 763

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

Syntax hints:   → wi 4   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  764  pm1.5  767  pm2.3  777  ordi  818  dcn  844  pm2.25dc  895  dcand  935  axi12  1538  dveeq2or  1840  equs5or  1854  sb4or  1857  sb4bor  1859  nfsb2or  1861  sbequilem  1862  sbequi  1863  sbal1yz  2030  dvelimor  2047  exmodc  2105  r19.44av  2666  exmidundif  4255  exmidundifim  4256  exmid1stab  4257  elsuci  4455  acexmidlemcase  5949  undifdcss  7032  updjudhf  7193  ctssdccl  7225  zindd  9504  fiubm  10986  lswex  11058  fsumsplitsn  11771  fprodcllem  11967  fprodsplitsn  11994  gsumwsubmcl  13378  gsumwmhm  13380  subctctexmid  16052