Theorem orim2i 539

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

Syntax hints:   → wi 4   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  orbi2i  540  pm1.5  543  pm2.3  594  r19.44v  3075  elpwunsn  4171  elsuci  5708  ordnbtwnOLD  5734  infxpenlem  8719  fin1a2lem12  9116  fin1a2  9120  entri3  9260  zindd  11354  hashnn0pnf  12992  limccnp  23461  tgldimor  25197  ex-natded5.7-2  26661  chirredi  28637  meran1  31580  dissym1  31590  ordtoplem  31604  ordcmp  31616  poimirlem31  32610  elfzr  40364