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  2234  spime  2418  nfsb  2552  nfmov  2585  nfmo  2587  nfeuw  2618  nfeu  2619  eqabi  2895  eqabri  2902  nfeq  2935  nfel  2936  dvelimc  2947  nfrexw  3310  nfral  3359  nfrex  3360  nfrmo  3410  nfreu  3411  rabbia2  3415  rabeqc  3424  nfrab  3448  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  5379  issoi  5599  nfiotaw  6493  nfiota  6495  nfriota  7382  nfov  7443  mpoeq123i  7489  mpoeq3ia  7491  opco1i  8122  xpord2indlem  8145  on2recsfn  8655  on2recsov  8656  iseri  8724  nfixpw  8923  nfixp  8924  en2i  8996  en3i  8997  ensymb  9008  entr  9012  1sdom2dom  9224  nfttrcl  9690  djulf1o  9917  djurf1o  9918  r0weon  10015  recmulnq  10973  nrex1  11073  nfneg  11477  negiso  12219  suprzcl2  12987  supxr  13365  xrinf0  13391  fac0  14340  sgn3da  15174  cnrecnv  15252  cau3  15443  cbvsum  15782  cbvsumv  15783  sum0  15807  ackbijnn  15917  flo1  15943  trireciplem  15951  trirecip  15952  ege2le3  16176  rpnnen2lem3  16304  ruclem4  16322  bitsf1ocnv  16534  prmreclem6  17013  prmrec  17014  modxai  17160  strfvn  17278  strss  17298  xpsvsca  17663  mreacs  17746  2oppccomf  17813  setc2obas  18183  setc2ohom  18184  cat1  18186  chnflenfi  18716  chninf  18723  mndprop  18865  grpprop  19076  isgrpi  19083  oppgmndb  19482  oppggrpb  19485  odfval  19659  efgrelexlemb  19877  ablprop  19920  ringprop  20432  opprrngb  20487  opprringb  20489  rlmbas  21377  rlmplusg  21378  rlm0  21379  rlmsub  21380  rlmmulr  21381  rlmsca2  21383  rlmvsca  21384  rlmtopn  21385  rlmds  21386  rlmvneg  21390  cncrng  21606  xrsmcmn  21608  cndrng  21614  cnsrng  21619  absabv  21637  xrs1mnd  21653  xrs10  21654  zringcyg  21682  pzriprngALT  21708  resrng  21834  psrbagsn  22279  evlsval  22302  psr1bas2  22415  psr1bas  22416  psr1plusg  22445  psr1vsca  22446  psr1mulr  22447  ply1plusgfvi  22466  ply1mpl0  22481  ply1mpl1  22483  ordtrestixx  23447  llyidm  23714  nllyidm  23715  toplly  23716  hauslly  23718  hausnlly  23719  lly1stc  23722  kgenf  23767  txswaphmeolem  24030  fmucndlem  24516  nrgtrg  24916  cnfldnm  25004  xrsxmet  25036  divcn  25096  expcn  25100  elcncf1ii  25124  iirevcn  25158  iihalf1cn  25160  iihalf2cn  25162  iimulcn  25166  icopnfcnv  25170  iccpnfcnv  25172  cnrehmeo  25181  tcphsub  25449  tcphphl  25455  iscmet3i  25540  cncmet  25550  rrxprds  25617  vitali  25841  i1f0  25915  itg20  25965  cbvitgv  26004  dvid  26145  dveflem  26206  dvef  26207  dvsincos  26208  ply1divalg2  26364  coe0  26482  iaa  26560  iaaOLD  26561  sincn  26680  coscn  26681  reefgim  26686  pilem3  26689  resinf1o  26773  circgrp  26789  circsubm  26790  logi  26824  divlogrlim  26872  dvrelog  26874  logcn  26884  dvlog  26888  advlog  26891  cxpcn  26982  cxpcn2  26983  resqrtcn  26986  sqrtcn  26987  atansopn  27169  dvatan  27172  leibpilem2  27178  leibpi  27179  leibpisum  27180  log2cnv  27181  log2ublem2  27184  log2ub  27186  divsqrtsumlem  27216  emcllem4  27235  emcllem6  27237  emcllem7  27238  lgamf  27278  lgam1  27300  basellem6  27322  basellem7  27323  basellem8  27324  basellem9  27325  vmaf  27355  logfacrlim  27460  lgsdir2lem5  27565  chebbnd1  27708  chtppilim  27711  chto1ub  27712  chebbnd2  27713  chto1lb  27714  chpchtlim  27715  chpo1ub  27716  chpo1ubb  27717  vmadivsum  27718  vmadivsumb  27719  mudivsum  27766  mulogsumlem  27767  mulogsum  27768  logdivsum  27769  vmalogdivsum2  27774  vmalogdivsum  27775  selberglem1  27781  selberglem2  27782  selbergb  27785  selberg2lem  27786  selberg2  27787  selberg2b  27788  selberg3lem2  27794  selberg3  27795  selberg4  27797  pntrmax  27800  pntrsumo1  27801  pntrsumbnd  27802  selbergr  27804  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntrlog2bndlem1  27813  pntrlog2bndlem4  27816  pnt2  27849  pnt  27850  dmcuts  28056  lrrecpo  28206  noxpordpo  28215  noxpordfr  28216  noxpordse  28217  n0ssno  28585  0n0s  28594  n0cut  28599  n0sge0  28603  zseo  28687  twocut  28688  nohalf  28689  halfcut  28723  bdaypw2n0bndlem  28728  0reno  28761  1reno  28762  istrkg2ld  28801  legval  28926  ttgsub  29335  cchhllem  29343  2wspdisj  30433  2wspiundisj  30434  konigsbergiedgw  30728  ipasslem7  31317  normlem6  31596  opsqrlem4  32624  fpwrelmap  33204  fpwrelmapffs  33205  xrs0  33446  elrgspnlem2  33683  1fldgenq  33763  dfprm3  33963  zringfrac  33964  0mplrim  34024  ccfldsrarelvec  34181  ccfldextdgrr  34182  constrextdg2  34259  iconstr  34276  constrsdrg  34285  2sqr3minply  34290  2sqr3nconstr  34291  cos9thpiminplylem3  34294  cos9thpiminply  34298  cos9thpinconstrlem1  34299  cos9thpinconstrlem2  34300  mdetlap1  34336  circtopn  34347  cnre2csqima  34421  cnvordtrestixx  34423  mndpluscn  34436  xrge0iifcnv  34443  zlm0  34470  zlm1  34471  qqhre  34530  rrhre  34531  esumnul  34558  hasheuni  34595  sxbrsigalem2  34797  oddpwdc  34865  eulerpartlemb  34879  eulerpartgbij  34883  eulerpartlemn  34892  fib0  34910  fib1  34911  ballotlemrinv  35045  signsw0g  35064  circlemethnat  35149  dvelimalcasei  35585  dvelimexcasei  35587  dfscott3  35626  kard0  35680  subfacval2  35766  sinccvglem  36251  circum  36253  antnest  36268  antnestALT  36273  faclim  36325  faclim2  36327  cnndvlem1  37234  bj-alextruim  37367  bj-dvelimv  37596  bj-inrab2  37672  bj-rabtrAUTO  37676  bj-opelidb  37904  bj-iomnnom  38011  sucneqoni  38120  wl-df-3xor  38222  wl-3xorbi123i  38230  wl-df3maxtru1  38246  wl-cbvalnae  38296  wl-equsal  38304  poimirlem30  38399  dvtan  38419  dvasin  38453  dvacos  38454  dvreasin  38455  dvreacos  38456  efald2  38828  lcmineqlem7  42901  3lexlogpow5ineq1  42920  3lexlogpow5ineq5  42926  aks4d1p1p6  42939  cxpi11d  43218  tan3rdpi  43227  asin1half  43232  redvmptabs  43235  readvrec2  43236  readvrec  43237  resuppsinopn  43238  readvcot  43239  re1m1e0m0  43272  re0m0e0  43277  reixi  43298  subresre  43306  3cubeslem4  43534  3cubes  43535  areaquad  44057  clsk1indlem4  44884  clsk1indlem1  44885  ismnushort  45125  lhe4.4ex1a  45153  sbtT  45390  eel0TT  45526  eelTTT  45528  eelT1  45530  eelTT  45593  eelT  45595  eelT0  45597  isosctrlem1ALT  45756  disjsnxp  45904  infxr  46196  nfxneg  46289  limsup0  46522  0cnv  46570  limsup10ex  46601  liminf10ex  46602  liminfvalxr  46611  liminf0  46621  dvsinax  46741  itgsin0pilem1  46778  iblempty  46793  stowei  46892  wallispilem5  46897  wallispi  46898  stirlinglem1  46902  stirlinglem12  46913  stirlinglem13  46914  stirlinglem14  46915  stirlingr  46918  dirkertrigeqlem1  46926  fourierdlem62  46996  fourierdlem73  47007  fourierdlem76  47010  fourierdlem77  47011  fourierdlem103  47037  fourierdlem104  47038  fourierclim  47052  fourier  47053  fouriersw  47059  etransclem41  47103  etransclem46  47108  salexct2  47167  salexct3  47170  salgencntex  47171  salgensscntex  47172  dmvolsal  47174  bor1sal  47183  iocborel  47184  sge00  47204  sge0sn  47207  ovolval5lem3  47482  ioosshoi  47497  vonioolem2  47509  smfmullem4  47622  numtowerdt  47734  goldpolyfactor  47745  goldrasin  47747  goldrapos  47748  goldratval  47754  cjnpoly  47757  dfafv2  48020  ichim  48357  grlimedgnedg  49047  nelsubc3  49997  fucofulem2  50237  setc2othin  50392  setcsnterm  50416  setc1obas  50418  setc1ohomfval  50419  setc1ocofval  50420  setc1oid  50421  termc2  50444  setc1onsubc  50528  onsetrec  50634  dvsec  50689  dvcsc  50690  dvcot  50691  joinlmuladdmuli  50702