Theorem orim2i 910

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  orbi2i  912  pm1.5  919  pm2.3  924  r19.44v  3194  elpwunsn  4688  elsuci  6432  infxpenlem  10008  fin1a2lem12  10406  fin1a2  10410  entri3  10554  zindd  12663  elfzr  13745  hashnn0pnf  14302  limccnp  25408  tgldimor  27753  ex-natded5.7-2  29665  chirredi  31647  meran1  35296  dissym1  35306  ordtoplem  35320  ordcmp  35332  poimirlem31  36519  simpcntrab  45586  setc2othin  47676