Theorem mptru 1574

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 1571). (Contributed by Mario Carneiro, 13-Mar-2014.)

Hypothesis

Ref	Expression
mptru.1	⊢ (⊤ → 𝜑)

Assertion

Ref	Expression
mptru	⊢ 𝜑

Proof of Theorem mptru

Step	Hyp	Ref	Expression
1		tru 1571	. 2 ⊢ ⊤
2		mptru.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1568

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 210  df-tru 1570

This theorem is referenced by:  hadbi123i  1623  cadbi123i  1638  nfan  1926  nfbi  1930  spimefv  2240  spime  2427  nfsb  2561  nfmov  2594  nfmo  2596  nfeuw  2627  nfeu  2628  eqabi  2904  eqabri  2911  nfeq  2944  nfel  2945  dvelimc  2956  nfrexw  3319  nfral  3370  nfrex  3371  nfrmo  3421  nfreu  3422  rabbia2  3426  rabeqc  3435  nfrab  3461  reuxfr  3721  reuxfr1  3724  nfsbc1  3772  nfsbcw  3775  nfsbc  3778  sbcbii  3809  csbeq2i  3869  nfcsb1  3884  nfcsbw  3887  nfcsb  3888  eqri  3965  ss2abi  4028  ss2rabi  4038  nfif  4523  nfdisjw  5092  nfdisj  5093  nfbr  5162  nfopab  5184  mpteq1i  5206  mpteq2ia  5210  mpteq12i  5212  ralxfr  5386  issoi  5606  nfiotaw  6497  nfiota  6499  nfriota  7380  nfov  7441  mpoeq123i  7487  mpoeq3ia  7489  opco1i  8119  xpord2indlem  8142  on2recsfn  8652  on2recsov  8653  iseri  8721  nfixpw  8913  nfixp  8914  en2i  8986  en3i  8987  ensymb  8998  entr  9002  1sdom2dom  9213  nfttrcl  9679  djulf1o  9897  djurf1o  9898  r0weon  9995  recmulnq  10948  nrex1  11048  nfneg  11452  negiso  12194  suprzcl2  12961  supxr  13338  xrinf0  13364  fac0  14311  sgn3da  15137  cnrecnv  15215  cau3  15406  cbvsum  15745  cbvsumv  15746  sum0  15771  ackbijnn  15881  flo1  15907  trireciplem  15915  trirecip  15916  ege2le3  16143  rpnnen2lem3  16271  ruclem4  16289  bitsf1ocnv  16501  prmreclem6  16980  prmrec  16981  modxai  17127  strfvn  17245  strss  17265  xpsvsca  17630  mreacs  17713  2oppccomf  17780  setc2obas  18150  setc2ohom  18151  cat1  18153  chnflenfi  18683  chninf  18690  mndprop  18817  grpprop  19018  isgrpi  19025  oppgmndb  19424  oppggrpb  19427  odfval  19601  efgrelexlemb  19819  ablprop  19862  ringprop  20372  opprrngb  20427  opprringb  20429  rlmbas  21291  rlmplusg  21292  rlm0  21293  rlmsub  21294  rlmmulr  21295  rlmsca2  21297  rlmvsca  21298  rlmtopn  21299  rlmds  21300  rlmvneg  21304  cncrng  21511  xrsmcmn  21513  cndrng  21519  cnsrng  21524  absabv  21542  xrs1mnd  21558  xrs10  21559  zringcyg  21587  pzriprngALT  21613  resrng  21739  psrbagsn  22182  evlsval  22205  psr1bas2  22318  psr1bas  22319  psr1plusg  22348  psr1vsca  22349  psr1mulr  22350  ply1plusgfvi  22369  ply1mpl0  22384  ply1mpl1  22386  ordtrestixx  23347  llyidm  23613  nllyidm  23614  toplly  23615  hauslly  23617  hausnlly  23618  lly1stc  23621  kgenf  23666  txswaphmeolem  23929  fmucndlem  24415  nrgtrg  24815  cnfldnm  24903  xrsxmet  24935  divcn  24995  expcn  24999  elcncf1ii  25023  iirevcn  25057  iihalf1cn  25059  iihalf2cn  25061  iimulcn  25065  icopnfcnv  25069  iccpnfcnv  25071  cnrehmeo  25080  tcphsub  25348  tcphphl  25354  iscmet3i  25439  cncmet  25449  rrxprds  25516  vitali  25740  i1f0  25814  itg20  25864  cbvitgv  25904  dvid  26045  dveflem  26106  dvef  26107  dvsincos  26108  ply1divalg2  26264  coe0  26381  iaa  26454  sincn  26572  coscn  26573  reefgim  26578  pilem3  26581  resinf1o  26666  circgrp  26682  circsubm  26683  logi  26717  divlogrlim  26765  dvrelog  26767  logcn  26777  dvlog  26781  advlog  26784  cxpcn  26875  cxpcn2  26876  resqrtcn  26879  sqrtcn  26880  atansopn  27062  dvatan  27065  leibpilem2  27071  leibpi  27072  leibpisum  27073  log2cnv  27074  log2ublem2  27077  log2ub  27079  divsqrtsumlem  27109  emcllem4  27128  emcllem6  27130  emcllem7  27131  lgamf  27171  lgam1  27193  basellem6  27215  basellem7  27216  basellem8  27217  basellem9  27218  vmaf  27248  logfacrlim  27353  lgsdir2lem5  27458  chebbnd1  27601  chtppilim  27604  chto1ub  27605  chebbnd2  27606  chto1lb  27607  chpchtlim  27608  chpo1ub  27609  chpo1ubb  27610  vmadivsum  27611  vmadivsumb  27612  mudivsum  27659  mulogsumlem  27660  mulogsum  27661  logdivsum  27662  vmalogdivsum2  27667  vmalogdivsum  27668  selberglem1  27674  selberglem2  27675  selbergb  27678  selberg2lem  27679  selberg2  27680  selberg2b  27681  selberg3lem2  27687  selberg3  27688  selberg4  27690  pntrmax  27693  pntrsumo1  27694  pntrsumbnd  27695  selbergr  27697  selberg3r  27698  selberg4r  27699  selberg34r  27700  pntrlog2bndlem1  27706  pntrlog2bndlem4  27709  pnt2  27742  pnt  27743  dmcuts  27949  lrrecpo  28099  noxpordpo  28108  noxpordfr  28109  noxpordse  28110  n0ssno  28478  0n0s  28487  n0cut  28492  n0sge0  28496  zseo  28580  twocut  28581  nohalf  28582  halfcut  28616  bdaypw2n0bndlem  28621  0reno  28654  1reno  28655  istrkg2ld  28694  legval  28818  ttgsub  29168  cchhllem  29176  2wspdisj  30254  2wspiundisj  30255  konigsbergiedgw  30539  ipasslem7  31128  normlem6  31407  opsqrlem4  32435  fpwrelmap  33018  fpwrelmapffs  33019  xrs0  33266  elrgspnlem2  33503  1fldgenq  33585  dfprm3  33787  zringfrac  33788  0mplrim  33848  ccfldsrarelvec  34005  ccfldextdgrr  34006  constrextdg2  34083  iconstr  34100  constrsdrg  34109  2sqr3minply  34114  2sqr3nconstr  34115  cos9thpiminplylem3  34118  cos9thpiminply  34122  cos9thpinconstrlem1  34123  cos9thpinconstrlem2  34124  mdetlap1  34160  circtopn  34171  cnre2csqima  34245  cnvordtrestixx  34247  mndpluscn  34260  xrge0iifcnv  34267  zlm0  34294  zlm1  34295  qqhre  34354  rrhre  34355  esumnul  34382  hasheuni  34419  sxbrsigalem2  34620  oddpwdc  34688  eulerpartlemb  34702  eulerpartgbij  34706  eulerpartlemn  34715  fib0  34733  fib1  34734  ballotlemrinv  34868  signsw0g  34887  circlemethnat  34972  dvelimalcasei  35408  dvelimexcasei  35410  subfacval2  35577  sinccvglem  36062  circum  36064  antnest  36079  antnestALT  36084  faclim  36136  faclim2  36138  cnndvlem1  37014  bj-alextruim  37147  bj-dvelimv  37376  bj-inrab2  37451  bj-rabtrAUTO  37455  bj-opelidb  37683  bj-iomnnom  37790  sucneqoni  37899  wl-df-3xor  38001  wl-3xorbi123i  38009  wl-df3maxtru1  38025  wl-cbvalnae  38075  wl-equsal  38083  poimirlem30  38188  dvtan  38208  dvasin  38242  dvacos  38243  dvreasin  38244  dvreacos  38245  efald2  38616  lcmineqlem7  42691  3lexlogpow5ineq1  42710  3lexlogpow5ineq5  42716  aks4d1p1p6  42729  cxpi11d  42993  tan3rdpi  43002  asin1half  43007  redvmptabs  43010  readvrec2  43011  readvrec  43012  resuppsinopn  43013  readvcot  43014  re1m1e0m0  43047  re0m0e0  43052  reixi  43073  subresre  43081  3cubeslem4  43311  3cubes  43312  areaquad  43834  clsk1indlem4  44661  clsk1indlem1  44662  ismnushort  44902  lhe4.4ex1a  44930  sbtT  45167  eel0TT  45303  eelTTT  45305  eelT1  45307  eelTT  45370  eelT  45372  eelT0  45374  isosctrlem1ALT  45533  disjsnxp  45681  infxr  45973  nfxneg  46066  limsup0  46299  0cnv  46347  limsup10ex  46378  liminf10ex  46379  liminfvalxr  46388  liminf0  46398  dvsinax  46518  itgsin0pilem1  46555  iblempty  46570  stowei  46669  wallispilem5  46674  wallispi  46675  stirlinglem1  46679  stirlinglem12  46690  stirlinglem13  46691  stirlinglem14  46692  stirlingr  46695  dirkertrigeqlem1  46703  fourierdlem62  46773  fourierdlem73  46784  fourierdlem76  46787  fourierdlem77  46788  fourierdlem103  46814  fourierdlem104  46815  fourierclim  46829  fourier  46830  fouriersw  46836  etransclem41  46880  etransclem46  46885  salexct2  46944  salexct3  46947  salgencntex  46948  salgensscntex  46949  dmvolsal  46951  bor1sal  46960  iocborel  46961  sge00  46981  sge0sn  46984  ovolval5lem3  47259  ioosshoi  47274  vonioolem2  47286  smfmullem4  47399  nthrucw  47493  goldrasin  47507  goldrapos  47508  cjnpoly  47514  dfafv2  47757  ichim  48094  grlimedgnedg  48784  nelsubc3  49733  fucofulem2  49973  setc2othin  50128  setcsnterm  50152  setc1obas  50154  setc1ohomfval  50155  setc1ocofval  50156  setc1oid  50157  termc2  50180  setc1onsubc  50264  onsetrec  50370  joinlmuladdmuli  50435