Theorem orim2i 923

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 23	. 2 ⊢ (𝜒 → 𝜒)
2		orim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	orim12i 921	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi2i  925  pm1.5  932  pm2.3  937  r19.44v  3200  elpwunsn  4646  elsuci  6419  infxpenlem  9985  fin1a2lem12  10383  fin1a2  10387  entri3  10531  zindd  12688  elfzr  13801  hashnn0pnf  14369  limccnp  26011  tgldimor  28729  ex-natded5.7-2  30672  chirredi  32655  meran1  36784  dissym1  36794  ordtoplem  36808  ordcmp  36820  poimirlem31  38162  simpcntrab  47442  setc2othin  50095