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  3168  elpwunsn  4636  elsuci  6380  infxpenlem  9911  fin1a2lem12  10309  fin1a2  10313  entri3  10457  zindd  12580  elfzr  13683  hashnn0pnf  14251  limccnp  25820  tgldimor  28481  ex-natded5.7-2  30394  chirredi  32376  meran1  36476  dissym1  36486  ordtoplem  36500  ordcmp  36512  poimirlem31  37711  simpcntrab  46992  setc2othin  49591