Theorem orim2i 911

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

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  orbi2i  913  pm1.5  920  pm2.3  925  r19.44v  3172  elpwunsn  4628  elsuci  6392  infxpenlem  9935  fin1a2lem12  10333  fin1a2  10337  entri3  10481  zindd  12630  elfzr  13736  hashnn0pnf  14304  limccnp  25858  tgldimor  28570  ex-natded5.7-2  30482  chirredi  32465  meran1  36593  dissym1  36603  ordtoplem  36617  ordcmp  36629  poimirlem31  37972  simpcntrab  47298  setc2othin  49941