Theorem orim2i 750

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 19	. 2 ⊢ (𝜒 → 𝜒)
2		orim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	orim12i 748	1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi2i  751  pm1.5  754  pm2.3  764  ordi  805  dcn  827  pm2.25dc  878  dcan  918  axi12  1494  dveeq2or  1788  equs5or  1802  sb4or  1805  sb4bor  1807  nfsb2or  1809  sbequilem  1810  sbequi  1811  sbal1yz  1974  dvelimor  1991  exmodc  2047  r19.44av  2588  exmidundif  4124  exmidundifim  4125  elsuci  4320  acexmidlemcase  5762  undifdcss  6804  updjudhf  6957  ctssdccl  6989  zindd  9162  fsumsplitsn  11172  exmid1stab  13184  subctctexmid  13185