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  1525  dveeq2or  1827  equs5or  1841  sb4or  1844  sb4bor  1846  nfsb2or  1848  sbequilem  1849  sbequi  1850  sbal1yz  2017  dvelimor  2034  exmodc  2092  r19.44av  2653  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  elsuci  4435  acexmidlemcase  5914  undifdcss  6981  updjudhf  7140  ctssdccl  7172  zindd  9438  fiubm  10902  fsumsplitsn  11556  fprodcllem  11752  fprodsplitsn  11779  gsumwsubmcl  13071  gsumwmhm  13073  subctctexmid  15561