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  3164  elpwunsn  4638  elsuci  6380  infxpenlem  9926  fin1a2lem12  10324  fin1a2  10328  entri3  10472  zindd  12595  elfzr  13701  hashnn0pnf  14267  limccnp  25808  tgldimor  28465  ex-natded5.7-2  30374  chirredi  32356  meran1  36384  dissym1  36394  ordtoplem  36408  ordcmp  36420  poimirlem31  37630  simpcntrab  46852  setc2othin  49452