Theorem orim2i 761

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

Syntax hints:   → wi 4   ∨ wo 708

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  762  pm1.5  765  pm2.3  775  ordi  816  dcn  842  pm2.25dc  893  dcan  933  axi12  1514  dveeq2or  1816  equs5or  1830  sb4or  1833  sb4bor  1835  nfsb2or  1837  sbequilem  1838  sbequi  1839  sbal1yz  2001  dvelimor  2018  exmodc  2076  r19.44av  2636  exmidundif  4205  exmidundifim  4206  exmid1stab  4207  elsuci  4402  acexmidlemcase  5867  undifdcss  6919  updjudhf  7075  ctssdccl  7107  zindd  9367  fiubm  10801  fsumsplitsn  11411  fprodcllem  11607  fprodsplitsn  11634  subctctexmid  14610