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  2055  dvelimor  2072  exmodc  2131  r19.44av  2702  exmidundif  4318  exmidundifim  4319  exmid1stab  4320  elsuci  4523  acexmidlemcase  6044  undifdcss  7182  updjudhf  7369  ctssdccl  7401  zindd  9695  fiubm  11191  lswex  11272  fsumsplitsn  12092  fprodcllem  12288  fprodsplitsn  12315  gsumwsubmcl  13701  gsumwmhm  13703  subctctexmid  16766