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  1932  nfbi  1936  spimefv  2235  spime  2419  nfsb  2553  nfmov  2586  nfmo  2588  nfeuw  2619  nfeu  2620  eqabi  2896  eqabri  2903  nfeq  2936  nfel  2937  dvelimc  2948  nfrexw  3311  nfral  3360  nfrex  3361  nfrmo  3411  nfreu  3412  rabbia2  3416  rabeqc  3425  nfrab  3449  reuxfr  3707  reuxfr1  3710  nfsbc1  3758  nfsbcw  3761  nfsbc  3764  sbcbii  3795  csbeq2i  3855  nfcsb1  3870  nfcsbw  3873  nfcsb  3874  eqri  3951  ss2abi  4014  ss2rabi  4024  nfif  4513  nfdisjw  5082  nfdisj  5083  nfbr  5152  nfopab  5174  mpteq1i  5196  mpteq2ia  5200  mpteq12i  5202  ralxfr  5376  issoi  5595  nfiotaw  6497  nfiota  6499  nfriota  7387  nfov  7448  mpoeq123i  7494  mpoeq3ia  7496  opco1i  8134  xpord2indlem  8157  on2recsfn  8669  on2recsov  8670  iseri  8738  nfixpw  8937  nfixp  8938  en2i  9010  en3i  9011  ensymb  9022  entr  9026  1sdom2dom  9238  nfttrcl  9705  djulf1o  9986  djurf1o  9987  r0weon  10084  recmulnq  11042  nrex1  11142  nfneg  11546  negiso  12290  suprzcl2  13058  supxr  13436  xrinf0  13462  fac0  14413  sgn3da  15247  cnrecnv  15325  cau3  15516  cbvsum  15855  cbvsumv  15856  sum0  15880  ackbijnn  15990  flo1  16016  trireciplem  16024  trirecip  16025  ege2le3  16249  rpnnen2lem3  16377  ruclem4  16395  bitsf1ocnv  16607  prmreclem6  17092  prmrec  17093  modxai  17239  strfvn  17357  strss  17377  xpsvsca  17742  mreacs  17825  2oppccomf  17892  setc2obas  18262  setc2ohom  18263  cat1  18265  chnflenfi  18795  chninf  18802  mndprop  18945  grpprop  19156  isgrpi  19163  oppgmndb  19562  oppggrpb  19565  odfval  19739  efgrelexlemb  19957  ablprop  20000  ringprop  20514  opprrngb  20569  opprringb  20571  rlmbas  21461  rlmplusg  21462  rlm0  21463  rlmsub  21464  rlmmulr  21465  rlmsca2  21467  rlmvsca  21468  rlmtopn  21469  rlmds  21470  rlmvneg  21474  cncrng  21692  xrsmcmn  21694  cndrng  21700  cnsrng  21705  absabv  21723  xrs1mnd  21739  xrs10  21740  zringcyg  21768  pzriprngALT  21794  resrng  21920  psrbagsn  22365  evlsval  22388  psr1bas2  22501  psr1bas  22502  psr1plusg  22531  psr1vsca  22532  psr1mulr  22533  ply1plusgfvi  22552  ply1mpl0  22567  ply1mpl1  22569  ordtrestixx  23533  llyidm  23800  nllyidm  23801  toplly  23802  hauslly  23804  hausnlly  23805  lly1stc  23808  kgenf  23853  txswaphmeolem  24116  fmucndlem  24602  nrgtrg  25002  cnfldnm  25090  xrsxmet  25122  divcn  25182  expcn  25186  elcncf1ii  25210  iirevcn  25244  iihalf1cn  25246  iihalf2cn  25248  iimulcn  25252  icopnfcnv  25256  iccpnfcnv  25258  cnrehmeo  25267  tcphsub  25535  tcphphl  25541  iscmet3i  25626  cncmet  25636  rrxprds  25703  vitali  25927  i1f0  26001  itg20  26051  cbvitgv  26090  dvid  26231  dveflem  26292  dvef  26293  dvsincos  26294  ply1divalg2  26450  coe0  26568  iaa  26644  iaaOLD  26645  sincn  26764  coscn  26765  reefgim  26770  pilem3  26773  resinf1o  26857  circgrp  26873  circsubm  26874  logi  26908  divlogrlim  26956  dvrelog  26958  logcn  26968  dvlog  26972  advlog  26975  cxpcn  27066  cxpcn2  27067  resqrtcn  27070  sqrtcn  27071  atansopn  27253  dvatan  27256  leibpilem2  27262  leibpi  27263  leibpisum  27264  log2cnv  27265  log2ublem2  27268  log2ub  27270  divsqrtsumlem  27300  emcllem4  27319  emcllem6  27321  emcllem7  27322  lgamf  27362  lgam1  27384  basellem6  27406  basellem7  27407  basellem8  27408  basellem9  27409  vmaf  27439  logfacrlim  27544  lgsdir2lem5  27649  chebbnd1  27792  chtppilim  27795  chto1ub  27796  chebbnd2  27797  chto1lb  27798  chpchtlim  27799  chpo1ub  27800  chpo1ubb  27801  vmadivsum  27802  vmadivsumb  27803  mudivsum  27850  mulogsumlem  27851  mulogsum  27852  logdivsum  27853  vmalogdivsum2  27858  vmalogdivsum  27859  selberglem1  27865  selberglem2  27866  selbergb  27869  selberg2lem  27870  selberg2  27871  selberg2b  27872  selberg3lem2  27878  selberg3  27879  selberg4  27881  pntrmax  27884  pntrsumo1  27885  pntrsumbnd  27886  selbergr  27888  selberg3r  27889  selberg4r  27890  selberg34r  27891  pntrlog2bndlem1  27897  pntrlog2bndlem4  27900  pnt2  27933  pnt  27934  dmcuts  28170  lrrecpo  28320  noxpordpo  28329  noxpordfr  28330  noxpordse  28331  n0ssno  28699  0n0s  28708  n0cut  28713  n0sge0  28717  zseo  28801  twocut  28802  nohalf  28803  halfcut  28837  bdaypw2n0bndlem  28842  0reno  28875  1reno  28876  istrkg2ld  28915  legval  29040  ttgsub  29449  cchhllem  29457  2wspdisj  30547  2wspiundisj  30548  konigsbergiedgw  30842  ipasslem7  31431  normlem6  31710  opsqrlem4  32738  fpwrelmap  33318  fpwrelmapffs  33319  xrs0  33560  elrgspnlem2  33797  1fldgenq  33877  dfprm3  34078  zringfrac  34079  0mplrim  34139  ccfldsrarelvec  34296  ccfldextdgrr  34297  constrextdg2  34374  iconstr  34391  constrsdrg  34400  2sqr3minply  34405  2sqr3nconstr  34406  cos9thpiminplylem3  34409  cos9thpiminply  34413  cos9thpinconstrlem1  34414  cos9thpinconstrlem2  34415  mdetlap1  34451  circtopn  34462  cnre2csqima  34536  cnvordtrestixx  34538  mndpluscn  34551  xrge0iifcnv  34558  zlm0  34585  zlm1  34586  qqhre  34645  rrhre  34646  esumnul  34673  hasheuni  34710  sxbrsigalem2  34911  oddpwdc  34979  eulerpartlemb  34993  eulerpartgbij  34997  eulerpartlemn  35006  fib0  35024  fib1  35025  ballotlemrinv  35159  signsw0g  35178  circlemethnat  35263  dvelimalcasei  35699  dvelimexcasei  35701  dfscott3  35731  kard0  35805  subfacval2  35931  sinccvglem  36416  circum  36418  antnest  36433  antnestALT  36438  faclim  36490  faclim2  36492  cnndvlem1  37383  bj-alextruim  37516  bj-dvelimv  37745  bj-inrab2  37821  bj-rabtrAUTO  37825  bj-opelidb  38053  bj-iomnnom  38160  sucneqoni  38269  wl-df-3xor  38371  wl-3xorbi123i  38379  wl-df3maxtru1  38395  wl-cbvalnae  38445  wl-equsal  38453  poimirlem30  38548  dvtan  38568  dvasin  38602  dvacos  38603  dvreasin  38604  dvreacos  38605  dfprop2  38626  efald2  38992  lcmineqlem7  43065  3lexlogpow5ineq1  43084  3lexlogpow5ineq5  43090  aks4d1p1p6  43103  cxpi11d  43374  tan3rdpi  43383  asin1half  43388  redvmptabs  43391  readvrec2  43392  readvrec  43393  resuppsinopn  43394  readvcot  43395  re1m1e0m0  43428  re0m0e0  43433  reixi  43454  subresre  43462  3cubeslem4  43679  3cubes  43680  areaquad  44202  clsk1indlem4  45029  clsk1indlem1  45030  ismnushort  45270  lhe4.4ex1a  45298  sbtT  45535  eel0TT  45671  eelTTT  45673  eelT1  45675  eelTT  45738  eelT  45740  eelT0  45742  isosctrlem1ALT  45901  disjsnxp  46056  infxr  46347  nfxneg  46440  limsup0  46673  0cnv  46721  limsup10ex  46752  liminf10ex  46753  liminfvalxr  46762  liminf0  46772  dvsinax  46892  itgsin0pilem1  46929  iblempty  46944  stowei  47043  wallispilem5  47048  wallispi  47049  stirlinglem1  47053  stirlinglem12  47064  stirlinglem13  47065  stirlinglem14  47066  stirlingr  47069  dirkertrigeqlem1  47077  fourierdlem62  47147  fourierdlem73  47158  fourierdlem76  47161  fourierdlem77  47162  fourierdlem103  47188  fourierdlem104  47189  fourierclim  47203  fourier  47204  fouriersw  47210  etransclem41  47254  etransclem46  47259  salexct2  47318  salexct3  47321  salgencntex  47322  salgensscntex  47323  dmvolsal  47325  bor1sal  47334  iocborel  47335  sge00  47355  sge0sn  47358  ovolval5lem3  47633  ioosshoi  47648  vonioolem2  47660  smfmullem4  47773  numtowerdt  47885  goldpolyfactor  47896  goldrasin  47898  goldrapos  47899  goldratval  47905  cjnpoly  47908  dfafv2  48171  ichim  48508  grlimedgnedg  49198  nelsubc3  50148  fucofulem2  50388  setc2othin  50543  setcsnterm  50567  setc1obas  50569  setc1ohomfval  50570  setc1ocofval  50571  setc1oid  50572  termc2  50595  setc1onsubc  50679  onsetrec  50770  dvsec  50825  dvcsc  50826  dvcot  50827  joinlmuladdmuli  50838