Theorem orim2i 733

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

Syntax hints:   → wi 4   ∨ wo 680

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi2i  734  pm1.5  737  pm2.3  747  ordi  788  dcn  810  pm2.25dc  859  dcan  899  axi12  1475  dveeq2or  1768  equs5or  1782  sb4or  1785  sb4bor  1787  nfsb2or  1789  sbequilem  1790  sbequi  1791  sbal1yz  1950  dvelimor  1967  exmodc  2023  r19.44av  2562  exmidundif  4087  exmidundifim  4088  elsuci  4283  acexmidlemcase  5721  undifdcss  6762  updjudhf  6914  ctssdccl  6946  zindd  9067  fsumsplitsn  11065