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  3180  elpwunsn  4665  elsuci  6426  infxpenlem  10032  fin1a2lem12  10430  fin1a2  10434  entri3  10578  zindd  12699  elfzr  13801  hashnn0pnf  14365  limccnp  25849  tgldimor  28486  ex-natded5.7-2  30398  chirredi  32380  meran1  36434  dissym1  36444  ordtoplem  36458  ordcmp  36470  poimirlem31  37680  simpcntrab  46879  setc2othin  49332