MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp1i Structured version   Unicode version

Theorem mp1i 12
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
StepHypRef Expression
1 mp1i.a . . 3  |-  ph
2 mp1i.b . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 5 . 2  |-  ps
43a1i 11 1  |-  ( ch 
->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6
This theorem is referenced by:  poirr2  5304  relcoi2  5443  fvrnressn  5988  isomin  6134  isoini  6135  supp0  6822  suppval1  6823  suppssr  6849  dmtpos  6885  mpt2curryd  6916  oaabs2  7212  mapsncnv  7384  boxcutc  7431  domunsncan  7536  pw2f1o  7541  unxpdom2  7644  sucxpdom  7645  findcard2d  7677  ac6sfi  7679  xpfi  7706  imafi  7728  snopfsupp  7767  fifo  7807  ordtypelem4  7861  oismo  7880  wofib  7885  brwdom2  7914  canthwdom  7920  cantnffvalOLD  7995  cantnfval  8000  cantnflt  8004  cantnff  8006  cantnf0  8007  cantnfp1lem1  8010  cantnfp1lem3  8012  cantnflem1b  8018  cantnflem1  8021  cantnfltOLD  8034  cantnfp1lem1OLD  8036  cantnfp1lem3OLD  8038  cantnflem1bOLD  8041  cantnflem1dOLD  8043  cantnflem1OLD  8044  cnfcom  8057  cnfcom2lem  8058  cnfcomOLD  8065  cnfcom2lemOLD  8066  ranksnb  8158  tskwe  8244  cardidm  8253  infxpenc  8308  infxpencOLD  8313  fseqdom  8320  dfac8clem  8326  dfac12lem2  8437  infmap2  8511  isfin4-3  8608  fin23lem14  8626  fin23lem40  8644  isf34lem7  8672  isf34lem6  8673  fin1a2lem12  8704  hsmexlem4  8722  hsmexlem5  8723  ac5b  8771  alephexp1  8867  alephsuc3  8868  fpwwe2lem8  8926  fpwwe2lem13  8931  canthwe  8940  canthp1lem2  8942  gchcda1  8945  pwfseqlem5  8952  wunco  9022  prlem934  9322  supsrlem  9399  msqge0  9991  ofnegsub  10450  ofsubge0  10451  xaddpnf1  11346  supxrmnf  11430  injresinjlem  11824  uzindi  11994  seqfeq4  12059  seqof  12067  bcval5  12298  hashdomi  12351  hash1snb  12383  brfi1uzind  12436  ccatlen  12503  lswccatn0lsw  12516  eqs1  12530  s111  12532  swrd0  12570  swrdspsleq  12585  wrdeqs1cat  12611  reps  12653  repsw0  12660  repswccat  12668  repswrevw  12669  lswcshw  12694  cshwsexa  12703  scshwfzeqfzo  12705  wrdlen2i  12795  relexpsucnnr  12862  relexpaddg  12888  shftfib  12907  limsupcl  13298  limsupgf  13300  limsupval2  13305  isercolllem3  13491  modfsummods  13609  ackbijnn  13642  supcvg  13669  fprodfac  13779  ege2le3  13827  rpnnen2lem5  13954  ruclem11  13975  fsumdvds  14031  bitsinv2  14095  sadaddlem  14118  smupf  14130  smup0  14131  smu01lem  14137  isprm6  14252  hashdvds  14307  reumodprminv  14331  prmreclem6  14441  vdwlem13  14513  ramtlecl  14520  0ram  14540  cshwshashnsame  14590  prmlem0  14593  wunndx  14650  prdsval  14862  xpsbas  14981  xpsadd  14983  xpsmul  14984  xpssca  14985  xpsvsca  14986  xpsless  14987  xpsle  14988  mreexexlem2d  15052  mreacs  15065  acsfn  15066  isofn  15181  ciclcl  15208  cicrcl  15209  cicsym  15210  cicer  15212  idfu2nd  15283  idfucl  15287  fucsect  15378  initoeu2lem1  15410  initoeu2lem2  15411  setccatid  15480  setcepi  15484  catchomfval  15494  estrccatid  15518  estrreslem1  15523  estrreslem2  15524  estrres  15525  funcestrcsetclem8  15533  fullestrcsetc  15537  embedsetcestrclem  15543  funcsetcestrclem8  15548  uncfval  15620  oduglb  15886  odumeet  15887  odulub  15888  odujoin  15889  isipodrs  15908  fpwipodrs  15911  isacs4lem  15915  isacs5lem  15916  idmhm  16092  submacs  16113  frmdup1  16149  mgmnsgrpex  16166  mulgneg2  16286  subgacs  16353  nsgacs  16354  idrespermg  16553  psgnunilem5  16636  psgnsn  16662  odf1o2  16710  frgpuplem  16907  cygctb  17011  gsumzunsnd  17096  gsum2dlem2  17112  gsum2dOLD  17114  gsummptnn0fz  17127  dprdsubg  17184  dmdprdsplit2lem  17207  dmdprdpr  17211  dprdpr  17212  dpjeq  17221  dpjeqOLD  17228  ablfac1eulem  17236  pgpfac1lem2  17239  pgpfaclem1  17245  srgbinomlem4  17307  unitgrp  17429  isirred  17461  brric  17506  mptscmfsupp0  17689  lssacs  17726  pwssplit1  17818  lbsextlem2  17918  lbsextlem3  17919  isnzr2hash  18025  0ring01eqbi  18034  rng1nnzr  18035  psrass1lem  18142  psrlidm  18169  psrlidmOLD  18170  resspsradd  18184  resspsrmul  18185  resspsrvsca  18186  mplcoe5lem  18243  ltbwe  18250  coe1fsupp  18367  psropprmul  18392  coe1add  18418  coe1mul2lem1  18421  coe1tm  18427  cply1coe0bi  18455  evls1rhmlem  18471  evl1sca  18483  evl1var  18485  pf1mpf  18501  pf1ind  18504  xrsmcmn  18554  xrs1mnd  18569  xrs10  18570  gsumfsum  18597  zringlpir  18618  zringcyg  18619  zndvds  18679  regsumsupp  18749  uvcvv1  18909  lsslinds  18951  matmulr  19025  ofco2  19038  mat0dimbas0  19053  mat1dimelbas  19058  mat1f1o  19065  dmatval  19079  scmatghm  19120  mavmul0  19139  mavmul0g  19140  m1detdiag  19184  mdetunilem9  19207  maducoeval2  19227  madugsum  19230  smadiadetlem0  19248  smadiadetlem1a  19250  smadiadetlem4  19256  smadiadetglem1  19258  smadiadetglem2  19259  smadiadetg  19260  cramer0  19277  cpmat  19295  mat2pmatfval  19309  cpm2mfval  19335  m2cpminvid2lem  19340  pmatcollpw3fi1lem2  19373  pmatcollpw3fi1  19374  idpm2idmp  19387  pm2mpmhmlem2  19405  chpmatfval  19416  chfacfscmulfsupp  19445  chfacfpmmulfsupp  19449  cpmidpmatlem2  19457  cpmadugsumlemF  19462  cpmidgsum2  19465  cpmadumatpolylem1  19467  cayhamlem3  19473  cayhamlem4  19474  indistopon  19587  mreclatdemoBAD  19683  mnfnei  19808  resthauslem  19950  sshauslem  19959  discmp  19984  conima  20011  1stcfb  20031  hauseqlcld  20232  xkoptsub  20240  xkofvcn  20270  idqtop  20292  tgqtop  20298  kqdisj  20318  xpstopnlem1  20395  xpstopnlem2  20397  ufildom1  20512  alexsubb  20631  alexsubALTlem3  20634  ptcmplem2  20638  ptcmplem3  20639  tmdgsum  20679  ustneism  20811  ustuqtop1  20829  iducn  20871  prdsmet  20958  imasdsf1olem  20961  xpsxmet  20968  xpsdsval  20969  xpsmet  20970  prdsbl  21079  met1stc  21109  prdsxmslem2  21117  xpsxms  21122  xpsms  21123  psmetutop  21171  dscmet  21178  nmoffn  21303  nmofval  21306  nmolb  21309  nmof  21311  cnbl0  21366  xrsmopn  21402  xrge0gsumle  21423  xrge0tsms  21424  negfcncf  21508  cnrehmeo  21538  lebnum  21549  xlebnum  21550  reparphti  21582  pcopt  21607  pcopt2  21608  pcorevcl  21610  pcorevlem  21611  pi1xfrval  21639  pi1xfrcnvlem  21641  pi1xfrcnv  21642  pi1cof  21644  pi1coval  21645  nmhmcn  21688  cphsubrglem  21709  csscld  21774  cmetcaulem  21812  cmpcmet  21841  ovolunlem1  21993  ovolicc2lem4  22016  ioovolcl  22064  ioorcl2  22066  uniioovol  22073  uniioombllem4  22080  uniioombllem5  22081  uniioombllem6  22082  dyadmbllem  22093  mbfsub  22154  itg1climres  22206  xrge0f  22223  itg2ge0  22227  itg2i1fseq2  22248  ibl0  22278  ellimc2  22366  limcflf  22370  dvreslem  22398  dvidlem  22404  dvid  22406  cpnres  22425  dvaddbr  22426  dvmulbr  22427  dvfre  22439  dvexp  22441  dvrec  22443  dvmptid  22445  dvmptc  22446  dvmptntr  22459  dvexp3  22464  dvlipcn  22480  dveq0  22486  dv11cn  22487  lhop2  22501  ftc1a  22523  tdeglem1  22541  tdeglem3  22542  tdeglem4  22543  tdeglem2  22544  mdeg0  22555  mdegle0  22562  ply1remlem  22648  fta1glem2  22652  plypf1  22694  coe0  22738  dvply1  22765  elqaalem3  22802  aaliou2b  22822  aaliou3lem8  22826  aaliou3lem7  22830  taylfvallem  22838  taylf  22841  tayl0  22842  taylpfval  22845  taylply  22849  dvtaylp  22850  taylthlem1  22853  taylthlem2  22854  ulmdvlem1  22880  ulmdvlem2  22881  ulmdvlem3  22882  radcnvcl  22897  psercnlem2  22904  psercn  22906  pserdv  22909  abelthlem3  22913  abelth  22921  sincn  22924  coscn  22925  reefgim  22930  tangtx  22983  pige3  22995  cosordlem  23003  logcn  23115  dvlog  23119  advlog  23122  advlogexp  23123  logtayl  23128  logccv  23131  dvcxp1  23203  cxpcn3lem  23208  cxpcn3  23209  resqrtcn  23210  sqrtcn  23211  loglesqrt  23219  logbfval  23248  logblog  23250  isosctrlem2  23269  dquartlem1  23298  quart  23308  atancj  23357  efiatan  23359  atantan  23370  atanbndlem  23372  atansopn  23379  dvatan  23382  atantayl  23384  leibpilem2  23388  leibpi  23389  log2tlbnd  23392  rlimcnp2  23413  efrlim  23416  divsqrtsumlem  23426  jensenlem1  23433  jensenlem2  23434  jensen  23435  amgmlem  23436  amgm  23437  emcllem4  23445  emcllem7  23448  wilthlem2  23460  wilthlem3  23461  basellem6  23476  chtrpcl  23566  ppiltx  23568  1sgm2ppw  23592  chtlepsi  23598  chpub  23612  logfacbnd3  23615  logfacrlim  23616  perfectlem2  23622  dchrelbas2  23629  dchrabs  23652  dchrhash  23663  bposlem7  23682  lgsdir2lem5  23719  lgsqrlem1  23733  lgseisenlem4  23744  lgsquad2lem1  23750  lgsquad3  23753  chpo1ub  23782  vmadivsumb  23785  rpvmasumlem  23789  dchrisumlem2  23792  dchrmusumlema  23795  dchrvmasumlem2  23800  dchrvmasumlema  23802  dchrvmasumiflem1  23803  dchrisum0flblem1  23810  dchrisum0lem1  23818  rplogsum  23829  mudivsum  23832  logdivsum  23835  mulog2sumlem2  23837  vmalogdivsum2  23840  2vmadivsumlem  23842  log2sumbnd  23846  selberglem2  23848  selbergb  23851  selberg2lem  23852  selberg2b  23854  selberg3lem1  23859  selberg4lem1  23862  selberg4  23863  pntrsumo1  23867  pntrlog2bndlem2  23880  pntrlog2bndlem3  23881  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  pntibndlem1  23891  pntibndlem2  23893  pntibndlem3  23894  pntlemb  23899  pntlemr  23904  pntlemf  23907  pntlem3  23911  pnt  23916  qabvle  23927  padicabv  23932  ostth1  23935  istrkg2ld  23975  tgldimor  24013  motgrp  24050  perpln1  24207  perpln2  24208  isperp  24209  uhgrares  24429  umgrares  24445  edgopval  24461  usgrares  24490  nbgraop  24544  nbgraopALT  24545  nbgraf1o0  24567  cusgra0v  24581  cusgra1v  24582  cusgraexilem2  24588  sizeusglecusg  24607  isuvtx  24609  2trllemH  24675  wlkntrllem3  24684  2wlklem1  24720  usgra2wlkspthlem1  24740  usgra2wlkspthlem2  24741  constr3trllem3  24773  constr3pthlem3  24778  wwlkn  24803  wlkiswwlk2  24818  wwlkn0s  24826  usg2wlkeq  24829  wwlkexthasheq  24855  wlknwwlknvbij  24861  clwwlkn  24888  clwwlkn2  24896  clwlkisclwwlklem2  24907  clwwlkvbij  24922  eclclwwlkn0  24952  hashecclwwlkn1  24955  usghashecclwwlk  24956  vdgr0  25021  rusgrasn  25066  eupatrl  25089  eupares  25096  vdegp1ai  25105  vdegp1bi  25106  frgra3v  25123  frgrancvvdeqlem9  25162  frgrancvvdgeq  25164  frg2wot1  25178  usgreghash2spotv  25187  extwwlkfablem2  25199  numclwwlkovf2  25205  numclwwlk2lem3  25227  vsfval  25645  ipasslem7  25868  minvecolem2  25908  h2hcau  26013  h2hlm  26014  hlimadd  26227  hhsscms  26312  chocunii  26336  occllem  26338  leopnmid  27173  opsqrlem1  27175  hmopidmchi  27186  mdslj1i  27354  addltmulALT  27482  imadifxp  27591  xaddeq0  27723  xrge0npcan  27837  gsumle  27923  xrge0tsmsd  27929  locfinreflem  27997  locfinref  27998  xpinpreima2  28043  cnre2csqlem  28046  tpr2rico  28048  ordtrestNEW  28057  ordtrest2NEW  28059  mndpluscn  28062  pnfneige0  28087  qqhghm  28122  qqhrhm  28123  qqhcn  28125  qqhucn  28126  rrhcn  28131  rrhre  28152  esumsplit  28201  esumpr  28214  esumfsup  28218  sigaclcu2  28269  pwsiga  28279  prsiga  28280  sigapildsys  28307  measvuni  28341  elmbfmvol2  28394  mbfmcnt  28395  sxbrsigalem1  28412  sxbrsiga  28417  omsfval  28421  carsgclctunlem2  28446  sibf0  28459  sitgclg  28467  sitmval  28473  eulerpartgbij  28494  eulerpartlemgh  28500  isrrvv  28565  rrvadd  28574  rrvmulc  28575  dstrvprob  28593  coinflipspace  28602  coinfliprv  28604  ballotlemfmpn  28616  ballotlem1ri  28656  sgnmulsgn  28671  plymul02  28686  signsplypnf  28690  signsply0  28691  signswrid  28698  lgamcvg2  28786  gamcvg2lem  28790  indispcon  28868  conpcon  28869  iccllyscon  28884  cvmopnlem  28912  cvmliftlem15  28932  cvmlift2lem3  28939  mrsubff  29061  mrsubccat  29067  circum  29229  fallfac0  29316  bpoly4  29974  elhf2  29985  finixpnum  30203  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  dvtan  30231  itg2addnclem  30232  ftc1anclem5  30260  dvcncxp1  30266  dvasin  30269  dvreasin  30271  dvreacos  30272  areacirclem1  30273  areacirc  30278  bnd2lem  30453  prdsbnd  30455  cntotbnd  30458  cnpwstotbnd  30459  isdrngo2  30527  prter2  30788  isnacs3  30808  diophrw  30857  lzenom  30868  diophin  30871  pellexlem5  30934  pw2f1ocnv  31145  dnnumch2  31157  kelac2lem  31176  kelac2  31177  dfac21  31178  pwfi2f1o  31210  pwfi2f1oOLD  31211  frlmpwfi  31214  mpaaeu  31267  rngunsnply  31290  mendbas  31301  mendplusgfval  31302  mendmulrfval  31304  mendsca  31306  mendvscafval  31307  subrgacs  31317  sdrgacs  31318  cntzsdrg  31319  idomodle  31321  phisum  31327  proot1ex  31329  deg1mhm  31335  itgpowd  31350  hashnzfzclim  31395  ofsubid  31397  ofdivrec  31399  dvconstbi  31407  fzisoeu  31666  sumnnodd  31802  negcncfg  31849  cnfdmsn  31850  divcncf  31852  dvmptresicc  31882  itgcoscmulx  31934  stoweidlem13  31961  stoweidlem26  31974  stoweidlem34  31982  stoweidlem42  31990  stoweidlem44  31992  stoweidlem48  31996  stoweidlem62  32010  stoweid  32011  stirlinglem7  32028  stirlinglem11  32032  stirlinglem12  32033  dirkeritg  32050  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem16  32071  fourierdlem21  32076  fourierdlem22  32077  fourierdlem24  32079  fourierdlem48  32103  fourierdlem49  32104  fourierdlem62  32117  fourierdlem70  32125  fourierdlem80  32135  fourierdlem83  32138  fourierdlem85  32140  fourierdlem102  32157  fourierdlem104  32159  fourierdlem111  32166  fourierdlem112  32167  fourierdlem114  32169  etransclem18  32201  etransclem23  32206  etransclem24  32207  etransclem25  32208  etransclem35  32218  etransclem46  32229  mod2eq1n2dvds  32462  perfectALTVlem2  32544  uhgrepe  32696  uhgres  32697  gordopval  32708  gsizopval  32709  usgedgnlp  32728  isfusgracl  32744  isfusgraclALT  32746  usgo0s0  32753  usgo0s0ALT  32754  usgo1s0ALT  32755  usgo1s0  32760  usgresvm1  32761  usgfis  32764  usgresvm1ALT  32765  usgrafiedgALT  32769  idmgmhm  32794  mgmplusgiopALT  32836  sgrp2sgrp  32870  isrnghm  32898  lidlmmgm  32931  2zrngnmlid  32955  dfrngc2  32980  rnghmsscmap2  32981  rnghmsscmap  32982  rngchomfvalALTV  32992  rngcidALTV  32999  funcrngcsetcALT  33007  dfringc2  33026  rhmsscmap2  33027  rhmsscmap  33028  rhmsscrnghm  33034  rngcresringcat  33038  funcringcsetcALTV2lem8  33051  ringchomfvalALTV  33055  ringcidALTV  33062  funcringcsetclem8ALTV  33074  srhmsubc  33084  fldc  33091  rngcrescrhm  33093  rhmsubclem3  33096  srhmsubcALTV  33103  fldcALTV  33110  rngcrescrhmALTV  33112  altgsumbcALT  33142  zlmodzxzel  33144  zlmodzxzsubm  33148  zlmodzxzsub  33149  gsumpr  33150  scmsuppss  33165  ply1mulgsum  33190  dmatALTbas  33202  lcoop  33212  lincval0  33216  lco0  33228  linds0  33266  snlindsntorlem  33271  lmod1lem2  33289  lmod1lem3  33290  lmod1zr  33294  lmod1zrnlvec  33295  zlmodzxznm  33298  zlmodzxzldeplem4  33304  expnegico01  33323  pw2m1lepw2m1  33327  fldivexpfllog2  33386  blennnelnn  33397  blenpw2  33399  nnpw2pmod  33404  blennnt2  33410  nnolog2flm1  33411  digfval  33418  dignnld  33424  dig2nn0ld  33425  0dig2nn0e  33433  0dig2nn0o  33434  eqlkr2  35238  tendoidcl  36908  cdlemk56  37110  dihpN  37476  mapdhval  37864  hlhillcs  38101  relexp01min  38237  trclrelexplem  38247  trclimalb2  38257
  Copyright terms: Public domain W3C validator