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  3199  elpwunsn  4648  elsuci  6431  infxpenlem  10020  fin1a2lem12  10417  fin1a2  10421  entri3  10571  zindd  12726  elfzr  13841  hashnn0pnf  14410  limccnp  26125  tgldimor  28852  ex-natded5.7-2  30900  chirredi  32883  meran1  37038  dissym1  37048  ordtoplem  37062  ordcmp  37074  poimirlem31  38408  simpcntrab  47706  setc2othin  50400