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  3203  elpwunsn  4655  elsuci  6437  infxpenlem  10016  fin1a2lem12  10413  fin1a2  10417  entri3  10561  zindd  12715  elfzr  13829  hashnn0pnf  14398  limccnp  26087  tgldimor  28808  ex-natded5.7-2  30800  chirredi  32783  meran1  36963  dissym1  36973  ordtoplem  36987  ordcmp  36999  poimirlem31  38343  simpcntrab  47625  setc2othin  50285