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  3193  elpwunsn  4683  elsuci  6450  infxpenlem  10054  fin1a2lem12  10452  fin1a2  10456  entri3  10600  zindd  12721  elfzr  13820  hashnn0pnf  14382  limccnp  25927  tgldimor  28511  ex-natded5.7-2  30432  chirredi  32414  meran1  36413  dissym1  36423  ordtoplem  36437  ordcmp  36449  poimirlem31  37659  simpcntrab  46890  setc2othin  49138