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  3171  elpwunsn  4641  elsuci  6386  infxpenlem  9923  fin1a2lem12  10321  fin1a2  10325  entri3  10469  zindd  12593  elfzr  13697  hashnn0pnf  14265  limccnp  25848  tgldimor  28574  ex-natded5.7-2  30487  chirredi  32469  meran1  36605  dissym1  36615  ordtoplem  36629  ordcmp  36641  poimirlem31  37848  simpcntrab  47110  setc2othin  49707