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  3167  elpwunsn  4637  elsuci  6375  infxpenlem  9901  fin1a2lem12  10299  fin1a2  10303  entri3  10447  zindd  12571  elfzr  13678  hashnn0pnf  14246  limccnp  25817  tgldimor  28478  ex-natded5.7-2  30387  chirredi  32369  meran1  36444  dissym1  36454  ordtoplem  36468  ordcmp  36480  poimirlem31  37690  simpcntrab  46907  setc2othin  49497