Theorem orim2i 910

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

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  orbi2i  912  pm1.5  919  pm2.3  924  r19.44v  3172  elpwunsn  4648  elsuci  6401  infxpenlem  9966  fin1a2lem12  10364  fin1a2  10368  entri3  10512  zindd  12635  elfzr  13741  hashnn0pnf  14307  limccnp  25792  tgldimor  28429  ex-natded5.7-2  30341  chirredi  32323  meran1  36399  dissym1  36409  ordtoplem  36423  ordcmp  36435  poimirlem31  37645  simpcntrab  46868  setc2othin  49455