Theorem orim2i 909

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  orbi2i  911  pm1.5  918  pm2.3  923  r19.44v  3200  elpwunsn  4707  elsuci  6462  infxpenlem  10082  fin1a2lem12  10480  fin1a2  10484  entri3  10628  zindd  12744  elfzr  13830  hashnn0pnf  14391  limccnp  25946  tgldimor  28528  ex-natded5.7-2  30444  chirredi  32426  meran1  36377  dissym1  36387  ordtoplem  36401  ordcmp  36413  poimirlem31  37611  simpcntrab  46791  setc2othin  48723