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  4291  exmidundifim  4292  exmid1stab  4293  elsuci  4495  acexmidlemcase  6005  undifdcss  7101  updjudhf  7262  ctssdccl  7294  zindd  9581  fiubm  11068  lswex  11141  fsumsplitsn  11942  fprodcllem  12138  fprodsplitsn  12165  gsumwsubmcl  13550  gsumwmhm  13552  subctctexmid  16479