Theorem orim2i 773

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orbi2i  774  pm1.5  777  pm2.3  787  ordi  828  dcn  854  pm2.25dc  905  dcand  945  axi12  1567  dveeq2or  1869  equs5or  1883  sb4or  1886  sb4bor  1888  nfsb2or  1890  sbequilem  1891  sbequi  1892  sbal1yz  2061  dvelimor  2078  exmodc  2137  r19.44av  2710  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  elsuci  4550  acexmidlemcase  6083  undifdcss  7235  updjudhf  7426  ctssdccl  7458  zindd  9776  fiubm  11294  lswex  11379  fsumsplitsn  12203  fprodcllem  12399  fprodsplitsn  12426  gzsumwsubmcl  13861  gzsumwmhm  13863  subctctexmid  17247