Theorem orim2i 911

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  orbi2i  913  pm1.5  920  pm2.3  925  r19.44v  3173  elpwunsn  4643  elsuci  6394  infxpenlem  9935  fin1a2lem12  10333  fin1a2  10337  entri3  10481  zindd  12605  elfzr  13709  hashnn0pnf  14277  limccnp  25860  tgldimor  28586  ex-natded5.7-2  30499  chirredi  32481  meran1  36624  dissym1  36634  ordtoplem  36648  ordcmp  36660  poimirlem31  37896  simpcntrab  47222  setc2othin  49819