Theorem mp1i 10

Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)

Hypotheses

Ref	Expression
mp1i.a	|- ph
mp1i.b	|- ( ph -> ps )

Assertion

Ref	Expression
mp1i	|- ( ch -> ps )

Proof of Theorem mp1i

Step	Hyp	Ref	Expression
1		mp1i.a	. . 3 |- ph
2		mp1i.b	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4	3	a1i 9	1 |- ( ch -> ps )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  poirr2  5175  relcoi2  5313  supp0  6468  tfrlemi14d  6594  tfri1dALT  6612  mapsncnv  6967  findcard2d  7185  findcard2sd  7186  ac6sfi  7192  xpfi  7229  fifo  7304  updjudhcoinlf  7410  updjudhcoinrg  7411  updjud  7412  casefun  7415  omp1eomlem  7424  difinfsnlem  7429  djufun  7434  ctm  7439  ismkvnex  7485  cauappcvgprlemladd  8015  caucvgprprlemmu  8052  caucvgsrlemfv  8148  recidpirqlemcalc  8214  recidpirq  8215  axaddf  8225  axmulf  8226  xaddpnf1  10227  fldiv4lem1div2  10720  q0mod  10770  q1mod  10771  mulp1mod1  10780  m1modnnsub1  10785  modqm1p1mod0  10790  modqltm1p1mod  10791  bcval5  11179  hashmap  11246  swrd0g  11410  negfi  11972  xrmaxadd  12005  fprodle  12385  fprodmodd  12386  ege2le3  12416  sinltxirr  12506  p1modz1  12539  moddvds  12544  fsumdvds  12587  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  bitsinv1lem  12706  3lcm2e6woprm  12842  6lcm4e12  12843  isprm6  12903  sqrt2irraplemnn  12935  fermltl  12990  phisum  12997  odzdvds  13002  reumodprminv  13010  pceu  13052  pcaddlem  13096  pcadd  13097  modxai  13173  modsubi  13176  ballotfilemofi  13197  ballotfilem2  13206  ballotfilemfmpn  13212  ballotfilem1ri  13256  ennnfonelemp1  13275  ennnfonelemkh  13281  ennnfonelemex  13283  exmidunben  13295  ssomct  13314  ssnnctlemct  13315  strslfv  13375  strleund  13434  idmhm  13753  mulgneg2  13936  gsumzfi  14135  prdsval  14150  prdsidlem  14170  pws0g  14190  dvdsrzring  14910  expghmap  14914  zndvds  14956  cnbl0  15558  negfcncf  15630  cnrehmeocntop  15634  divcncfap  15638  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvid  15719  dvidre  15721  dvmulxxbr  15726  dvexp  15735  plycjlemc  15784  plycj  15785  dvply1  15789  dvply2g  15790  sincn  15793  coscn  15794  coseq0q4123  15858  tangtx  15862  cosordlem  15873  wilthlem1  16008  1sgm2ppw  16023  perfectlem2  16028  lgslem1  16033  lgsvalmod  16052  lgsmod  16059  lgsdir2lem5  16065  lgsne0  16071  gausslemma2d  16102  lgseisenlem4  16106  lgseisen  16107  lgsquad2lem1  16114  lgsquad3  16117  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  uspgr2wlkeq  16520  konigsberglem2  16644  pwf1oexmid  16943  nninfsellemdc  16958  trilpolemlt1  16995  apdiff  17002  qdiff  17003  iswomninnlem  17004