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  3192  elpwunsn  4689  elsuci  6453  infxpenlem  10051  fin1a2lem12  10449  fin1a2  10453  entri3  10597  zindd  12717  elfzr  13816  hashnn0pnf  14378  limccnp  25941  tgldimor  28525  ex-natded5.7-2  30441  chirredi  32423  meran1  36394  dissym1  36404  ordtoplem  36418  ordcmp  36430  poimirlem31  37638  simpcntrab  46826  setc2othin  48857