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

This theorem is referenced by:  hadbi123i  1597  cadbi123i  1612  nfan  1902  nfbi  1906  spimefv  2191  spime  2387  nfsb  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  eqabi  2868  eqabri  2876  nfeq  2915  nfel  2916  dvelimc  2930  nfralwOLD  3293  nfrexw  3294  nfral  3345  nfrex  3346  nfreuwOLD  3395  nfrmowOLD  3396  nfrmo  3403  nfreu  3404  rabbia2  3408  rabeqc  3417  nfrabw  3441  nfrabwOLD  3442  nfrab  3444  reuxfr  3710  reuxfr1  3713  nfsbc1  3761  nfsbcw  3764  nfsbc  3767  sbcbii  3802  csbeq2i  3866  nfcsb1  3882  nfcsbw  3885  nfcsb  3886  eqri  3967  vn0  4303  nfif  4521  nfdisjw  5087  nfdisj  5088  nfbr  5157  nfopab  5179  mpteq1i  5206  mpteq2ia  5213  mpteq12i  5216  ralxfr  5374  issoi  5584  nfiotaw  6457  nfiota  6459  nfriota  7331  nfov  7392  mpoeq123i  7438  mpoeq3ia  7440  opco1i  8062  xpord2indlem  8084  dfwrecsOLD  8249  on2recsfn  8618  on2recsov  8619  iseri  8682  nfixpw  8861  nfixp  8862  en2i  8937  en3i  8938  ensymb  8949  entr  8953  1sdom2dom  9198  nfttrcl  9656  djulf1o  9857  djurf1o  9858  r0weon  9957  recmulnq  10909  nrex1  11009  nfneg  11406  negiso  12144  suprzcl2  12872  supxr  13242  xrinf0  13267  fac0  14186  cnrecnv  15062  cau3  15252  cbvsum  15591  sum0  15617  ackbijnn  15724  flo1  15750  trireciplem  15758  trirecip  15759  ege2le3  15983  rpnnen2lem3  16109  ruclem4  16127  bitsf1ocnv  16335  prmreclem6  16804  prmrec  16805  modxai  16951  strfvn  17069  strss  17090  xpsvsca  17473  mreacs  17552  2oppccomf  17621  setc2obas  17994  setc2ohom  17995  cat1  17997  mndprop  18596  grpprop  18780  isgrpi  18787  oppgmndb  19150  oppggrpb  19153  odfval  19328  efgrelexlemb  19546  ablprop  19589  ringprop  20022  opprringb  20075  rlmbas  20723  rlmplusg  20724  rlm0  20725  rlmsub  20726  rlmmulr  20727  rlmsca2  20729  rlmvsca  20730  rlmtopn  20731  rlmds  20732  rlmvneg  20736  cncrng  20855  xrsmcmn  20857  cndrng  20863  cnsrng  20868  xrs1mnd  20872  xrs10  20873  absabv  20891  zringcyg  20927  resrng  21062  psrbagsn  21508  evlsval  21533  psr1bas2  21598  psr1bas  21599  psr1plusg  21630  psr1vsca  21631  psr1mulr  21632  ply1plusgfvi  21650  ply1mpl0  21663  ply1mpl1  21665  ordtrestixx  22610  llyidm  22876  nllyidm  22877  toplly  22878  hauslly  22880  hausnlly  22881  lly1stc  22884  kgenf  22929  txswaphmeolem  23192  fmucndlem  23680  nrgtrg  24091  cnfldnm  24179  xrsxmet  24209  divcn  24268  expcn  24272  elcncf1ii  24296  iirevcn  24330  iihalf1cn  24332  iihalf2cn  24334  iimulcn  24338  icopnfcnv  24342  iccpnfcnv  24344  cnrehmeo  24353  tcphsub  24622  tcphphl  24628  iscmet3i  24713  cncmet  24723  rrxprds  24790  vitali  25014  i1f0  25088  itg20  25139  dvid  25319  dveflem  25380  dvef  25381  dvsincos  25382  ply1divalg2  25540  coe0  25654  iaa  25722  sincn  25840  coscn  25841  reefgim  25846  pilem3  25849  resinf1o  25929  circgrp  25945  circsubm  25946  divlogrlim  26027  dvrelog  26029  logcn  26039  dvlog  26043  advlog  26046  cxpcn  26135  cxpcn2  26136  resqrtcn  26139  sqrtcn  26140  atansopn  26319  dvatan  26322  leibpilem2  26328  leibpi  26329  leibpisum  26330  log2cnv  26331  log2ublem2  26334  log2ub  26336  divsqrtsumlem  26366  emcllem4  26385  emcllem6  26387  emcllem7  26388  lgamf  26428  lgam1  26450  basellem6  26472  basellem7  26473  basellem8  26474  basellem9  26475  vmaf  26505  logfacrlim  26609  lgsdir2lem5  26714  chebbnd1  26857  chtppilim  26860  chto1ub  26861  chebbnd2  26862  chto1lb  26863  chpchtlim  26864  chpo1ub  26865  chpo1ubb  26866  vmadivsum  26867  vmadivsumb  26868  mudivsum  26915  mulogsumlem  26916  mulogsum  26917  logdivsum  26918  vmalogdivsum2  26923  vmalogdivsum  26924  selberglem1  26930  selberglem2  26931  selbergb  26934  selberg2lem  26935  selberg2  26936  selberg2b  26937  selberg3lem2  26943  selberg3  26944  selberg4  26946  pntrmax  26949  pntrsumo1  26950  pntrsumbnd  26951  selbergr  26953  selberg3r  26954  selberg4r  26955  selberg34r  26956  pntrlog2bndlem1  26962  pntrlog2bndlem4  26965  pnt2  26998  pnt  26999  dmscut  27193  lrrecpo  27296  noxpordpo  27305  noxpordfr  27306  noxpordse  27307  istrkg2ld  27465  legval  27589  ttgsub  27888  cchhllem  27898  cchhllemOLD  27899  2wspdisj  28970  2wspiundisj  28971  konigsbergiedgw  29255  ipasslem7  29841  normlem6  30120  opsqrlem4  31148  fpwrelmap  31718  fpwrelmapffs  31719  xrs0  31936  1fldgenq  32160  ccfldsrarelvec  32442  ccfldextdgrr  32443  mdetlap1  32496  circtopn  32507  cnre2csqima  32581  cnvordtrestixx  32583  mndpluscn  32596  xrge0iifcnv  32603  zlm0  32630  zlm1  32631  qqhre  32690  rrhre  32691  esumnul  32736  hasheuni  32773  sxbrsigalem2  32975  oddpwdc  33043  eulerpartlemb  33057  eulerpartgbij  33061  eulerpartlemn  33070  fib0  33088  fib1  33089  ballotlemrinv  33222  sgn3da  33230  signsw0g  33257  circlemethnat  33343  subfacval2  33868  sinccvglem  34347  circum  34349  logi  34393  faclim  34405  faclim2  34407  cnndvlem1  35076  bj-dvelimv  35395  bj-inrab2  35471  bj-rabtrAUTO  35475  bj-opelidb  35696  bj-iomnnom  35803  sucneqoni  35910  wl-df-3xor  36012  wl-3xorbi123i  36020  wl-df3maxtru1  36036  wl-cbvalnae  36065  wl-equsal  36072  poimirlem30  36181  dvtan  36201  dvasin  36235  dvacos  36236  dvreasin  36237  dvreacos  36238  efald2  36610  lcmineqlem7  40565  3lexlogpow5ineq1  40584  3lexlogpow5ineq5  40590  aks4d1p1p6  40603  re1m1e0m0  40924  re0m0e0  40929  reixi  40949  subresre  40957  3cubeslem4  41070  3cubes  41071  areaquad  41608  clsk1indlem4  42438  clsk1indlem1  42439  ismnushort  42703  lhe4.4ex1a  42731  sbtT  42971  eel0TT  43108  eelTTT  43110  eelT1  43112  eelTT  43175  eelT  43177  eelT0  43179  isosctrlem1ALT  43338  disjsnxp  43400  infxr  43722  nfxneg  43816  limsup0  44055  0cnv  44103  limsup10ex  44134  liminf10ex  44135  liminfvalxr  44144  liminf0  44154  dvsinax  44274  itgsin0pilem1  44311  iblempty  44326  stowei  44425  wallispilem5  44430  wallispi  44431  stirlinglem1  44435  stirlinglem12  44446  stirlinglem13  44447  stirlinglem14  44448  stirlingr  44451  dirkertrigeqlem1  44459  fourierdlem62  44529  fourierdlem73  44540  fourierdlem76  44543  fourierdlem77  44544  fourierdlem103  44570  fourierdlem104  44571  fourierclim  44585  fourier  44586  fouriersw  44592  etransclem41  44636  etransclem46  44641  salexct2  44700  salexct3  44703  salgencntex  44704  salgensscntex  44705  dmvolsal  44707  bor1sal  44716  iocborel  44717  sge00  44737  sge0sn  44740  ovolval5lem3  45015  ioosshoi  45030  vonioolem2  45042  smfmullem4  45155  upwrdfi  45246  dfafv2  45484  ichim  45769  setc2othin  47196  onsetrec  47273  joinlmuladdmuli  47340