MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptru Structured version   Visualization version   GIF version

Theorem mptru 1660
Description: Eliminate as an antecedent. A proposition implied by is true. This is modus ponens ax-mp 5 when the minor hypothesis is (which holds by tru 1657). (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypothesis
Ref Expression
mptru.1 (⊤ → 𝜑)
Assertion
Ref Expression
mptru 𝜑

Proof of Theorem mptru
StepHypRef Expression
1 tru 1657 . 2
2 mptru.1 . 2 (⊤ → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1653
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 198  df-tru 1656
This theorem is referenced by:  hadbi123i  1705  cadbi123i  1720  nfan  1998  nfbi  2002  spime  2362  nfmo  2579  nfeu  2604  abeq2i  2878  nfceqi  2904  nfeq  2919  nfel  2920  dvelimc  2930  nfral  3092  nfrex  3153  nfreu  3261  nfrmo  3262  nfrab  3271  rabbia2  3336  nfsbc1  3617  nfsbc  3620  sbcbii  3654  nfcsb1  3708  nfcsb  3711  csbeq2i  4156  nfif  4274  nfdisj  4791  nfbr  4858  mpteq12i  4903  ralxfr  5051  reuxfr2  5057  reuxfr  5059  issoi  5231  nfiota  6037  nfriota  6816  nfov  6876  mpt2eq123i  6920  mpt2eq3ia  6922  iseri  7978  nfixp  8136  en2i  8202  en3i  8203  ensymb  8212  entr  8216  djulf1o  8993  djurf1o  8994  r0weon  9090  recmulnq  10043  axcnex  10225  nfneg  10535  negiso  11261  suprzcl2  11984  supxr  12350  xrinf0  12375  cnrecnv  14204  cau3  14394  cbvsum  14724  sum0  14751  ackbijnn  14858  flo1  14884  trireciplem  14892  trirecip  14893  ege2le3  15116  rpnnen2lem3  15241  bitsf1ocnv  15461  prmreclem6  15918  prmrec  15919  modxai  16065  strfvn  16166  strss  16196  xpssca  16518  xpsvsca  16519  mreacs  16598  2oppccomf  16664  mndprop  17597  grpprop  17719  isgrpi  17726  oppgmndb  18062  oppggrpb  18065  efgrelexlemb  18443  ablprop  18484  ringprop  18865  opprringb  18913  rlmbas  19483  rlmplusg  19484  rlm0  19485  rlmsub  19486  rlmmulr  19487  rlmsca2  19489  rlmvsca  19490  rlmtopn  19491  rlmds  19492  rlmvneg  19495  psrbagsn  19782  evlsval  19806  psr1bas2  19847  psr1bas  19848  psr1plusg  19879  psr1vsca  19880  psr1mulr  19881  ply1plusgfvi  19899  ply1mpl0  19912  ply1mpl1  19914  cncrng  20054  xrsmcmn  20056  cndrng  20062  cnsrng  20067  xrs1mnd  20071  xrs10  20072  absabv  20090  zringcyg  20126  recrng  20255  ordtrestixx  21320  llyidm  21585  nllyidm  21586  toplly  21587  hauslly  21589  hausnlly  21590  lly1stc  21593  kgenf  21638  hmpher  21881  txswaphmeolem  21901  fmucndlem  22388  nrgtrg  22787  cnfldnm  22875  xrsxmet  22905  divcn  22964  expcn  22968  elcncf1ii  22992  iirevcn  23022  iihalf1cn  23024  iihalf2cn  23026  iimulcn  23030  icopnfcnv  23034  iccpnfcnv  23036  cnrehmeo  23045  tcphsub  23312  tcphphl  23318  iscmet3i  23403  cncmet  23413  rrxprds  23480  vitali  23685  i1f0  23759  itg20  23809  dvid  23986  dveflem  24047  dvef  24048  dvsincos  24049  ply1divalg2  24203  coe0  24317  iaa  24385  sincn  24503  coscn  24504  reefgim  24509  pilem3  24512  pilem3OLD  24513  resinf1o  24588  circgrp  24604  circsubm  24605  divlogrlim  24686  dvrelog  24688  logcn  24698  dvlog  24702  advlog  24705  cxpcn  24791  cxpcn2  24792  resqrtcn  24795  sqrtcn  24796  atansopn  24964  dvatan  24967  leibpilem2  24973  leibpi  24974  leibpisum  24975  log2cnv  24976  log2ublem2  24979  log2ub  24981  divsqrtsumlem  25011  emcllem4  25030  emcllem6  25032  emcllem7  25033  lgamf  25073  lgam1  25095  basellem6  25117  basellem7  25118  basellem8  25119  basellem9  25120  vmaf  25150  logfacrlim  25254  lgsdir2lem5  25359  chebbnd1  25466  chtppilim  25469  chto1ub  25470  chebbnd2  25471  chto1lb  25472  chpchtlim  25473  chpo1ub  25474  chpo1ubb  25475  vmadivsum  25476  vmadivsumb  25477  mudivsum  25524  mulogsumlem  25525  mulogsum  25526  logdivsum  25527  vmalogdivsum2  25532  vmalogdivsum  25533  selberglem1  25539  selberglem2  25540  selbergb  25543  selberg2lem  25544  selberg2  25545  selberg2b  25546  selberg3lem2  25552  selberg3  25553  selberg4  25555  pntrmax  25558  pntrsumo1  25559  pntrsumbnd  25560  selbergr  25562  selberg3r  25563  selberg4r  25564  selberg34r  25565  pntrlog2bndlem1  25571  pntrlog2bndlem4  25574  pnt2  25607  pnt  25608  istrkg2ld  25664  legval  25784  ttgsub  26064  cchhllem  26072  trlsfval  26900  pthsfval  26927  spthsfval  26928  clwlks  26978  crcts  26994  cycls  26995  2wspdisj  27205  2wspiundisj  27206  eupths  27496  konigsbergiedgw  27547  ipasslem7  28168  normlem6  28449  opsqrlem4  29479  eqri  29792  fpwrelmap  29978  fpwrelmapffs  29979  xrs0  30143  mdetlap1  30360  circtopn  30372  cnre2csqima  30425  cnvordtrestixx  30427  mndpluscn  30440  xrge0iifcnv  30447  zlm0  30474  zlm1  30475  qqhre  30532  rrhre  30533  esumnul  30578  hasheuni  30615  sxbrsigalem2  30816  oddpwdc  30884  eulerpartlemb  30898  eulerpartgbij  30902  eulerpartlemn  30911  fib0  30930  fib1  30931  ballotlemrinv  31064  sgn3da  31072  signsw0g  31103  circlemethnat  31191  subfacval2  31638  sinccvglem  32033  circum  32035  logi  32086  faclim  32098  faclim2  32100  dmscut  32383  cnndvlem1  32988  bj-spimev  33176  bj-dvelimv  33285  bj-inrab2  33373  bj-rabtrAUTO  33378  sucneqoni  33668  wl-cbvalnae  33766  wl-equsal  33772  poimirlem30  33884  dvtan  33904  dvasin  33940  dvacos  33941  dvreasin  33942  dvreacos  33943  efald2  34320  areaquad  38502  clsk1indlem4  39040  clsk1indlem1  39041  lhe4.4ex1a  39226  sbtT  39469  eel0TT  39615  eelTTT  39617  eelT1  39619  eelTT  39683  eelT  39685  eelT0  39687  isosctrlem1ALT  39846  disjsnxp  39914  infxr  40245  nfxneg  40352  limsup0  40588  0cnv  40636  limsup10ex  40667  liminf10ex  40668  liminfvalxr  40677  liminf0  40687  dvsinax  40789  itgsin0pilem1  40827  iblempty  40842  stowei  40942  wallispilem5  40947  wallispi  40948  stirlinglem1  40952  stirlinglem12  40963  stirlinglem13  40964  stirlinglem14  40965  stirlingr  40968  dirkertrigeqlem1  40976  fourierdlem62  41046  fourierdlem73  41057  fourierdlem76  41060  fourierdlem77  41061  fourierdlem103  41087  fourierdlem104  41088  fourierclim  41102  fourier  41103  fouriersw  41109  etransclem41  41153  etransclem46  41158  salexct2  41218  salexct3  41221  salgencntex  41222  salgensscntex  41223  dmvolsal  41225  bor1sal  41234  iocborel  41235  sge00  41254  sge0sn  41257  ovolval5lem3  41532  ioosshoi  41547  vonioolem2  41559  smfmullem4  41665  dfafv2  41904  onsetrec  43147  joinlmuladdmuli  43215
  Copyright terms: Public domain W3C validator