Theorem mptru 1547

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

Syntax hints:   → wi 4  ⊤wtru 1541

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 1543

This theorem is referenced by:  hadbi123i  1596  cadbi123i  1611  nfan  1899  nfbi  1903  spimefv  2199  spime  2394  nfsb  2528  nfmov  2560  nfmo  2562  nfeuw  2593  nfeu  2594  eqabi  2871  eqabri  2879  nfeq  2913  nfel  2914  dvelimc  2925  nfralwOLD  3296  nfrexw  3297  nfral  3358  nfrex  3359  nfreuwOLD  3410  nfrmowOLD  3411  nfrmo  3418  nfreu  3419  rabbia2  3423  rabeqc  3433  nfrabw  3459  nfrabwOLD  3460  nfrab  3462  reuxfr  3737  reuxfr1  3740  nfsbc1  3789  nfsbcw  3792  nfsbc  3795  sbcbii  3827  csbeq2i  3887  nfcsb1  3902  nfcsbw  3905  nfcsb  3906  eqri  3984  vn0  4325  nfif  4536  nfdisjw  5103  nfdisj  5104  nfbr  5171  nfopab  5193  mpteq1i  5216  mpteq2ia  5221  mpteq12i  5223  ralxfr  5389  issoi  5602  nfiotaw  6493  nfiota  6495  nfriota  7379  nfov  7440  mpoeq123i  7488  mpoeq3ia  7490  opco1i  8129  xpord2indlem  8151  dfwrecsOLD  8317  on2recsfn  8684  on2recsov  8685  iseri  8751  nfixpw  8935  nfixp  8936  en2i  9009  en3i  9010  ensymb  9021  entr  9025  1sdom2dom  9260  nfttrcl  9730  djulf1o  9931  djurf1o  9932  r0weon  10031  recmulnq  10983  nrex1  11083  nfneg  11483  negiso  12227  suprzcl2  12959  supxr  13334  xrinf0  13360  fac0  14299  cnrecnv  15189  cau3  15379  cbvsum  15716  cbvsumv  15717  sum0  15742  ackbijnn  15849  flo1  15875  trireciplem  15883  trirecip  15884  ege2le3  16111  rpnnen2lem3  16239  ruclem4  16257  bitsf1ocnv  16468  prmreclem6  16946  prmrec  16947  modxai  17093  strfvn  17210  strss  17230  xpsvsca  17596  mreacs  17675  2oppccomf  17742  setc2obas  18112  setc2ohom  18113  cat1  18115  mndprop  18743  grpprop  18940  isgrpi  18947  oppgmndb  19343  oppggrpb  19346  odfval  19518  efgrelexlemb  19736  ablprop  19779  ringprop  20255  opprrngb  20311  opprringb  20313  rlmbas  21156  rlmplusg  21157  rlm0  21158  rlmsub  21159  rlmmulr  21160  rlmsca2  21162  rlmvsca  21163  rlmtopn  21164  rlmds  21165  rlmvneg  21169  dfcnfldOLD  21336  cncrng  21356  cncrngOLD  21357  xrsmcmn  21359  cndrng  21366  cndrngOLD  21367  cnsrng  21373  xrs1mnd  21377  xrs10  21378  absabv  21397  zringcyg  21435  pzriprngALT  21461  resrng  21586  psrbagsn  22026  evlsval  22049  psr1bas2  22130  psr1bas  22131  psr1plusg  22161  psr1vsca  22162  psr1mulr  22163  ply1plusgfvi  22182  ply1mpl0  22197  ply1mpl1  22199  ordtrestixx  23165  llyidm  23431  nllyidm  23432  toplly  23433  hauslly  23435  hausnlly  23436  lly1stc  23439  kgenf  23484  txswaphmeolem  23747  fmucndlem  24234  nrgtrg  24634  cnfldnm  24722  xrsxmet  24754  divcnOLD  24813  divcn  24815  expcn  24819  expcnOLD  24821  elcncf1ii  24845  iirevcn  24880  iihalf1cn  24882  iihalf1cnOLD  24883  iihalf2cn  24885  iihalf2cnOLD  24886  iimulcn  24890  iimulcnOLD  24891  icopnfcnv  24896  iccpnfcnv  24898  cnrehmeo  24907  cnrehmeoOLD  24908  tcphsub  25178  tcphphl  25184  iscmet3i  25269  cncmet  25279  rrxprds  25346  vitali  25571  i1f0  25645  itg20  25695  cbvitgv  25735  dvid  25876  dveflem  25940  dvef  25941  dvsincos  25942  ply1divalg2  26101  coe0  26218  iaa  26290  sincn  26411  coscn  26412  reefgim  26417  pilem3  26420  resinf1o  26502  circgrp  26518  circsubm  26519  logi  26553  divlogrlim  26601  dvrelog  26603  logcn  26613  dvlog  26617  advlog  26620  cxpcn  26711  cxpcnOLD  26712  cxpcn2  26713  resqrtcn  26716  sqrtcn  26717  atansopn  26899  dvatan  26902  leibpilem2  26908  leibpi  26909  leibpisum  26910  log2cnv  26911  log2ublem2  26914  log2ub  26916  divsqrtsumlem  26947  emcllem4  26966  emcllem6  26968  emcllem7  26969  lgamf  27009  lgam1  27031  basellem6  27053  basellem7  27054  basellem8  27055  basellem9  27056  vmaf  27086  logfacrlim  27192  lgsdir2lem5  27297  chebbnd1  27440  chtppilim  27443  chto1ub  27444  chebbnd2  27445  chto1lb  27446  chpchtlim  27447  chpo1ub  27448  chpo1ubb  27449  vmadivsum  27450  vmadivsumb  27451  mudivsum  27498  mulogsumlem  27499  mulogsum  27500  logdivsum  27501  vmalogdivsum2  27506  vmalogdivsum  27507  selberglem1  27513  selberglem2  27514  selbergb  27517  selberg2lem  27518  selberg2  27519  selberg2b  27520  selberg3lem2  27526  selberg3  27527  selberg4  27529  pntrmax  27532  pntrsumo1  27533  pntrsumbnd  27534  selbergr  27536  selberg3r  27537  selberg4r  27538  selberg34r  27539  pntrlog2bndlem1  27545  pntrlog2bndlem4  27548  pnt2  27581  pnt  27582  dmscut  27780  lrrecpo  27905  noxpordpo  27914  noxpordfr  27915  noxpordse  27916  n0sex  28267  n0ssno  28270  0n0s  28279  n0scut  28283  n0sge0  28287  1p1e2s  28359  zseo  28365  twocut  28366  nohalf  28367  halfcut  28390  0reno  28405  istrkg2ld  28444  legval  28568  ttgsub  28863  cchhllem  28871  2wspdisj  29949  2wspiundisj  29950  konigsbergiedgw  30234  ipasslem7  30822  normlem6  31101  opsqrlem4  32129  fpwrelmap  32715  fpwrelmapffs  32716  sgn3da  32818  xrs0  33003  elrgspnlem2  33243  1fldgenq  33321  dfprm3  33573  zringfrac  33574  ccfldsrarelvec  33717  ccfldextdgrr  33718  constrextdg2  33788  iconstr  33805  constrsdrg  33814  2sqr3minply  33819  2sqr3nconstr  33820  cos9thpiminplylem3  33823  cos9thpiminply  33827  cos9thpinconstrlem1  33828  mdetlap1  33862  circtopn  33873  cnre2csqima  33947  cnvordtrestixx  33949  mndpluscn  33962  xrge0iifcnv  33969  zlm0  33996  zlm1  33997  qqhre  34056  rrhre  34057  esumnul  34084  hasheuni  34121  sxbrsigalem2  34323  oddpwdc  34391  eulerpartlemb  34405  eulerpartgbij  34409  eulerpartlemn  34418  fib0  34436  fib1  34437  ballotlemrinv  34571  signsw0g  34593  circlemethnat  34678  dvelimalcasei  35112  dvelimexcasei  35114  subfacval2  35214  sinccvglem  35699  circum  35701  antnest  35716  faclim  35768  faclim2  35770  cnndvlem1  36560  bj-dvelimv  36876  bj-inrab2  36951  bj-rabtrAUTO  36955  bj-opelidb  37175  bj-iomnnom  37282  sucneqoni  37389  wl-df-3xor  37491  wl-3xorbi123i  37499  wl-df3maxtru1  37515  wl-cbvalnae  37556  wl-equsal  37564  poimirlem30  37679  dvtan  37699  dvasin  37733  dvacos  37734  dvreasin  37735  dvreacos  37736  efald2  38107  lcmineqlem7  42053  3lexlogpow5ineq1  42072  3lexlogpow5ineq5  42078  aks4d1p1p6  42091  cxpi11d  42361  tan3rdpi  42370  asin1half  42375  redvmptabs  42378  readvrec2  42379  readvrec  42380  resuppsinopn  42381  readvcot  42382  re1m1e0m0  42415  re0m0e0  42420  reixi  42440  subresre  42448  3cubeslem4  42687  3cubes  42688  areaquad  43215  clsk1indlem4  44043  clsk1indlem1  44044  ismnushort  44300  lhe4.4ex1a  44328  sbtT  44567  eel0TT  44703  eelTTT  44705  eelT1  44707  eelTT  44770  eelT  44772  eelT0  44774  isosctrlem1ALT  44933  disjsnxp  45074  infxr  45374  nfxneg  45468  limsup0  45703  0cnv  45751  limsup10ex  45782  liminf10ex  45783  liminfvalxr  45792  liminf0  45802  dvsinax  45922  itgsin0pilem1  45959  iblempty  45974  stowei  46073  wallispilem5  46078  wallispi  46079  stirlinglem1  46083  stirlinglem12  46094  stirlinglem13  46095  stirlinglem14  46096  stirlingr  46099  dirkertrigeqlem1  46107  fourierdlem62  46177  fourierdlem73  46188  fourierdlem76  46191  fourierdlem77  46192  fourierdlem103  46218  fourierdlem104  46219  fourierclim  46233  fourier  46234  fouriersw  46240  etransclem41  46284  etransclem46  46289  salexct2  46348  salexct3  46351  salgencntex  46352  salgensscntex  46353  dmvolsal  46355  bor1sal  46364  iocborel  46365  sge00  46385  sge0sn  46388  ovolval5lem3  46663  ioosshoi  46678  vonioolem2  46690  smfmullem4  46803  upwrdfi  46896  dfafv2  47141  ichim  47451  nelsubc3  49018  fucofulem2  49202  setc2othin  49332  setcsnterm  49355  setc1obas  49357  setc1ohomfval  49358  setc1ocofval  49359  setc1oid  49360  termc2  49383  setc1onsubc  49459  onsetrec  49552  joinlmuladdmuli  49617