Theorem orim2i 908

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

Syntax hints:   → wi 4   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  orbi2i  910  pm1.5  917  pm2.3  922  r19.44v  3305  elpwunsn  4581  elsuci  6225  infxpenlem  9424  fin1a2lem12  9822  fin1a2  9826  entri3  9970  zindd  12071  elfzr  13145  hashnn0pnf  13698  limccnp  24494  tgldimor  26296  ex-natded5.7-2  28197  chirredi  30177  meran1  33872  dissym1  33882  ordtoplem  33896  ordcmp  33908  poimirlem31  35088  simpcntrab  43484