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  5121  relcoi2  5259  tfrlemi14d  6485  tfri1dALT  6503  mapsncnv  6850  findcard2d  7061  findcard2sd  7062  ac6sfi  7068  xpfi  7105  fifo  7158  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  casefun  7263  omp1eomlem  7272  difinfsnlem  7277  djufun  7282  ctm  7287  ismkvnex  7333  cauappcvgprlemladd  7856  caucvgprprlemmu  7893  caucvgsrlemfv  7989  recidpirqlemcalc  8055  recidpirq  8056  axaddf  8066  axmulf  8067  xaddpnf1  10054  fldiv4lem1div2  10539  q0mod  10589  q1mod  10590  mulp1mod1  10599  m1modnnsub1  10604  modqm1p1mod0  10609  modqltm1p1mod  10610  bcval5  10997  swrd0g  11207  negfi  11754  xrmaxadd  11787  fprodle  12166  fprodmodd  12167  ege2le3  12197  sinltxirr  12287  p1modz1  12320  moddvds  12325  fsumdvds  12368  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  bitsinv1lem  12487  3lcm2e6woprm  12623  6lcm4e12  12624  isprm6  12684  sqrt2irraplemnn  12716  fermltl  12771  phisum  12778  odzdvds  12783  reumodprminv  12791  pceu  12833  pcaddlem  12877  pcadd  12878  modxai  12954  modsubi  12957  ennnfonelemp1  12992  ennnfonelemkh  12998  ennnfonelemex  13000  exmidunben  13012  ssomct  13031  ssnnctlemct  13032  strslfv  13092  strleund  13151  prdsval  13321  prdsidlem  13495  pws0g  13499  idmhm  13517  mulgneg2  13708  gsumfzfsumlemm  14566  dvdsrzring  14582  expghmap  14586  zndvds  14628  cnbl0  15223  negfcncf  15295  cnrehmeocntop  15299  divcncfap  15303  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvid  15384  dvidre  15386  dvmulxxbr  15391  dvexp  15400  plycjlemc  15449  plycj  15450  dvply1  15454  dvply2g  15455  sincn  15458  coscn  15459  coseq0q4123  15523  tangtx  15527  cosordlem  15538  wilthlem1  15669  1sgm2ppw  15684  perfectlem2  15689  lgslem1  15694  lgsvalmod  15713  lgsmod  15720  lgsdir2lem5  15726  lgsne0  15732  gausslemma2d  15763  lgseisenlem4  15767  lgseisen  15768  lgsquad2lem1  15775  lgsquad3  15778  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgslem3d1  15794  uspgr2wlkeq  16106  pwf1oexmid  16424  nninfsellemdc  16436  trilpolemlt1  16469  apdiff  16476  iswomninnlem  16477