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  5074  relcoi2  5212  tfrlemi14d  6418  tfri1dALT  6436  mapsncnv  6781  findcard2d  6987  findcard2sd  6988  ac6sfi  6994  xpfi  7028  fifo  7081  updjudhcoinlf  7181  updjudhcoinrg  7182  updjud  7183  casefun  7186  omp1eomlem  7195  difinfsnlem  7200  djufun  7205  ctm  7210  ismkvnex  7256  cauappcvgprlemladd  7770  caucvgprprlemmu  7807  caucvgsrlemfv  7903  recidpirqlemcalc  7969  recidpirq  7970  axaddf  7980  axmulf  7981  xaddpnf1  9967  fldiv4lem1div2  10448  q0mod  10498  q1mod  10499  mulp1mod1  10508  m1modnnsub1  10513  modqm1p1mod0  10518  modqltm1p1mod  10519  bcval5  10906  negfi  11481  xrmaxadd  11514  fprodle  11893  fprodmodd  11894  ege2le3  11924  sinltxirr  12014  p1modz1  12047  moddvds  12052  fsumdvds  12095  oddnn02np1  12133  oddge22np1  12134  evennn02n  12135  evennn2n  12136  bitsinv1lem  12214  3lcm2e6woprm  12350  6lcm4e12  12351  isprm6  12411  sqrt2irraplemnn  12443  fermltl  12498  phisum  12505  odzdvds  12510  reumodprminv  12518  pceu  12560  pcaddlem  12604  pcadd  12605  modxai  12681  modsubi  12684  ennnfonelemp1  12719  ennnfonelemkh  12725  ennnfonelemex  12727  exmidunben  12739  ssomct  12758  ssnnctlemct  12759  strslfv  12819  strleund  12877  prdsval  13047  prdsidlem  13221  pws0g  13225  idmhm  13243  mulgneg2  13434  gsumfzfsumlemm  14291  dvdsrzring  14307  expghmap  14311  zndvds  14353  cnbl0  14948  negfcncf  15020  cnrehmeocntop  15024  divcncfap  15028  dvidlemap  15105  dvidrelem  15106  dvidsslem  15107  dvid  15109  dvidre  15111  dvmulxxbr  15116  dvexp  15125  plycjlemc  15174  plycj  15175  dvply1  15179  dvply2g  15180  sincn  15183  coscn  15184  coseq0q4123  15248  tangtx  15252  cosordlem  15263  wilthlem1  15394  1sgm2ppw  15409  perfectlem2  15414  lgslem1  15419  lgsvalmod  15438  lgsmod  15445  lgsdir2lem5  15451  lgsne0  15457  gausslemma2d  15488  lgseisenlem4  15492  lgseisen  15493  lgsquad2lem1  15500  lgsquad3  15503  2lgslem3a1  15516  2lgslem3b1  15517  2lgslem3c1  15518  2lgslem3d1  15519  pwf1oexmid  15869  nninfsellemdc  15880  trilpolemlt1  15913  apdiff  15920  iswomninnlem  15921