Theorem orim2i 910

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 908	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orbi2i  912  pm1.5  919  pm2.3  924  r19.44v  3181  elpwunsn  4664  elsuci  6431  infxpenlem  10035  fin1a2lem12  10433  fin1a2  10437  entri3  10581  zindd  12702  elfzr  13801  hashnn0pnf  14364  limccnp  25863  tgldimor  28447  ex-natded5.7-2  30360  chirredi  32342  meran1  36387  dissym1  36397  ordtoplem  36411  ordcmp  36423  poimirlem31  37633  simpcntrab  46857  setc2othin  49165