Theorem orim2i 908

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 22	. 2 ⊢ (𝜒 → 𝜒)
2		orim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	orim12i 906	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-or 845

This theorem is referenced by:  orbi2i  910  pm1.5  917  pm2.3  922  r19.44v  3281  elpwunsn  4619  elsuci  6332  infxpenlem  9769  fin1a2lem12  10167  fin1a2  10171  entri3  10315  zindd  12421  elfzr  13500  hashnn0pnf  14056  limccnp  25055  tgldimor  26863  ex-natded5.7-2  28776  chirredi  30756  meran1  34600  dissym1  34610  ordtoplem  34624  ordcmp  34636  poimirlem31  35808  simpcntrab  44386  setc2othin  46337