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  3352  elpwunsn  4621  elsuci  6257  infxpenlem  9439  fin1a2lem12  9833  fin1a2  9837  entri3  9981  zindd  12084  elfzr  13151  hashnn0pnf  13703  limccnp  24489  tgldimor  26288  ex-natded5.7-2  28191  chirredi  30171  meran1  33759  dissym1  33769  ordtoplem  33783  ordcmp  33795  poimirlem31  34938  simpcntrab  43147