Theorem mptru 1548

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 1545). (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 1545	. 2 ⊢ ⊤
2		mptru.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1542

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 207  df-tru 1544

This theorem is referenced by:  hadbi123i  1597  cadbi123i  1612  nfan  1900  nfbi  1904  spimefv  2203  spime  2391  nfsb  2525  nfmov  2558  nfmo  2560  nfeuw  2591  nfeu  2592  eqabi  2869  eqabri  2876  nfeq  2910  nfel  2911  dvelimc  2922  nfrexw  3282  nfral  3342  nfrex  3343  nfrmo  3395  nfreu  3396  rabbia2  3400  rabeqc  3409  nfrabw  3434  nfrab  3436  reuxfr  3705  reuxfr1  3708  nfsbc1  3757  nfsbcw  3760  nfsbc  3763  sbcbii  3795  csbeq2i  3855  nfcsb1  3870  nfcsbw  3873  nfcsb  3874  eqri  3952  ss2rabi  4026  nfif  4508  nfdisjw  5075  nfdisj  5076  nfbr  5143  nfopab  5165  mpteq1i  5187  mpteq2ia  5191  mpteq12i  5193  ralxfr  5357  issoi  5566  nfiotaw  6450  nfiota  6452  nfriota  7325  nfov  7386  mpoeq123i  7432  mpoeq3ia  7434  opco1i  8065  xpord2indlem  8087  on2recsfn  8593  on2recsov  8594  iseri  8660  nfixpw  8852  nfixp  8853  en2i  8925  en3i  8926  ensymb  8937  entr  8941  1sdom2dom  9152  nfttrcl  9618  djulf1o  9822  djurf1o  9823  r0weon  9920  recmulnq  10873  nrex1  10973  nfneg  11374  negiso  12120  suprzcl2  12849  supxr  13226  xrinf0  13252  fac0  14197  cnrecnv  15086  cau3  15277  cbvsum  15616  cbvsumv  15617  sum0  15642  ackbijnn  15749  flo1  15775  trireciplem  15783  trirecip  15784  ege2le3  16011  rpnnen2lem3  16139  ruclem4  16157  bitsf1ocnv  16369  prmreclem6  16847  prmrec  16848  modxai  16994  strfvn  17111  strss  17131  xpsvsca  17496  mreacs  17579  2oppccomf  17646  setc2obas  18016  setc2ohom  18017  cat1  18019  chnflenfi  18549  chninf  18556  mndprop  18683  grpprop  18880  isgrpi  18887  oppgmndb  19282  oppggrpb  19285  odfval  19459  efgrelexlemb  19677  ablprop  19720  ringprop  20223  opprrngb  20280  opprringb  20282  rlmbas  21143  rlmplusg  21144  rlm0  21145  rlmsub  21146  rlmmulr  21147  rlmsca2  21149  rlmvsca  21150  rlmtopn  21151  rlmds  21152  rlmvneg  21156  dfcnfldOLD  21323  cncrng  21341  cncrngOLD  21342  xrsmcmn  21344  cndrng  21351  cndrngOLD  21352  cnsrng  21358  absabv  21377  xrs1mnd  21393  xrs10  21394  zringcyg  21422  pzriprngALT  21448  resrng  21574  psrbagsn  22016  evlsval  22039  psr1bas2  22128  psr1bas  22129  psr1plusg  22159  psr1vsca  22160  psr1mulr  22161  ply1plusgfvi  22180  ply1mpl0  22195  ply1mpl1  22197  ordtrestixx  23164  llyidm  23430  nllyidm  23431  toplly  23432  hauslly  23434  hausnlly  23435  lly1stc  23438  kgenf  23483  txswaphmeolem  23746  fmucndlem  24232  nrgtrg  24632  cnfldnm  24720  xrsxmet  24752  divcnOLD  24811  divcn  24813  expcn  24817  expcnOLD  24819  elcncf1ii  24843  iirevcn  24878  iihalf1cn  24880  iihalf1cnOLD  24881  iihalf2cn  24883  iihalf2cnOLD  24884  iimulcn  24888  iimulcnOLD  24889  icopnfcnv  24894  iccpnfcnv  24896  cnrehmeo  24905  cnrehmeoOLD  24906  tcphsub  25175  tcphphl  25181  iscmet3i  25266  cncmet  25276  rrxprds  25343  vitali  25568  i1f0  25642  itg20  25692  cbvitgv  25732  dvid  25873  dveflem  25937  dvef  25938  dvsincos  25939  ply1divalg2  26098  coe0  26215  iaa  26287  sincn  26408  coscn  26409  reefgim  26414  pilem3  26417  resinf1o  26499  circgrp  26515  circsubm  26516  logi  26550  divlogrlim  26598  dvrelog  26600  logcn  26610  dvlog  26614  advlog  26617  cxpcn  26708  cxpcnOLD  26709  cxpcn2  26710  resqrtcn  26713  sqrtcn  26714  atansopn  26896  dvatan  26899  leibpilem2  26905  leibpi  26906  leibpisum  26907  log2cnv  26908  log2ublem2  26911  log2ub  26913  divsqrtsumlem  26944  emcllem4  26963  emcllem6  26965  emcllem7  26966  lgamf  27006  lgam1  27028  basellem6  27050  basellem7  27051  basellem8  27052  basellem9  27053  vmaf  27083  logfacrlim  27189  lgsdir2lem5  27294  chebbnd1  27437  chtppilim  27440  chto1ub  27441  chebbnd2  27442  chto1lb  27443  chpchtlim  27444  chpo1ub  27445  chpo1ubb  27446  vmadivsum  27447  vmadivsumb  27448  mudivsum  27495  mulogsumlem  27496  mulogsum  27497  logdivsum  27498  vmalogdivsum2  27503  vmalogdivsum  27504  selberglem1  27510  selberglem2  27511  selbergb  27514  selberg2lem  27515  selberg2  27516  selberg2b  27517  selberg3lem2  27523  selberg3  27524  selberg4  27526  pntrmax  27529  pntrsumo1  27530  pntrsumbnd  27531  selbergr  27533  selberg3r  27534  selberg4r  27535  selberg34r  27536  pntrlog2bndlem1  27542  pntrlog2bndlem4  27545  pnt2  27578  pnt  27579  dmscut  27779  lrrecpo  27911  noxpordpo  27920  noxpordfr  27921  noxpordse  27922  n0ssno  28281  0n0s  28290  n0scut  28294  n0sge0  28298  1p1e2s  28374  zseo  28380  twocut  28381  nohalf  28382  halfcut  28415  bdaypw2n0s  28420  0reno  28441  1reno  28442  istrkg2ld  28481  legval  28605  ttgsub  28900  cchhllem  28908  2wspdisj  29987  2wspiundisj  29988  konigsbergiedgw  30272  ipasslem7  30860  normlem6  31139  opsqrlem4  32167  fpwrelmap  32761  fpwrelmapffs  32762  sgn3da  32864  xrs0  33037  elrgspnlem2  33274  1fldgenq  33353  dfprm3  33583  zringfrac  33584  ccfldsrarelvec  33777  ccfldextdgrr  33778  constrextdg2  33855  iconstr  33872  constrsdrg  33881  2sqr3minply  33886  2sqr3nconstr  33887  cos9thpiminplylem3  33890  cos9thpiminply  33894  cos9thpinconstrlem1  33895  cos9thpinconstrlem2  33896  mdetlap1  33932  circtopn  33943  cnre2csqima  34017  cnvordtrestixx  34019  mndpluscn  34032  xrge0iifcnv  34039  zlm0  34066  zlm1  34067  qqhre  34126  rrhre  34127  esumnul  34154  hasheuni  34191  sxbrsigalem2  34392  oddpwdc  34460  eulerpartlemb  34474  eulerpartgbij  34478  eulerpartlemn  34487  fib0  34505  fib1  34506  ballotlemrinv  34640  signsw0g  34662  circlemethnat  34747  dvelimalcasei  35181  dvelimexcasei  35183  subfacval2  35330  sinccvglem  35815  circum  35817  antnest  35832  antnestALT  35837  faclim  35889  faclim2  35891  cnndvlem1  36680  bj-dvelimv  36997  bj-inrab2  37072  bj-rabtrAUTO  37076  bj-opelidb  37296  bj-iomnnom  37403  sucneqoni  37510  wl-df-3xor  37612  wl-3xorbi123i  37620  wl-df3maxtru1  37636  wl-cbvalnae  37677  wl-equsal  37685  poimirlem30  37790  dvtan  37810  dvasin  37844  dvacos  37845  dvreasin  37846  dvreacos  37847  efald2  38218  lcmineqlem7  42228  3lexlogpow5ineq1  42247  3lexlogpow5ineq5  42253  aks4d1p1p6  42266  cxpi11d  42540  tan3rdpi  42549  asin1half  42554  redvmptabs  42557  readvrec2  42558  readvrec  42559  resuppsinopn  42560  readvcot  42561  re1m1e0m0  42594  re0m0e0  42599  reixi  42620  subresre  42628  3cubeslem4  42873  3cubes  42874  areaquad  43400  clsk1indlem4  44227  clsk1indlem1  44228  ismnushort  44484  lhe4.4ex1a  44512  sbtT  44750  eel0TT  44886  eelTTT  44888  eelT1  44890  eelTT  44953  eelT  44955  eelT0  44957  isosctrlem1ALT  45116  disjsnxp  45257  infxr  45553  nfxneg  45647  limsup0  45880  0cnv  45928  limsup10ex  45959  liminf10ex  45960  liminfvalxr  45969  liminf0  45979  dvsinax  46099  itgsin0pilem1  46136  iblempty  46151  stowei  46250  wallispilem5  46255  wallispi  46256  stirlinglem1  46260  stirlinglem12  46271  stirlinglem13  46272  stirlinglem14  46273  stirlingr  46276  dirkertrigeqlem1  46284  fourierdlem62  46354  fourierdlem73  46365  fourierdlem76  46368  fourierdlem77  46369  fourierdlem103  46395  fourierdlem104  46396  fourierclim  46410  fourier  46411  fouriersw  46417  etransclem41  46461  etransclem46  46466  salexct2  46525  salexct3  46528  salgencntex  46529  salgensscntex  46530  dmvolsal  46532  bor1sal  46541  iocborel  46542  sge00  46562  sge0sn  46565  ovolval5lem3  46840  ioosshoi  46855  vonioolem2  46867  smfmullem4  46980  nthrucw  47072  cjnpoly  47077  dfafv2  47320  ichim  47645  grlimedgnedg  48319  nelsubc3  49258  fucofulem2  49498  setc2othin  49653  setcsnterm  49677  setc1obas  49679  setc1ohomfval  49680  setc1ocofval  49681  setc1oid  49682  termc2  49705  setc1onsubc  49789  onsetrec  49895  joinlmuladdmuli  49960