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 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1571

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 210  df-tru 1573

This theorem is referenced by:  hadbi123i  1626  cadbi123i  1641  nfan  1929  nfbi  1933  spimefv  2234  spime  2421  nfsb  2555  nfmov  2588  nfmo  2590  nfeuw  2621  nfeu  2622  eqabi  2898  eqabri  2905  nfeq  2938  nfel  2939  dvelimc  2950  nfrexw  3313  nfral  3363  nfrex  3364  nfrmo  3414  nfreu  3415  rabbia2  3419  rabeqc  3428  nfrab  3453  reuxfr  3712  reuxfr1  3715  nfsbc1  3763  nfsbcw  3766  nfsbc  3769  sbcbii  3800  csbeq2i  3861  nfcsb1  3876  nfcsbw  3879  nfcsb  3880  eqri  3957  ss2abi  4020  ss2rabi  4030  nfif  4518  nfdisjw  5088  nfdisj  5089  nfbr  5158  nfopab  5180  mpteq1i  5202  mpteq2ia  5206  mpteq12i  5208  ralxfr  5385  issoi  5605  nfiotaw  6496  nfiota  6498  nfriota  7379  nfov  7440  mpoeq123i  7486  mpoeq3ia  7488  opco1i  8116  xpord2indlem  8139  on2recsfn  8649  on2recsov  8650  iseri  8718  nfixpw  8910  nfixp  8911  en2i  8983  en3i  8984  ensymb  8995  entr  8999  1sdom2dom  9210  nfttrcl  9676  djulf1o  9894  djurf1o  9895  r0weon  9992  recmulnq  10944  nrex1  11044  nfneg  11448  negiso  12190  suprzcl2  12957  supxr  13334  xrinf0  13360  fac0  14308  sgn3da  15134  cnrecnv  15212  cau3  15403  cbvsum  15742  cbvsumv  15743  sum0  15768  ackbijnn  15878  flo1  15904  trireciplem  15912  trirecip  15913  ege2le3  16139  rpnnen2lem3  16267  ruclem4  16285  bitsf1ocnv  16497  prmreclem6  16976  prmrec  16977  modxai  17123  strfvn  17241  strss  17261  xpsvsca  17626  mreacs  17709  2oppccomf  17776  setc2obas  18146  setc2ohom  18147  cat1  18149  chnflenfi  18679  chninf  18686  mndprop  18813  grpprop  19014  isgrpi  19021  oppgmndb  19420  oppggrpb  19423  odfval  19597  efgrelexlemb  19815  ablprop  19858  ringprop  20369  opprrngb  20424  opprringb  20426  rlmbas  21314  rlmplusg  21315  rlm0  21316  rlmsub  21317  rlmmulr  21318  rlmsca2  21320  rlmvsca  21321  rlmtopn  21322  rlmds  21323  rlmvneg  21327  cncrng  21543  xrsmcmn  21545  cndrng  21551  cnsrng  21556  absabv  21574  xrs1mnd  21590  xrs10  21591  zringcyg  21619  pzriprngALT  21645  resrng  21771  psrbagsn  22214  evlsval  22237  psr1bas2  22350  psr1bas  22351  psr1plusg  22380  psr1vsca  22381  psr1mulr  22382  ply1plusgfvi  22401  ply1mpl0  22416  ply1mpl1  22418  ordtrestixx  23379  llyidm  23645  nllyidm  23646  toplly  23647  hauslly  23649  hausnlly  23650  lly1stc  23653  kgenf  23698  txswaphmeolem  23961  fmucndlem  24447  nrgtrg  24847  cnfldnm  24935  xrsxmet  24967  divcn  25027  expcn  25031  elcncf1ii  25055  iirevcn  25089  iihalf1cn  25091  iihalf2cn  25093  iimulcn  25097  icopnfcnv  25101  iccpnfcnv  25103  cnrehmeo  25112  tcphsub  25380  tcphphl  25386  iscmet3i  25471  cncmet  25481  rrxprds  25548  vitali  25772  i1f0  25846  itg20  25896  cbvitgv  25936  dvid  26077  dveflem  26138  dvef  26139  dvsincos  26140  ply1divalg2  26296  coe0  26413  iaa  26488  sincn  26607  coscn  26608  reefgim  26613  pilem3  26616  resinf1o  26701  circgrp  26717  circsubm  26718  logi  26752  divlogrlim  26800  dvrelog  26802  logcn  26812  dvlog  26816  advlog  26819  cxpcn  26910  cxpcn2  26911  resqrtcn  26914  sqrtcn  26915  atansopn  27097  dvatan  27100  leibpilem2  27106  leibpi  27107  leibpisum  27108  log2cnv  27109  log2ublem2  27112  log2ub  27114  divsqrtsumlem  27144  emcllem4  27163  emcllem6  27165  emcllem7  27166  lgamf  27206  lgam1  27228  basellem6  27250  basellem7  27251  basellem8  27252  basellem9  27253  vmaf  27283  logfacrlim  27388  lgsdir2lem5  27493  chebbnd1  27636  chtppilim  27639  chto1ub  27640  chebbnd2  27641  chto1lb  27642  chpchtlim  27643  chpo1ub  27644  chpo1ubb  27645  vmadivsum  27646  vmadivsumb  27647  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  logdivsum  27697  vmalogdivsum2  27702  vmalogdivsum  27703  selberglem1  27709  selberglem2  27710  selbergb  27713  selberg2lem  27714  selberg2  27715  selberg2b  27716  selberg3lem2  27722  selberg3  27723  selberg4  27725  pntrmax  27728  pntrsumo1  27729  pntrsumbnd  27730  selbergr  27732  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntrlog2bndlem1  27741  pntrlog2bndlem4  27744  pnt2  27777  pnt  27778  dmcuts  27984  lrrecpo  28134  noxpordpo  28143  noxpordfr  28144  noxpordse  28145  n0ssno  28513  0n0s  28522  n0cut  28527  n0sge0  28531  zseo  28615  twocut  28616  nohalf  28617  halfcut  28651  bdaypw2n0bndlem  28656  0reno  28689  1reno  28690  istrkg2ld  28729  legval  28853  ttgsub  29228  cchhllem  29236  2wspdisj  30314  2wspiundisj  30315  konigsbergiedgw  30599  ipasslem7  31188  normlem6  31467  opsqrlem4  32495  fpwrelmap  33078  fpwrelmapffs  33079  xrs0  33326  elrgspnlem2  33563  1fldgenq  33643  dfprm3  33843  zringfrac  33844  0mplrim  33904  ccfldsrarelvec  34061  ccfldextdgrr  34062  constrextdg2  34139  iconstr  34156  constrsdrg  34165  2sqr3minply  34170  2sqr3nconstr  34171  cos9thpiminplylem3  34174  cos9thpiminply  34178  cos9thpinconstrlem1  34179  cos9thpinconstrlem2  34180  mdetlap1  34216  circtopn  34227  cnre2csqima  34301  cnvordtrestixx  34303  mndpluscn  34316  xrge0iifcnv  34323  zlm0  34350  zlm1  34351  qqhre  34410  rrhre  34411  esumnul  34438  hasheuni  34475  sxbrsigalem2  34676  oddpwdc  34744  eulerpartlemb  34758  eulerpartgbij  34762  eulerpartlemn  34771  fib0  34789  fib1  34790  ballotlemrinv  34924  signsw0g  34943  circlemethnat  35028  dvelimalcasei  35464  dvelimexcasei  35466  dfscott3  35512  kard0  35567  subfacval2  35679  sinccvglem  36164  circum  36166  antnest  36181  antnestALT  36186  faclim  36238  faclim2  36240  cnndvlem1  37126  bj-alextruim  37259  bj-dvelimv  37488  bj-inrab2  37564  bj-rabtrAUTO  37568  bj-opelidb  37796  bj-iomnnom  37903  sucneqoni  38012  wl-df-3xor  38114  wl-3xorbi123i  38122  wl-df3maxtru1  38138  wl-cbvalnae  38188  wl-equsal  38196  poimirlem30  38301  dvtan  38321  dvasin  38355  dvacos  38356  dvreasin  38357  dvreacos  38358  efald2  38729  lcmineqlem7  42802  3lexlogpow5ineq1  42821  3lexlogpow5ineq5  42827  aks4d1p1p6  42840  cxpi11d  43104  tan3rdpi  43113  asin1half  43118  redvmptabs  43121  readvrec2  43122  readvrec  43123  resuppsinopn  43124  readvcot  43125  re1m1e0m0  43158  re0m0e0  43163  reixi  43184  subresre  43192  3cubeslem4  43420  3cubes  43421  areaquad  43943  clsk1indlem4  44770  clsk1indlem1  44771  ismnushort  45011  lhe4.4ex1a  45039  sbtT  45276  eel0TT  45412  eelTTT  45414  eelT1  45416  eelTT  45479  eelT  45481  eelT0  45483  isosctrlem1ALT  45642  disjsnxp  45790  infxr  46082  nfxneg  46175  limsup0  46408  0cnv  46456  limsup10ex  46487  liminf10ex  46488  liminfvalxr  46497  liminf0  46507  dvsinax  46627  itgsin0pilem1  46664  iblempty  46679  stowei  46778  wallispilem5  46783  wallispi  46784  stirlinglem1  46788  stirlinglem12  46799  stirlinglem13  46800  stirlinglem14  46801  stirlingr  46804  dirkertrigeqlem1  46812  fourierdlem62  46882  fourierdlem73  46893  fourierdlem76  46896  fourierdlem77  46897  fourierdlem103  46923  fourierdlem104  46924  fourierclim  46938  fourier  46939  fouriersw  46945  etransclem41  46989  etransclem46  46994  salexct2  47053  salexct3  47056  salgencntex  47057  salgensscntex  47058  dmvolsal  47060  bor1sal  47069  iocborel  47070  sge00  47090  sge0sn  47093  ovolval5lem3  47368  ioosshoi  47383  vonioolem2  47395  smfmullem4  47508  nthrucw  47607  goldrasin  47619  goldrapos  47620  cjnpoly  47626  dfafv2  47869  ichim  48206  grlimedgnedg  48896  nelsubc3  49849  fucofulem2  50089  setc2othin  50244  setcsnterm  50268  setc1obas  50270  setc1ohomfval  50271  setc1ocofval  50272  setc1oid  50273  termc2  50296  setc1onsubc  50380  onsetrec  50486  joinlmuladdmuli  50551