Theorem orim2i 751

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

Syntax hints:   -> wi 4   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi2i  752  pm1.5  755  pm2.3  765  ordi  806  dcn  832  pm2.25dc  883  dcan  923  axi12  1502  dveeq2or  1804  equs5or  1818  sb4or  1821  sb4bor  1823  nfsb2or  1825  sbequilem  1826  sbequi  1827  sbal1yz  1989  dvelimor  2006  exmodc  2064  r19.44av  2625  exmidundif  4185  exmidundifim  4186  elsuci  4381  acexmidlemcase  5837  undifdcss  6888  updjudhf  7044  ctssdccl  7076  zindd  9309  fiubm  10741  fsumsplitsn  11351  fprodcllem  11547  fprodsplitsn  11574  exmid1stab  13880  subctctexmid  13881