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  3198  elpwunsn  4645  elsuci  6425  infxpenlem  10073  fin1a2lem12  10470  fin1a2  10474  entri3  10624  zindd  12781  elfzr  13896  hashnn0pnf  14466  limccnp  26191  tgldimor  28947  ex-natded5.7-2  30995  chirredi  32978  meran1  37169  dissym1  37179  ordtoplem  37193  ordcmp  37205  poimirlem31  38537  simpcntrab  47824  setc2othin  50518