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  4239  exmidundifim  4240  exmid1stab  4241  elsuci  4438  acexmidlemcase  5917  undifdcss  6984  updjudhf  7145  ctssdccl  7177  zindd  9444  fiubm  10920  fsumsplitsn  11575  fprodcllem  11771  fprodsplitsn  11798  gsumwsubmcl  13128  gsumwmhm  13130  subctctexmid  15645