Theorem mptru 1577

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1573

This theorem is used by:  hadbi123i  1626  cadbi123i  1644  nfan  1934  nfbi  1938  spimefv  2238  spime  2421  nfsb  2555  nfmov  2588  nfmo  2590  nfeuw  2621  nfeu  2622  eqabi  2899  eqabri  2906  nfeq  2939  nfel  2940  dvelimc  2951  nfrexw  3314  nfral  3363  nfrex  3364  nfrmo  3414  nfreu  3415  rabbia2  3419  rabeqc  3428  nfrab  3452  reuxfr  3710  reuxfr1  3713  nfsbc1  3761  nfsbcw  3764  nfsbc  3767  sbcbii  3798  csbeq2i  3859  nfcsb1  3874  nfcsbw  3877  nfcsb  3878  eqri  3933  ss2abi  3994  ss2rabi  4004  nfif  4516  nfdisjw  5087  nfdisj  5088  nfbr  5158  nfopab  5180  mpteq1i  5202  mpteq2ia  5206  mpteq12i  5208  ralxfr  5383  issoi  5602  nfiotaw  6524  nfiota  6526  nfriota  7420  nfov  7481  mpoeq123i  7527  mpoeq3ia  7529  opco1i  8173  xpord2indlem  8201  on2recsfn  8714  on2recsov  8715  iseri  8783  nfixpw  8982  nfixp  8983  en2i  9055  en3i  9056  ensymb  9067  entr  9071  1sdom2dom  9283  nfttrcl  9749  djulf1o  10030  djurf1o  10031  r0weon  10130  recmulnq  11088  nrex1  11188  nfneg  11592  negiso  12337  suprzcl2  13105  supxr  13483  xrinf0  13509  fac0  14461  sgn3da  15297  cnrecnv  15375  cau3  15567  cbvsum  15906  cbvsumv  15907  sum0  15931  ackbijnn  16041  flo1  16067  trireciplem  16075  trirecip  16076  ege2le3  16300  rpnnen2lem3  16428  ruclem4  16446  bitsf1ocnv  16658  prmreclem6  17143  prmrec  17144  modxai  17290  strfvn  17408  strss  17428  xpsvsca  17799  mreacs  17882  2oppccomf  17949  setc2obas  18319  setc2ohom  18320  cat1  18322  chnflenfi  18852  chninf  18859  mndprop  19002  grpprop  19213  isgrpi  19220  oppgmndb  19620  oppggrpb  19623  odfval  19797  efgrelexlemb  20015  ablprop  20058  ringprop  20572  opprrngb  20627  opprringb  20629  rlmbas  21519  rlmplusg  21520  rlm0  21521  rlmsub  21522  rlmmulr  21523  rlmsca2  21525  rlmvsca  21526  rlmtopn  21527  rlmds  21528  rlmvneg  21532  cncrng  21751  xrsmcmn  21753  cndrng  21759  cnsrng  21764  absabv  21784  xrs1mnd  21800  xrs10  21801  zringcyg  21830  pzriprngALT  21856  resrng  21982  psrbagsn  22427  evlsval  22450  psr1bas2  22563  psr1bas  22564  psr1plusg  22593  psr1vsca  22594  psr1mulr  22595  ply1plusgfvi  22614  ply1mpl0  22629  ply1mpl1  22631  ordtrestixx  23595  llyidm  23862  nllyidm  23863  toplly  23864  hauslly  23866  hausnlly  23867  lly1stc  23870  kgenf  23915  txswaphmeolem  24178  fmucndlem  24664  nrgtrg  25064  cnfldnm  25152  xrsxmet  25184  divcn  25244  expcn  25248  elcncf1ii  25272  iirevcn  25306  iihalf1cn  25308  iihalf2cn  25310  iimulcn  25314  icopnfcnv  25318  iccpnfcnv  25320  cnrehmeo  25329  tcphsub  25597  tcphphl  25603  iscmet3i  25688  cncmet  25698  rrxprds  25765  vitali  25989  i1f0  26063  itg20  26113  cbvitgv  26152  dvid  26293  dveflem  26354  dvef  26355  dvsincos  26356  ply1divalg2  26512  coe0  26630  iaa  26708  iaaOLD  26709  sincn  26828  coscn  26829  reefgim  26834  pilem3  26837  resinf1o  26921  circgrp  26937  circsubm  26938  logi  26972  divlogrlim  27020  dvrelog  27022  logcn  27032  dvlog  27036  advlog  27039  cxpcn  27130  cxpcn2  27131  resqrtcn  27134  sqrtcn  27135  atansopn  27317  dvatan  27320  leibpilem2  27326  leibpi  27327  leibpisum  27328  log2cnv  27329  log2ublem2  27332  log2ub  27334  divsqrtsumlem  27364  emcllem4  27383  emcllem6  27385  emcllem7  27386  lgamf  27426  lgam1  27448  basellem6  27470  basellem7  27471  basellem8  27472  basellem9  27473  vmaf  27503  logfacrlim  27608  lgsdir2lem5  27713  chebbnd1  27856  chtppilim  27859  chto1ub  27860  chebbnd2  27861  chto1lb  27862  chpchtlim  27863  chpo1ub  27864  chpo1ubb  27865  vmadivsum  27866  vmadivsumb  27867  mudivsum  27914  mulogsumlem  27915  mulogsum  27916  logdivsum  27917  vmalogdivsum2  27922  vmalogdivsum  27923  selberglem1  27929  selberglem2  27930  selbergb  27933  selberg2lem  27934  selberg2  27935  selberg2b  27936  selberg3lem2  27942  selberg3  27943  selberg4  27945  pntrmax  27948  pntrsumo1  27949  pntrsumbnd  27950  selbergr  27952  selberg3r  27953  selberg4r  27954  selberg34r  27955  pntrlog2bndlem1  27961  pntrlog2bndlem4  27964  pnt2  27997  pnt  27998  dmcuts  28234  lrrecpo  28384  noxpordpo  28393  noxpordfr  28394  noxpordse  28395  n0ssno  28763  0n0s  28772  n0cut  28777  n0sge0  28781  zseo  28865  twocut  28866  nohalf  28867  halfcut  28901  bdaypw2n0bndlem  28906  0reno  28939  1reno  28940  istrkg2ld  28979  legval  29104  ttgsub  29513  cchhllem  29521  2wspdisj  30611  2wspiundisj  30612  konigsbergiedgw  30906  ipasslem7  31495  normlem6  31774  opsqrlem4  32802  fpwrelmap  33421  fpwrelmapffs  33422  xrs0  33666  elrgspnlem2  33903  zzedom  33958  1fldgenq  33988  dfprm3  34188  zringfrac  34189  0mplrim  34257  ccfldsrarelvec  34414  ccfldextdgrr  34415  constrextdg2  34492  iconstr  34509  constrsdrg  34518  2sqr3minply  34523  2sqr3nconstr  34524  cos9thpiminplylem3  34527  cos9thpiminply  34531  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  mdetlap1  34569  circtopn  34580  cnre2csqima  34654  cnvordtrestixx  34656  mndpluscn  34669  xrge0iifcnv  34676  zlm0  34703  zlm1  34704  qqhre  34763  rrhre  34764  esumnul  34791  hasheuni  34828  sxbrsigalem2  35029  oddpwdc  35097  eulerpartlemb  35111  eulerpartgbij  35115  eulerpartlemn  35124  fib0  35142  fib1  35143  ballotlemrinv  35277  signsw0g  35296  circlemethnat  35381  dvelimalcasei  35817  dvelimexcasei  35819  dfscott3  35868  kard0  35963  subfacval2  36160  sinccvglem  36645  circum  36647  antnest  36662  antnestALT  36667  faclim  36726  faclim2  36728  cnndvlem1  37618  bj-alextruim  37751  bj-dvelimv  37980  bj-inrab2  38056  bj-rabtrAUTO  38060  bj-opelidb  38341  bj-iomnnom  38448  sucneqoni  38557  wl-df-3xor  38659  wl-3xorbi123i  38667  wl-df3maxtru1  38683  wl-cbvalnae  38733  wl-equsal  38741  poimirlem30  38836  dvtan  38856  dvasin  38890  dvacos  38891  dvreasin  38892  dvreacos  38893  dfprop2  38914  efald2  39278  lcmineqlem7  43351  3lexlogpow5ineq1  43370  3lexlogpow5ineq5  43376  aks4d1p1p6  43389  cxpi11d  43660  tan3rdpi  43669  asin1half  43674  redvmptabs  43677  readvrec2  43678  readvrec  43679  resuppsinopn  43680  readvcot  43681  re1m1e0m0  43714  re0m0e0  43719  reixi  43740  subresre  43748  3cubeslem4  43965  3cubes  43966  areaquad  44479  clsk1indlem4  45305  clsk1indlem1  45306  ismnushort  45546  lhe4.4ex1a  45574  sbtT  45810  eel0TT  45946  eelTTT  45948  eelT1  45950  eelTT  46013  eelT  46015  eelT0  46017  isosctrlem1ALT  46176  disjsnxp  46361  infxr  46651  nfxneg  46744  limsup0  46977  0cnv  47025  limsup10ex  47056  liminf10ex  47057  liminfvalxr  47066  liminf0  47076  dvsinax  47196  itgsin0pilem1  47233  iblempty  47248  stowei  47347  wallispilem5  47352  wallispi  47353  stirlinglem1  47357  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  stirlingr  47373  dirkertrigeqlem1  47381  fourierdlem62  47451  fourierdlem73  47462  fourierdlem76  47465  fourierdlem77  47466  fourierdlem103  47492  fourierdlem104  47493  fourierclim  47507  fourier  47508  fouriersw  47514  etransclem41  47558  etransclem46  47563  salexct2  47622  salexct3  47625  salgencntex  47626  salgensscntex  47627  dmvolsal  47629  bor1sal  47638  iocborel  47639  sge00  47659  sge0sn  47662  ovolval5lem3  47937  ioosshoi  47952  vonioolem2  47964  smfmullem4  48077  numtowerdt  48189  goldpolyfactor  48200  goldrasin  48202  goldrapos  48203  goldratval  48209  cjnpoly  48212  dfafv2  48475  ichim  48812  grlimedgnedg  49502  rrx2xpref1o  50162  nelsubc3  50516  fucofulem2  50764  fucoisfunc2lem1  50819  setc2othin  50932  setcsnterm  50956  setc1obas  50958  setc1ohomfval  50959  setc1ocofval  50960  setc1oid  50961  termc2  50984  setc1onsubc  51071  parcatid2  51094  parcatid  51095  parmapfunc2  51105  parmapfunc  51106  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114  onsetrec  51207  dvsec  51284  dvcsc  51285  dvcot  51286  joinlmuladdmuli  51297