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  3207  elpwunsn  4655  elsuci  6434  infxpenlem  10000  fin1a2lem12  10398  fin1a2  10402  entri3  10546  zindd  12700  elfzr  13813  hashnn0pnf  14381  limccnp  26033  tgldimor  28751  ex-natded5.7-2  30733  chirredi  32716  meran1  36870  dissym1  36880  ordtoplem  36894  ordcmp  36906  poimirlem31  38250  simpcntrab  47536  setc2othin  50193