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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6

This theorem is used by:  poirr2  5183  relcoi2  5321  supp0  6482  tfrlemi14d  6608  tfri1dALT  6626  mapsncnv  6981  findcard2d  7199  findcard2sd  7200  ac6sfi  7206  xpfi  7243  fifo  7319  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  casefun  7431  omp1eomlem  7440  difinfsnlem  7445  djufun  7450  ctm  7455  ismkvnex  7501  cauappcvgprlemladd  8031  caucvgprprlemmu  8068  caucvgsrlemfv  8164  recidpirqlemcalc  8230  recidpirq  8231  axaddf  8241  axmulf  8242  xaddpnf1  10265  fldiv4lem1div2  10763  q0mod  10813  q1mod  10814  mulp1mod1  10823  m1modnnsub1  10828  modqm1p1mod0  10833  modqltm1p1mod  10834  bcval5  11223  hashmap  11290  swrd0g  11454  negfi  12017  xrmaxadd  12052  fprodle  12432  fprodmodd  12433  ege2le3  12463  sinltxirr  12553  p1modz1  12586  moddvds  12591  fsumdvds  12634  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  bitsinv1lem  12753  3lcm2e6woprm  12889  6lcm4e12  12890  isprm6  12951  sqrt2irraplemnn  12984  nn0sqdcq  13013  fermltl  13041  phisum  13048  odzdvds  13053  reumodprminv  13061  pceu  13103  pcaddlem  13147  pcadd  13148  modxai  13224  modsubi  13228  prmlem0  13249  ballotfilemofi  13277  ballotfilem2  13286  ballotfilemfmpn  13292  ballotfilem1ri  13336  ennnfonelemp1  13355  ennnfonelemkh  13361  ennnfonelemex  13363  exmidunben  13375  ssomct  13394  ssnnctlemct  13395  strslfv  13455  strleund  13516  idmhm  13835  mulgneg2  14018  gsumzfi  14248  gsum2dfilem2  14272  prdsval  14280  prdsidlem  14300  pws0g  14320  dvdsrzring  15047  expghmap  15051  zndvds  15093  psrlidmfi  15199  cnbl0  15760  negfcncf  15832  cnrehmeocntop  15836  divcncfap  15840  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvid  15921  dvidre  15923  dvmulxxbr  15928  dvexp  15937  plycjlemc  15986  plycj  15987  dvply1  15991  dvply2g  15992  sincn  15995  coscn  15996  coseq0q4123  16061  tangtx  16065  cosordlem  16077  log2tlbndlog2  16220  wilthlem1  16232  chtqrpcl  16279  1sgm2ppw  16289  perfectlem2  16300  bposlem7  16317  lgslem1  16324  lgsvalmod  16343  lgsmod  16350  lgsdir2lem5  16356  lgsne0  16362  gausslemma2d  16393  lgseisenlem4  16397  lgseisen  16398  lgsquad2lem1  16405  lgsquad3  16408  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  uspgr2wlkeq  16811  konigsberglem2  16935  pwf1oexmid  17234  nninfsellemdc  17259  trilpolemlt1  17297  apdiff  17304  qdiff  17305  iswomninnlem  17306