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  2205  spime  2393  nfsb  2527  nfmov  2560  nfmo  2562  nfeuw  2593  nfeu  2594  eqabi  2871  eqabri  2878  nfeq  2912  nfel  2913  dvelimc  2924  nfrexw  3284  nfral  3344  nfrex  3345  nfrmo  3397  nfreu  3398  rabbia2  3402  rabeqc  3411  nfrabw  3436  nfrab  3438  reuxfr  3707  reuxfr1  3710  nfsbc1  3759  nfsbcw  3762  nfsbc  3765  sbcbii  3797  csbeq2i  3857  nfcsb1  3872  nfcsbw  3875  nfcsb  3876  eqri  3954  ss2rabi  4028  nfif  4510  nfdisjw  5077  nfdisj  5078  nfbr  5145  nfopab  5167  mpteq1i  5189  mpteq2ia  5193  mpteq12i  5195  ralxfr  5359  issoi  5568  nfiotaw  6452  nfiota  6454  nfriota  7327  nfov  7388  mpoeq123i  7434  mpoeq3ia  7436  opco1i  8067  xpord2indlem  8089  on2recsfn  8595  on2recsov  8596  iseri  8662  nfixpw  8854  nfixp  8855  en2i  8927  en3i  8928  ensymb  8939  entr  8943  1sdom2dom  9154  nfttrcl  9620  djulf1o  9824  djurf1o  9825  r0weon  9922  recmulnq  10875  nrex1  10975  nfneg  11376  negiso  12122  suprzcl2  12851  supxr  13228  xrinf0  13254  fac0  14199  cnrecnv  15088  cau3  15279  cbvsum  15618  cbvsumv  15619  sum0  15644  ackbijnn  15751  flo1  15777  trireciplem  15785  trirecip  15786  ege2le3  16013  rpnnen2lem3  16141  ruclem4  16159  bitsf1ocnv  16371  prmreclem6  16849  prmrec  16850  modxai  16996  strfvn  17113  strss  17133  xpsvsca  17498  mreacs  17581  2oppccomf  17648  setc2obas  18018  setc2ohom  18019  cat1  18021  chnflenfi  18551  chninf  18558  mndprop  18685  grpprop  18882  isgrpi  18889  oppgmndb  19284  oppggrpb  19287  odfval  19461  efgrelexlemb  19679  ablprop  19722  ringprop  20225  opprrngb  20282  opprringb  20284  rlmbas  21145  rlmplusg  21146  rlm0  21147  rlmsub  21148  rlmmulr  21149  rlmsca2  21151  rlmvsca  21152  rlmtopn  21153  rlmds  21154  rlmvneg  21158  dfcnfldOLD  21325  cncrng  21343  cncrngOLD  21344  xrsmcmn  21346  cndrng  21353  cndrngOLD  21354  cnsrng  21360  absabv  21379  xrs1mnd  21395  xrs10  21396  zringcyg  21424  pzriprngALT  21450  resrng  21576  psrbagsn  22018  evlsval  22041  psr1bas2  22130  psr1bas  22131  psr1plusg  22161  psr1vsca  22162  psr1mulr  22163  ply1plusgfvi  22182  ply1mpl0  22197  ply1mpl1  22199  ordtrestixx  23166  llyidm  23432  nllyidm  23433  toplly  23434  hauslly  23436  hausnlly  23437  lly1stc  23440  kgenf  23485  txswaphmeolem  23748  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  25177  tcphphl  25183  iscmet3i  25268  cncmet  25278  rrxprds  25345  vitali  25570  i1f0  25644  itg20  25694  cbvitgv  25734  dvid  25875  dveflem  25939  dvef  25940  dvsincos  25941  ply1divalg2  26100  coe0  26217  iaa  26289  sincn  26410  coscn  26411  reefgim  26416  pilem3  26419  resinf1o  26501  circgrp  26517  circsubm  26518  logi  26552  divlogrlim  26600  dvrelog  26602  logcn  26612  dvlog  26616  advlog  26619  cxpcn  26710  cxpcnOLD  26711  cxpcn2  26712  resqrtcn  26715  sqrtcn  26716  atansopn  26898  dvatan  26901  leibpilem2  26907  leibpi  26908  leibpisum  26909  log2cnv  26910  log2ublem2  26913  log2ub  26915  divsqrtsumlem  26946  emcllem4  26965  emcllem6  26967  emcllem7  26968  lgamf  27008  lgam1  27030  basellem6  27052  basellem7  27053  basellem8  27054  basellem9  27055  vmaf  27085  logfacrlim  27191  lgsdir2lem5  27296  chebbnd1  27439  chtppilim  27442  chto1ub  27443  chebbnd2  27444  chto1lb  27445  chpchtlim  27446  chpo1ub  27447  chpo1ubb  27448  vmadivsum  27449  vmadivsumb  27450  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  logdivsum  27500  vmalogdivsum2  27505  vmalogdivsum  27506  selberglem1  27512  selberglem2  27513  selbergb  27516  selberg2lem  27517  selberg2  27518  selberg2b  27519  selberg3lem2  27525  selberg3  27526  selberg4  27528  pntrmax  27531  pntrsumo1  27532  pntrsumbnd  27533  selbergr  27535  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem4  27547  pnt2  27580  pnt  27581  dmcuts  27787  lrrecpo  27937  noxpordpo  27946  noxpordfr  27947  noxpordse  27948  n0ssno  28316  0n0s  28325  n0cut  28330  n0sge0  28334  zseo  28418  twocut  28419  nohalf  28420  halfcut  28454  bdaypw2n0bndlem  28459  0reno  28492  1reno  28493  istrkg2ld  28532  legval  28656  ttgsub  28951  cchhllem  28959  2wspdisj  30038  2wspiundisj  30039  konigsbergiedgw  30323  ipasslem7  30911  normlem6  31190  opsqrlem4  32218  fpwrelmap  32812  fpwrelmapffs  32813  sgn3da  32915  xrs0  33088  elrgspnlem2  33325  1fldgenq  33404  dfprm3  33634  zringfrac  33635  ccfldsrarelvec  33828  ccfldextdgrr  33829  constrextdg2  33906  iconstr  33923  constrsdrg  33932  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpiminplylem3  33941  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  mdetlap1  33983  circtopn  33994  cnre2csqima  34068  cnvordtrestixx  34070  mndpluscn  34083  xrge0iifcnv  34090  zlm0  34117  zlm1  34118  qqhre  34177  rrhre  34178  esumnul  34205  hasheuni  34242  sxbrsigalem2  34443  oddpwdc  34511  eulerpartlemb  34525  eulerpartgbij  34529  eulerpartlemn  34538  fib0  34556  fib1  34557  ballotlemrinv  34691  signsw0g  34713  circlemethnat  34798  dvelimalcasei  35232  dvelimexcasei  35234  subfacval2  35381  sinccvglem  35866  circum  35868  antnest  35883  antnestALT  35888  faclim  35940  faclim2  35942  cnndvlem1  36737  bj-dvelimv  37054  bj-inrab2  37129  bj-rabtrAUTO  37133  bj-opelidb  37357  bj-iomnnom  37464  sucneqoni  37571  wl-df-3xor  37673  wl-3xorbi123i  37681  wl-df3maxtru1  37697  wl-cbvalnae  37738  wl-equsal  37746  poimirlem30  37851  dvtan  37871  dvasin  37905  dvacos  37906  dvreasin  37907  dvreacos  37908  efald2  38279  lcmineqlem7  42289  3lexlogpow5ineq1  42308  3lexlogpow5ineq5  42314  aks4d1p1p6  42327  cxpi11d  42598  tan3rdpi  42607  asin1half  42612  redvmptabs  42615  readvrec2  42616  readvrec  42617  resuppsinopn  42618  readvcot  42619  re1m1e0m0  42652  re0m0e0  42657  reixi  42678  subresre  42686  3cubeslem4  42931  3cubes  42932  areaquad  43458  clsk1indlem4  44285  clsk1indlem1  44286  ismnushort  44542  lhe4.4ex1a  44570  sbtT  44808  eel0TT  44944  eelTTT  44946  eelT1  44948  eelTT  45011  eelT  45013  eelT0  45015  isosctrlem1ALT  45174  disjsnxp  45315  infxr  45611  nfxneg  45705  limsup0  45938  0cnv  45986  limsup10ex  46017  liminf10ex  46018  liminfvalxr  46027  liminf0  46037  dvsinax  46157  itgsin0pilem1  46194  iblempty  46209  stowei  46308  wallispilem5  46313  wallispi  46314  stirlinglem1  46318  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlingr  46334  dirkertrigeqlem1  46342  fourierdlem62  46412  fourierdlem73  46423  fourierdlem76  46426  fourierdlem77  46427  fourierdlem103  46453  fourierdlem104  46454  fourierclim  46468  fourier  46469  fouriersw  46475  etransclem41  46519  etransclem46  46524  salexct2  46583  salexct3  46586  salgencntex  46587  salgensscntex  46588  dmvolsal  46590  bor1sal  46599  iocborel  46600  sge00  46620  sge0sn  46623  ovolval5lem3  46898  ioosshoi  46913  vonioolem2  46925  smfmullem4  47038  nthrucw  47130  cjnpoly  47135  dfafv2  47378  ichim  47703  grlimedgnedg  48377  nelsubc3  49316  fucofulem2  49556  setc2othin  49711  setcsnterm  49735  setc1obas  49737  setc1ohomfval  49738  setc1ocofval  49739  setc1oid  49740  termc2  49763  setc1onsubc  49847  onsetrec  49953  joinlmuladdmuli  50018