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  1536  dveeq2or  1838  equs5or  1852  sb4or  1855  sb4bor  1857  nfsb2or  1859  sbequilem  1860  sbequi  1861  sbal1yz  2028  dvelimor  2045  exmodc  2103  r19.44av  2664  exmidundif  4249  exmidundifim  4250  exmid1stab  4251  elsuci  4449  acexmidlemcase  5938  undifdcss  7019  updjudhf  7180  ctssdccl  7212  zindd  9490  fiubm  10971  fsumsplitsn  11692  fprodcllem  11888  fprodsplitsn  11915  gsumwsubmcl  13299  gsumwmhm  13301  subctctexmid  15899