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

This theorem is referenced by:  hadbi123i  1598  cadbi123i  1613  nfan  1903  nfbi  1907  spimefv  2192  spime  2389  nfsb  2523  nfmov  2555  nfmo  2557  nfeuw  2588  nfeu  2589  eqabi  2870  eqabri  2878  nfeq  2917  nfel  2918  dvelimc  2932  nfralwOLD  3310  nfrexw  3311  nfral  3371  nfrex  3372  nfreuwOLD  3423  nfrmowOLD  3424  nfrmo  3431  nfreu  3432  rabbia2  3436  rabeqc  3445  nfrabw  3469  nfrabwOLD  3470  nfrab  3473  reuxfr  3746  reuxfr1  3749  nfsbc1  3797  nfsbcw  3800  nfsbc  3803  sbcbii  3838  csbeq2i  3902  nfcsb1  3918  nfcsbw  3921  nfcsb  3922  eqri  4003  vn0  4339  nfif  4559  nfdisjw  5126  nfdisj  5127  nfbr  5196  nfopab  5218  mpteq1i  5245  mpteq2ia  5252  mpteq12i  5255  ralxfr  5413  issoi  5623  nfiotaw  6500  nfiota  6502  nfriota  7378  nfov  7439  mpoeq123i  7485  mpoeq3ia  7487  opco1i  8111  xpord2indlem  8133  dfwrecsOLD  8298  on2recsfn  8666  on2recsov  8667  iseri  8730  nfixpw  8910  nfixp  8911  en2i  8986  en3i  8987  ensymb  8998  entr  9002  1sdom2dom  9247  nfttrcl  9706  djulf1o  9907  djurf1o  9908  r0weon  10007  recmulnq  10959  nrex1  11059  nfneg  11456  negiso  12194  suprzcl2  12922  supxr  13292  xrinf0  13317  fac0  14236  cnrecnv  15112  cau3  15302  cbvsum  15641  sum0  15667  ackbijnn  15774  flo1  15800  trireciplem  15808  trirecip  15809  ege2le3  16033  rpnnen2lem3  16159  ruclem4  16177  bitsf1ocnv  16385  prmreclem6  16854  prmrec  16855  modxai  17001  strfvn  17119  strss  17140  xpsvsca  17523  mreacs  17602  2oppccomf  17671  setc2obas  18044  setc2ohom  18045  cat1  18047  mndprop  18651  grpprop  18838  isgrpi  18845  oppgmndb  19222  oppggrpb  19225  odfval  19400  efgrelexlemb  19618  ablprop  19661  ringprop  20104  opprringb  20162  rlmbas  20817  rlmplusg  20818  rlm0  20819  rlmsub  20820  rlmmulr  20821  rlmsca2  20823  rlmvsca  20824  rlmtopn  20825  rlmds  20826  rlmvneg  20830  cncrng  20966  xrsmcmn  20968  cndrng  20974  cnsrng  20979  xrs1mnd  20983  xrs10  20984  absabv  21002  zringcyg  21039  resrng  21174  psrbagsn  21624  evlsval  21649  psr1bas2  21714  psr1bas  21715  psr1plusg  21744  psr1vsca  21745  psr1mulr  21746  ply1plusgfvi  21764  ply1mpl0  21777  ply1mpl1  21779  ordtrestixx  22726  llyidm  22992  nllyidm  22993  toplly  22994  hauslly  22996  hausnlly  22997  lly1stc  23000  kgenf  23045  txswaphmeolem  23308  fmucndlem  23796  nrgtrg  24207  cnfldnm  24295  xrsxmet  24325  divcn  24384  expcn  24388  elcncf1ii  24412  iirevcn  24446  iihalf1cn  24448  iihalf2cn  24450  iimulcn  24454  icopnfcnv  24458  iccpnfcnv  24460  cnrehmeo  24469  tcphsub  24738  tcphphl  24744  iscmet3i  24829  cncmet  24839  rrxprds  24906  vitali  25130  i1f0  25204  itg20  25255  dvid  25435  dveflem  25496  dvef  25497  dvsincos  25498  ply1divalg2  25656  coe0  25770  iaa  25838  sincn  25956  coscn  25957  reefgim  25962  pilem3  25965  resinf1o  26045  circgrp  26061  circsubm  26062  divlogrlim  26143  dvrelog  26145  logcn  26155  dvlog  26159  advlog  26162  cxpcn  26253  cxpcn2  26254  resqrtcn  26257  sqrtcn  26258  atansopn  26437  dvatan  26440  leibpilem2  26446  leibpi  26447  leibpisum  26448  log2cnv  26449  log2ublem2  26452  log2ub  26454  divsqrtsumlem  26484  emcllem4  26503  emcllem6  26505  emcllem7  26506  lgamf  26546  lgam1  26568  basellem6  26590  basellem7  26591  basellem8  26592  basellem9  26593  vmaf  26623  logfacrlim  26727  lgsdir2lem5  26832  chebbnd1  26975  chtppilim  26978  chto1ub  26979  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ub  26983  chpo1ubb  26984  vmadivsum  26985  vmadivsumb  26986  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  logdivsum  27036  vmalogdivsum2  27041  vmalogdivsum  27042  selberglem1  27048  selberglem2  27049  selbergb  27052  selberg2lem  27053  selberg2  27054  selberg2b  27055  selberg3lem2  27061  selberg3  27062  selberg4  27064  pntrmax  27067  pntrsumo1  27068  pntrsumbnd  27069  selbergr  27071  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntrlog2bndlem1  27080  pntrlog2bndlem4  27083  pnt2  27116  pnt  27117  dmscut  27313  lrrecpo  27427  noxpordpo  27436  noxpordfr  27437  noxpordse  27438  n0scut  27707  istrkg2ld  27742  legval  27866  ttgsub  28165  cchhllem  28175  cchhllemOLD  28176  2wspdisj  29247  2wspiundisj  29248  konigsbergiedgw  29532  ipasslem7  30120  normlem6  30399  opsqrlem4  31427  fpwrelmap  31989  fpwrelmapffs  31990  xrs0  32207  1fldgenq  32443  ccfldsrarelvec  32776  ccfldextdgrr  32777  mdetlap1  32837  circtopn  32848  cnre2csqima  32922  cnvordtrestixx  32924  mndpluscn  32937  xrge0iifcnv  32944  zlm0  32971  zlm1  32972  qqhre  33031  rrhre  33032  esumnul  33077  hasheuni  33114  sxbrsigalem2  33316  oddpwdc  33384  eulerpartlemb  33398  eulerpartgbij  33402  eulerpartlemn  33411  fib0  33429  fib1  33430  ballotlemrinv  33563  sgn3da  33571  signsw0g  33598  circlemethnat  33684  subfacval2  34209  sinccvglem  34688  circum  34690  logi  34735  faclim  34747  faclim2  34749  gg-divcn  35194  gg-expcn  35195  gg-iihalf1cn  35198  gg-iihalf2cn  35199  gg-iimulcn  35200  gg-cnrehmeo  35202  gg-cxpcn  35215  gg-dfcnfld  35218  gg-cncrng  35231  cnndvlem1  35461  bj-dvelimv  35780  bj-inrab2  35856  bj-rabtrAUTO  35860  bj-opelidb  36081  bj-iomnnom  36188  sucneqoni  36295  wl-df-3xor  36397  wl-3xorbi123i  36405  wl-df3maxtru1  36421  wl-cbvalnae  36450  wl-equsal  36457  poimirlem30  36566  dvtan  36586  dvasin  36620  dvacos  36621  dvreasin  36622  dvreacos  36623  efald2  36994  lcmineqlem7  40948  3lexlogpow5ineq1  40967  3lexlogpow5ineq5  40973  aks4d1p1p6  40986  re1m1e0m0  41318  re0m0e0  41323  reixi  41343  subresre  41351  3cubeslem4  41475  3cubes  41476  areaquad  42013  clsk1indlem4  42843  clsk1indlem1  42844  ismnushort  43108  lhe4.4ex1a  43136  sbtT  43376  eel0TT  43513  eelTTT  43515  eelT1  43517  eelTT  43580  eelT  43582  eelT0  43584  isosctrlem1ALT  43743  disjsnxp  43805  infxr  44125  nfxneg  44219  limsup0  44458  0cnv  44506  limsup10ex  44537  liminf10ex  44538  liminfvalxr  44547  liminf0  44557  dvsinax  44677  itgsin0pilem1  44714  iblempty  44729  stowei  44828  wallispilem5  44833  wallispi  44834  stirlinglem1  44838  stirlinglem12  44849  stirlinglem13  44850  stirlinglem14  44851  stirlingr  44854  dirkertrigeqlem1  44862  fourierdlem62  44932  fourierdlem73  44943  fourierdlem76  44946  fourierdlem77  44947  fourierdlem103  44973  fourierdlem104  44974  fourierclim  44988  fourier  44989  fouriersw  44995  etransclem41  45039  etransclem46  45044  salexct2  45103  salexct3  45106  salgencntex  45107  salgensscntex  45108  dmvolsal  45110  bor1sal  45119  iocborel  45120  sge00  45140  sge0sn  45143  ovolval5lem3  45418  ioosshoi  45433  vonioolem2  45445  smfmullem4  45558  upwrdfi  45649  dfafv2  45888  ichim  46173  opprrngb  46723  pzriprngALT  46867  setc2othin  47724  onsetrec  47801  joinlmuladdmuli  47868