Theorem orim2i 924

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 922	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi2i  926  pm1.5  933  pm2.3  938  r19.44v  3197  elpwunsn  4641  elsuci  6432  infxpenlem  10095  fin1a2lem12  10492  fin1a2  10496  entri3  10646  zindd  12803  elfzr  13919  hashnn0pnf  14489  limccnp  26216  tgldimor  28970  ex-natded5.7-2  31018  chirredi  33001  rankse  35793  r0maxss  35942  meran1  37291  dissym1  37301  ordtoplem  37315  ordcmp  37327  poimirlem31  38662  simpcntrab  47973  setc2othin  50694