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  3201  elpwunsn  4645  elsuci  6453  infxpenlem  10122  fin1a2lem12  10519  fin1a2  10523  entri3  10673  zindd  12830  elfzr  13946  hashnn0pnf  14516  limccnp  26244  tgldimor  28998  ex-natded5.7-2  31046  chirredi  33029  rankse  35836  r0maxss  36016  meran1  37390  dissym1  37400  ordtoplem  37414  ordcmp  37426  poimirlem31  38774  simpcntrab  48095  setc2othin  50816