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  4294  exmidundifim  4295  exmid1stab  4296  elsuci  4498  acexmidlemcase  6008  undifdcss  7110  updjudhf  7272  ctssdccl  7304  zindd  9591  fiubm  11085  lswex  11158  fsumsplitsn  11964  fprodcllem  12160  fprodsplitsn  12187  gsumwsubmcl  13572  gsumwmhm  13574  subctctexmid  16551