Theorem orim2i 768

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 766	1 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  769  pm1.5  772  pm2.3  782  ordi  823  dcn  849  pm2.25dc  900  dcand  940  axi12  1562  dveeq2or  1864  equs5or  1878  sb4or  1881  sb4bor  1883  nfsb2or  1885  sbequilem  1886  sbequi  1887  sbal1yz  2054  dvelimor  2071  exmodc  2130  r19.44av  2692  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  elsuci  4500  acexmidlemcase  6013  undifdcss  7115  updjudhf  7278  ctssdccl  7310  zindd  9598  fiubm  11093  lswex  11169  fsumsplitsn  11989  fprodcllem  12185  fprodsplitsn  12212  gsumwsubmcl  13597  gsumwmhm  13599  subctctexmid  16652