Theorem orim2i 762

Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)

Hypothesis

Ref	Expression
orim1i.1	|- ( ph -> ps )

Assertion

Ref	Expression
orim2i	|- ( ( ch \/ ph ) -> ( ch \/ ps ) )

Proof of Theorem orim2i

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2		orim1i.1	. 2 |- ( ph -> ps )
3	1, 2	orim12i 760	1 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  763  pm1.5  766  pm2.3  776  ordi  817  dcn  843  pm2.25dc  894  dcand  934  axi12  1528  dveeq2or  1830  equs5or  1844  sb4or  1847  sb4bor  1849  nfsb2or  1851  sbequilem  1852  sbequi  1853  sbal1yz  2020  dvelimor  2037  exmodc  2095  r19.44av  2656  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  elsuci  4439  acexmidlemcase  5920  undifdcss  6993  updjudhf  7154  ctssdccl  7186  zindd  9461  fiubm  10937  fsumsplitsn  11592  fprodcllem  11788  fprodsplitsn  11815  gsumwsubmcl  13198  gsumwmhm  13200  subctctexmid  15731