Theorem orim2i 916

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

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  orbi2i  918  pm1.5  925  pm2.3  930  r19.44v  3175  elpwunsn  4623  elsuci  6386  infxpenlem  9933  fin1a2lem12  10331  fin1a2  10335  entri3  10479  zindd  12628  elfzr  13734  hashnn0pnf  14302  limccnp  25883  tgldimor  28595  ex-natded5.7-2  30507  chirredi  32490  meran1  36646  dissym1  36656  ordtoplem  36670  ordcmp  36682  poimirlem31  38025  simpcntrab  47320  setc2othin  49963