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  3173  elpwunsn  4629  elsuci  6386  infxpenlem  9926  fin1a2lem12  10324  fin1a2  10328  entri3  10472  zindd  12621  elfzr  13727  hashnn0pnf  14295  limccnp  25868  tgldimor  28584  ex-natded5.7-2  30497  chirredi  32480  meran1  36609  dissym1  36619  ordtoplem  36633  ordcmp  36645  poimirlem31  37986  simpcntrab  47316  setc2othin  49953