Theorem mptru 1549

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

Syntax hints:   → wi 4  ⊤wtru 1543

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 1545

This theorem is referenced by:  hadbi123i  1598  cadbi123i  1613  nfan  1901  nfbi  1905  spimefv  2206  spime  2394  nfsb  2528  nfmov  2561  nfmo  2563  nfeuw  2594  nfeu  2595  eqabi  2872  eqabri  2879  nfeq  2913  nfel  2914  dvelimc  2925  nfrexw  3286  nfral  3337  nfrex  3338  nfrmo  3388  nfreu  3389  rabbia2  3393  rabeqc  3402  nfrab  3428  reuxfr  3696  reuxfr1  3699  nfsbc1  3748  nfsbcw  3751  nfsbc  3754  sbcbii  3786  csbeq2i  3846  nfcsb1  3861  nfcsbw  3864  nfcsb  3865  eqri  3943  ss2abi  4007  ss2rabi  4017  nfif  4498  nfdisjw  5065  nfdisj  5066  nfbr  5133  nfopab  5155  mpteq1i  5177  mpteq2ia  5181  mpteq12i  5183  ralxfr  5352  issoi  5569  nfiotaw  6453  nfiota  6455  nfriota  7330  nfov  7391  mpoeq123i  7437  mpoeq3ia  7439  opco1i  8069  xpord2indlem  8091  on2recsfn  8597  on2recsov  8598  iseri  8665  nfixpw  8858  nfixp  8859  en2i  8931  en3i  8932  ensymb  8943  entr  8947  1sdom2dom  9158  nfttrcl  9626  djulf1o  9830  djurf1o  9831  r0weon  9928  recmulnq  10881  nrex1  10981  nfneg  11383  negiso  12130  suprzcl2  12882  supxr  13259  xrinf0  13285  fac0  14232  cnrecnv  15121  cau3  15312  cbvsum  15651  cbvsumv  15652  sum0  15677  ackbijnn  15787  flo1  15813  trireciplem  15821  trirecip  15822  ege2le3  16049  rpnnen2lem3  16177  ruclem4  16195  bitsf1ocnv  16407  prmreclem6  16886  prmrec  16887  modxai  17033  strfvn  17150  strss  17170  xpsvsca  17535  mreacs  17618  2oppccomf  17685  setc2obas  18055  setc2ohom  18056  cat1  18058  chnflenfi  18588  chninf  18595  mndprop  18722  grpprop  18922  isgrpi  18929  oppgmndb  19324  oppggrpb  19327  odfval  19501  efgrelexlemb  19719  ablprop  19762  ringprop  20265  opprrngb  20320  opprringb  20322  rlmbas  21183  rlmplusg  21184  rlm0  21185  rlmsub  21186  rlmmulr  21187  rlmsca2  21189  rlmvsca  21190  rlmtopn  21191  rlmds  21192  rlmvneg  21196  dfcnfldOLD  21363  cncrng  21381  cncrngOLD  21382  xrsmcmn  21384  cndrng  21391  cndrngOLD  21392  cnsrng  21398  absabv  21417  xrs1mnd  21433  xrs10  21434  zringcyg  21462  pzriprngALT  21488  resrng  21614  psrbagsn  22054  evlsval  22077  psr1bas2  22166  psr1bas  22167  psr1plusg  22197  psr1vsca  22198  psr1mulr  22199  ply1plusgfvi  22218  ply1mpl0  22233  ply1mpl1  22235  ordtrestixx  23200  llyidm  23466  nllyidm  23467  toplly  23468  hauslly  23470  hausnlly  23471  lly1stc  23474  kgenf  23519  txswaphmeolem  23782  fmucndlem  24268  nrgtrg  24668  cnfldnm  24756  xrsxmet  24788  divcn  24848  expcn  24852  elcncf1ii  24876  iirevcn  24910  iihalf1cn  24912  iihalf2cn  24914  iimulcn  24918  icopnfcnv  24922  iccpnfcnv  24924  cnrehmeo  24933  tcphsub  25201  tcphphl  25207  iscmet3i  25292  cncmet  25302  rrxprds  25369  vitali  25593  i1f0  25667  itg20  25717  cbvitgv  25757  dvid  25898  dveflem  25959  dvef  25960  dvsincos  25961  ply1divalg2  26117  coe0  26234  iaa  26305  sincn  26425  coscn  26426  reefgim  26431  pilem3  26434  resinf1o  26516  circgrp  26532  circsubm  26533  logi  26567  divlogrlim  26615  dvrelog  26617  logcn  26627  dvlog  26631  advlog  26634  cxpcn  26725  cxpcn2  26726  resqrtcn  26729  sqrtcn  26730  atansopn  26912  dvatan  26915  leibpilem2  26921  leibpi  26922  leibpisum  26923  log2cnv  26924  log2ublem2  26927  log2ub  26929  divsqrtsumlem  26960  emcllem4  26979  emcllem6  26981  emcllem7  26982  lgamf  27022  lgam1  27044  basellem6  27066  basellem7  27067  basellem8  27068  basellem9  27069  vmaf  27099  logfacrlim  27204  lgsdir2lem5  27309  chebbnd1  27452  chtppilim  27455  chto1ub  27456  chebbnd2  27457  chto1lb  27458  chpchtlim  27459  chpo1ub  27460  chpo1ubb  27461  vmadivsum  27462  vmadivsumb  27463  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  logdivsum  27513  vmalogdivsum2  27518  vmalogdivsum  27519  selberglem1  27525  selberglem2  27526  selbergb  27529  selberg2lem  27530  selberg2  27531  selberg2b  27532  selberg3lem2  27538  selberg3  27539  selberg4  27541  pntrmax  27544  pntrsumo1  27545  pntrsumbnd  27546  selbergr  27548  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntrlog2bndlem1  27557  pntrlog2bndlem4  27560  pnt2  27593  pnt  27594  dmcuts  27800  lrrecpo  27950  noxpordpo  27959  noxpordfr  27960  noxpordse  27961  n0ssno  28329  0n0s  28338  n0cut  28343  n0sge0  28347  zseo  28431  twocut  28432  nohalf  28433  halfcut  28467  bdaypw2n0bndlem  28472  0reno  28505  1reno  28506  istrkg2ld  28545  legval  28669  ttgsub  28964  cchhllem  28972  2wspdisj  30051  2wspiundisj  30052  konigsbergiedgw  30336  ipasslem7  30925  normlem6  31204  opsqrlem4  32232  fpwrelmap  32824  fpwrelmapffs  32825  sgn3da  32925  xrs0  33084  elrgspnlem2  33322  1fldgenq  33401  dfprm3  33631  zringfrac  33632  ccfldsrarelvec  33834  ccfldextdgrr  33835  constrextdg2  33912  iconstr  33929  constrsdrg  33938  2sqr3minply  33943  2sqr3nconstr  33944  cos9thpiminplylem3  33947  cos9thpiminply  33951  cos9thpinconstrlem1  33952  cos9thpinconstrlem2  33953  mdetlap1  33989  circtopn  34000  cnre2csqima  34074  cnvordtrestixx  34076  mndpluscn  34089  xrge0iifcnv  34096  zlm0  34123  zlm1  34124  qqhre  34183  rrhre  34184  esumnul  34211  hasheuni  34248  sxbrsigalem2  34449  oddpwdc  34517  eulerpartlemb  34531  eulerpartgbij  34535  eulerpartlemn  34544  fib0  34562  fib1  34563  ballotlemrinv  34697  signsw0g  34719  circlemethnat  34804  dvelimalcasei  35237  dvelimexcasei  35239  subfacval2  35388  sinccvglem  35873  circum  35875  antnest  35890  antnestALT  35895  faclim  35947  faclim2  35949  cnndvlem1  36816  bj-alextruim  36950  bj-dvelimv  37179  bj-inrab2  37254  bj-rabtrAUTO  37258  bj-opelidb  37485  bj-iomnnom  37592  sucneqoni  37699  wl-df-3xor  37801  wl-3xorbi123i  37809  wl-df3maxtru1  37825  wl-cbvalnae  37875  wl-equsal  37883  poimirlem30  37988  dvtan  38008  dvasin  38042  dvacos  38043  dvreasin  38044  dvreacos  38045  efald2  38416  lcmineqlem7  42491  3lexlogpow5ineq1  42510  3lexlogpow5ineq5  42516  aks4d1p1p6  42529  cxpi11d  42792  tan3rdpi  42801  asin1half  42806  redvmptabs  42809  readvrec2  42810  readvrec  42811  resuppsinopn  42812  readvcot  42813  re1m1e0m0  42846  re0m0e0  42851  reixi  42872  subresre  42880  3cubeslem4  43138  3cubes  43139  areaquad  43665  clsk1indlem4  44492  clsk1indlem1  44493  ismnushort  44749  lhe4.4ex1a  44777  sbtT  45015  eel0TT  45151  eelTTT  45153  eelT1  45155  eelTT  45218  eelT  45220  eelT0  45222  isosctrlem1ALT  45381  disjsnxp  45522  infxr  45817  nfxneg  45910  limsup0  46143  0cnv  46191  limsup10ex  46222  liminf10ex  46223  liminfvalxr  46232  liminf0  46242  dvsinax  46362  itgsin0pilem1  46399  iblempty  46414  stowei  46513  wallispilem5  46518  wallispi  46519  stirlinglem1  46523  stirlinglem12  46534  stirlinglem13  46535  stirlinglem14  46536  stirlingr  46539  dirkertrigeqlem1  46547  fourierdlem62  46617  fourierdlem73  46628  fourierdlem76  46631  fourierdlem77  46632  fourierdlem103  46658  fourierdlem104  46659  fourierclim  46673  fourier  46674  fouriersw  46680  etransclem41  46724  etransclem46  46729  salexct2  46788  salexct3  46791  salgencntex  46792  salgensscntex  46793  dmvolsal  46795  bor1sal  46804  iocborel  46805  sge00  46825  sge0sn  46828  ovolval5lem3  47103  ioosshoi  47118  vonioolem2  47130  smfmullem4  47243  nthrucw  47335  goldrasin  47347  goldrapos  47348  cjnpoly  47352  dfafv2  47595  ichim  47932  grlimedgnedg  48622  nelsubc3  49561  fucofulem2  49801  setc2othin  49956  setcsnterm  49980  setc1obas  49982  setc1ohomfval  49983  setc1ocofval  49984  setc1oid  49985  termc2  50008  setc1onsubc  50092  onsetrec  50198  joinlmuladdmuli  50263