Theorem orim2i 907

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

Syntax hints:   → wi 4   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  orbi2i  909  pm1.5  916  pm2.3  921  r19.44v  3354  elpwunsn  4623  elsuci  6259  infxpenlem  9441  fin1a2lem12  9835  fin1a2  9839  entri3  9983  zindd  12086  elfzr  13153  hashnn0pnf  13705  limccnp  24491  tgldimor  26290  ex-natded5.7-2  28193  chirredi  30173  meran1  33761  dissym1  33771  ordtoplem  33785  ordcmp  33797  poimirlem31  34925  simpcntrab  43134