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  1864  equs5or  1878  sb4or  1881  sb4bor  1883  nfsb2or  1885  sbequilem  1886  sbequi  1887  sbal1yz  2054  dvelimor  2071  exmodc  2130  r19.44av  2693  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  elsuci  4506  acexmidlemcase  6023  undifdcss  7158  updjudhf  7321  ctssdccl  7353  zindd  9641  fiubm  11136  lswex  11212  fsumsplitsn  12032  fprodcllem  12228  fprodsplitsn  12255  gsumwsubmcl  13640  gsumwmhm  13642  subctctexmid  16702