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  2237  spime  2423  nfsb  2557  nfmov  2590  nfmo  2592  nfeuw  2623  nfeu  2624  eqabi  2900  eqabri  2907  nfeq  2940  nfel  2941  dvelimc  2952  nfrexw  3315  nfral  3365  nfrex  3366  nfrmo  3416  nfreu  3417  rabbia2  3421  rabeqc  3430  nfrab  3455  reuxfr  3714  reuxfr1  3717  nfsbc1  3765  nfsbcw  3768  nfsbc  3771  sbcbii  3802  csbeq2i  3862  nfcsb1  3877  nfcsbw  3880  nfcsb  3881  eqri  3958  ss2abi  4021  ss2rabi  4031  nfif  4520  nfdisjw  5090  nfdisj  5091  nfbr  5160  nfopab  5182  mpteq1i  5204  mpteq2ia  5208  mpteq12i  5210  ralxfr  5387  issoi  5607  nfiotaw  6500  nfiota  6502  nfriota  7388  nfov  7449  mpoeq123i  7495  mpoeq3ia  7497  opco1i  8126  xpord2indlem  8149  on2recsfn  8659  on2recsov  8660  iseri  8728  nfixpw  8920  nfixp  8921  en2i  8993  en3i  8994  ensymb  9005  entr  9009  1sdom2dom  9221  nfttrcl  9687  djulf1o  9914  djurf1o  9915  r0weon  10012  recmulnq  10964  nrex1  11064  nfneg  11468  negiso  12210  suprzcl2  12978  supxr  13355  xrinf0  13381  fac0  14330  sgn3da  15162  cnrecnv  15240  cau3  15431  cbvsum  15770  cbvsumv  15771  sum0  15795  ackbijnn  15905  flo1  15931  trireciplem  15939  trirecip  15940  ege2le3  16166  rpnnen2lem3  16294  ruclem4  16312  bitsf1ocnv  16524  prmreclem6  17003  prmrec  17004  modxai  17150  strfvn  17268  strss  17288  xpsvsca  17653  mreacs  17736  2oppccomf  17803  setc2obas  18173  setc2ohom  18174  cat1  18176  chnflenfi  18706  chninf  18713  mndprop  18853  grpprop  19063  isgrpi  19070  oppgmndb  19469  oppggrpb  19472  odfval  19646  efgrelexlemb  19864  ablprop  19907  ringprop  20419  opprrngb  20474  opprringb  20476  rlmbas  21364  rlmplusg  21365  rlm0  21366  rlmsub  21367  rlmmulr  21368  rlmsca2  21370  rlmvsca  21371  rlmtopn  21372  rlmds  21373  rlmvneg  21377  cncrng  21593  xrsmcmn  21595  cndrng  21601  cnsrng  21606  absabv  21624  xrs1mnd  21640  xrs10  21641  zringcyg  21669  pzriprngALT  21695  resrng  21821  psrbagsn  22264  evlsval  22287  psr1bas2  22400  psr1bas  22401  psr1plusg  22430  psr1vsca  22431  psr1mulr  22432  ply1plusgfvi  22451  ply1mpl0  22466  ply1mpl1  22468  ordtrestixx  23429  llyidm  23696  nllyidm  23697  toplly  23698  hauslly  23700  hausnlly  23701  lly1stc  23704  kgenf  23749  txswaphmeolem  24012  fmucndlem  24498  nrgtrg  24898  cnfldnm  24986  xrsxmet  25018  divcn  25078  expcn  25082  elcncf1ii  25106  iirevcn  25140  iihalf1cn  25142  iihalf2cn  25144  iimulcn  25148  icopnfcnv  25152  iccpnfcnv  25154  cnrehmeo  25163  tcphsub  25431  tcphphl  25437  iscmet3i  25522  cncmet  25532  rrxprds  25599  vitali  25823  i1f0  25897  itg20  25947  cbvitgv  25987  dvid  26128  dveflem  26189  dvef  26190  dvsincos  26191  ply1divalg2  26347  coe0  26464  iaa  26539  sincn  26658  coscn  26659  reefgim  26664  pilem3  26667  resinf1o  26752  circgrp  26768  circsubm  26769  logi  26803  divlogrlim  26851  dvrelog  26853  logcn  26863  dvlog  26867  advlog  26870  cxpcn  26961  cxpcn2  26962  resqrtcn  26965  sqrtcn  26966  atansopn  27148  dvatan  27151  leibpilem2  27157  leibpi  27158  leibpisum  27159  log2cnv  27160  log2ublem2  27163  log2ub  27165  divsqrtsumlem  27195  emcllem4  27214  emcllem6  27216  emcllem7  27217  lgamf  27257  lgam1  27279  basellem6  27301  basellem7  27302  basellem8  27303  basellem9  27304  vmaf  27334  logfacrlim  27439  lgsdir2lem5  27544  chebbnd1  27687  chtppilim  27690  chto1ub  27691  chebbnd2  27692  chto1lb  27693  chpchtlim  27694  chpo1ub  27695  chpo1ubb  27696  vmadivsum  27697  vmadivsumb  27698  mudivsum  27745  mulogsumlem  27746  mulogsum  27747  logdivsum  27748  vmalogdivsum2  27753  vmalogdivsum  27754  selberglem1  27760  selberglem2  27761  selbergb  27764  selberg2lem  27765  selberg2  27766  selberg2b  27767  selberg3lem2  27773  selberg3  27774  selberg4  27776  pntrmax  27779  pntrsumo1  27780  pntrsumbnd  27781  selbergr  27783  selberg3r  27784  selberg4r  27785  selberg34r  27786  pntrlog2bndlem1  27792  pntrlog2bndlem4  27795  pnt2  27828  pnt  27829  dmcuts  28035  lrrecpo  28185  noxpordpo  28194  noxpordfr  28195  noxpordse  28196  n0ssno  28564  0n0s  28573  n0cut  28578  n0sge0  28582  zseo  28666  twocut  28667  nohalf  28668  halfcut  28702  bdaypw2n0bndlem  28707  0reno  28740  1reno  28741  istrkg2ld  28780  legval  28904  ttgsub  29283  cchhllem  29291  2wspdisj  30381  2wspiundisj  30382  konigsbergiedgw  30670  ipasslem7  31259  normlem6  31538  opsqrlem4  32566  fpwrelmap  33148  fpwrelmapffs  33149  xrs0  33390  elrgspnlem2  33627  1fldgenq  33707  dfprm3  33907  zringfrac  33908  0mplrim  33968  ccfldsrarelvec  34125  ccfldextdgrr  34126  constrextdg2  34203  iconstr  34220  constrsdrg  34229  2sqr3minply  34234  2sqr3nconstr  34235  cos9thpiminplylem3  34238  cos9thpiminply  34242  cos9thpinconstrlem1  34243  cos9thpinconstrlem2  34244  mdetlap1  34280  circtopn  34291  cnre2csqima  34365  cnvordtrestixx  34367  mndpluscn  34380  xrge0iifcnv  34387  zlm0  34414  zlm1  34415  qqhre  34474  rrhre  34475  esumnul  34502  hasheuni  34539  sxbrsigalem2  34741  oddpwdc  34809  eulerpartlemb  34823  eulerpartgbij  34827  eulerpartlemn  34836  fib0  34854  fib1  34855  ballotlemrinv  34989  signsw0g  35008  circlemethnat  35093  dvelimalcasei  35529  dvelimexcasei  35531  dfscott3  35570  kard0  35624  subfacval2  35716  sinccvglem  36201  circum  36203  antnest  36218  antnestALT  36223  faclim  36275  faclim2  36277  cnndvlem1  37183  bj-alextruim  37316  bj-dvelimv  37545  bj-inrab2  37621  bj-rabtrAUTO  37625  bj-opelidb  37853  bj-iomnnom  37960  sucneqoni  38069  wl-df-3xor  38171  wl-3xorbi123i  38179  wl-df3maxtru1  38195  wl-cbvalnae  38245  wl-equsal  38253  poimirlem30  38358  dvtan  38378  dvasin  38412  dvacos  38413  dvreasin  38414  dvreacos  38415  efald2  38787  lcmineqlem7  42860  3lexlogpow5ineq1  42879  3lexlogpow5ineq5  42885  aks4d1p1p6  42898  cxpi11d  43162  tan3rdpi  43171  asin1half  43176  redvmptabs  43179  readvrec2  43180  readvrec  43181  resuppsinopn  43182  readvcot  43183  re1m1e0m0  43216  re0m0e0  43221  reixi  43242  subresre  43250  3cubeslem4  43478  3cubes  43479  areaquad  44001  clsk1indlem4  44828  clsk1indlem1  44829  ismnushort  45069  lhe4.4ex1a  45097  sbtT  45334  eel0TT  45470  eelTTT  45472  eelT1  45474  eelTT  45537  eelT  45539  eelT0  45541  isosctrlem1ALT  45700  disjsnxp  45848  infxr  46140  nfxneg  46233  limsup0  46466  0cnv  46514  limsup10ex  46545  liminf10ex  46546  liminfvalxr  46555  liminf0  46565  dvsinax  46685  itgsin0pilem1  46722  iblempty  46737  stowei  46836  wallispilem5  46841  wallispi  46842  stirlinglem1  46846  stirlinglem12  46857  stirlinglem13  46858  stirlinglem14  46859  stirlingr  46862  dirkertrigeqlem1  46870  fourierdlem62  46940  fourierdlem73  46951  fourierdlem76  46954  fourierdlem77  46955  fourierdlem103  46981  fourierdlem104  46982  fourierclim  46996  fourier  46997  fouriersw  47003  etransclem41  47047  etransclem46  47052  salexct2  47111  salexct3  47114  salgencntex  47115  salgensscntex  47116  dmvolsal  47118  bor1sal  47127  iocborel  47128  sge00  47148  sge0sn  47151  ovolval5lem3  47426  ioosshoi  47441  vonioolem2  47453  smfmullem4  47566  nthrucw  47665  goldrasin  47677  goldrapos  47678  cjnpoly  47684  dfafv2  47927  ichim  48264  grlimedgnedg  48954  nelsubc3  49906  fucofulem2  50146  setc2othin  50301  setcsnterm  50325  setc1obas  50327  setc1ohomfval  50328  setc1ocofval  50329  setc1oid  50330  termc2  50353  setc1onsubc  50437  onsetrec  50543  joinlmuladdmuli  50608