Theorem orim2i 921

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 22	. 2 ⊢ (𝜒 → 𝜒)
2		orim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	orim12i 919	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-or 859

This theorem is referenced by:  orbi2i  923  pm1.5  930  pm2.3  935  r19.44v  3196  elpwunsn  4642  elsuci  6411  infxpenlem  9966  fin1a2lem12  10365  fin1a2  10369  entri3  10513  zindd  12671  elfzr  13784  hashnn0pnf  14352  limccnp  25933  tgldimor  28648  ex-natded5.7-2  30560  chirredi  32543  meran1  36735  dissym1  36745  ordtoplem  36759  ordcmp  36771  poimirlem31  38114  simpcntrab  47408  setc2othin  50051