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  4651  elsuci  6432  infxpenlem  9998  fin1a2lem12  10396  fin1a2  10400  entri3  10544  zindd  12698  elfzr  13812  hashnn0pnf  14380  limccnp  26031  tgldimor  28749  ex-natded5.7-2  30741  chirredi  32724  meran1  36900  dissym1  36910  ordtoplem  36924  ordcmp  36936  poimirlem31  38280  simpcntrab  47564  setc2othin  50221