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

This theorem is referenced by:  orbi2i  909  pm1.5  916  pm2.3  921  r19.44v  3278  elpwunsn  4616  elsuci  6317  infxpenlem  9700  fin1a2lem12  10098  fin1a2  10102  entri3  10246  zindd  12351  elfzr  13428  hashnn0pnf  13984  limccnp  24960  tgldimor  26767  ex-natded5.7-2  28677  chirredi  30657  meran1  34527  dissym1  34537  ordtoplem  34551  ordcmp  34563  poimirlem31  35735  simpcntrab  44273  setc2othin  46225