Theorem mptru 1576

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

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

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 1572

This theorem is used by:  hadbi123i  1625  cadbi123i  1643  nfan  1931  nfbi  1935  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  3706  reuxfr1  3709  nfsbc1  3757  nfsbcw  3760  nfsbc  3763  sbcbii  3794  csbeq2i  3855  nfcsb1  3870  nfcsbw  3873  nfcsb  3874  eqri  3929  ss2abi  3990  ss2rabi  4000  nfif  4512  nfdisjw  5081  nfdisj  5082  nfbr  5151  nfopab  5173  mpteq1i  5195  mpteq2ia  5199  mpteq12i  5201  ralxfr  5376  issoi  5595  nfiotaw  6501  nfiota  6503  nfriota  7393  nfov  7454  mpoeq123i  7500  mpoeq3ia  7502  opco1i  8143  xpord2indlem  8171  on2recsfn  8684  on2recsov  8685  iseri  8753  nfixpw  8952  nfixp  8953  en2i  9025  en3i  9026  ensymb  9037  entr  9041  1sdom2dom  9253  nfttrcl  9719  djulf1o  10000  djurf1o  10001  r0weon  10098  recmulnq  11056  nrex1  11156  nfneg  11560  negiso  12304  suprzcl2  13072  supxr  13450  xrinf0  13476  fac0  14427  sgn3da  15263  cnrecnv  15341  cau3  15532  cbvsum  15871  cbvsumv  15872  sum0  15896  ackbijnn  16006  flo1  16032  trireciplem  16040  trirecip  16041  ege2le3  16265  rpnnen2lem3  16393  ruclem4  16411  bitsf1ocnv  16623  prmreclem6  17108  prmrec  17109  modxai  17255  strfvn  17373  strss  17393  xpsvsca  17758  mreacs  17841  2oppccomf  17908  setc2obas  18278  setc2ohom  18279  cat1  18281  chnflenfi  18811  chninf  18818  mndprop  18961  grpprop  19172  isgrpi  19179  oppgmndb  19578  oppggrpb  19581  odfval  19755  efgrelexlemb  19973  ablprop  20016  ringprop  20530  opprrngb  20585  opprringb  20587  rlmbas  21477  rlmplusg  21478  rlm0  21479  rlmsub  21480  rlmmulr  21481  rlmsca2  21483  rlmvsca  21484  rlmtopn  21485  rlmds  21486  rlmvneg  21490  cncrng  21708  xrsmcmn  21710  cndrng  21716  cnsrng  21721  absabv  21739  xrs1mnd  21755  xrs10  21756  zringcyg  21784  pzriprngALT  21810  resrng  21936  psrbagsn  22381  evlsval  22404  psr1bas2  22517  psr1bas  22518  psr1plusg  22547  psr1vsca  22548  psr1mulr  22549  ply1plusgfvi  22568  ply1mpl0  22583  ply1mpl1  22585  ordtrestixx  23549  llyidm  23816  nllyidm  23817  toplly  23818  hauslly  23820  hausnlly  23821  lly1stc  23824  kgenf  23869  txswaphmeolem  24132  fmucndlem  24618  nrgtrg  25018  cnfldnm  25106  xrsxmet  25138  divcn  25198  expcn  25202  elcncf1ii  25226  iirevcn  25260  iihalf1cn  25262  iihalf2cn  25264  iimulcn  25268  icopnfcnv  25272  iccpnfcnv  25274  cnrehmeo  25283  tcphsub  25551  tcphphl  25557  iscmet3i  25642  cncmet  25652  rrxprds  25719  vitali  25943  i1f0  26017  itg20  26067  cbvitgv  26106  dvid  26247  dveflem  26308  dvef  26309  dvsincos  26310  ply1divalg2  26466  coe0  26584  iaa  26660  iaaOLD  26661  sincn  26780  coscn  26781  reefgim  26786  pilem3  26789  resinf1o  26873  circgrp  26889  circsubm  26890  logi  26924  divlogrlim  26972  dvrelog  26974  logcn  26984  dvlog  26988  advlog  26991  cxpcn  27082  cxpcn2  27083  resqrtcn  27086  sqrtcn  27087  atansopn  27269  dvatan  27272  leibpilem2  27278  leibpi  27279  leibpisum  27280  log2cnv  27281  log2ublem2  27284  log2ub  27286  divsqrtsumlem  27316  emcllem4  27335  emcllem6  27337  emcllem7  27338  lgamf  27378  lgam1  27400  basellem6  27422  basellem7  27423  basellem8  27424  basellem9  27425  vmaf  27455  logfacrlim  27560  lgsdir2lem5  27665  chebbnd1  27808  chtppilim  27811  chto1ub  27812  chebbnd2  27813  chto1lb  27814  chpchtlim  27815  chpo1ub  27816  chpo1ubb  27817  vmadivsum  27818  vmadivsumb  27819  mudivsum  27866  mulogsumlem  27867  mulogsum  27868  logdivsum  27869  vmalogdivsum2  27874  vmalogdivsum  27875  selberglem1  27881  selberglem2  27882  selbergb  27885  selberg2lem  27886  selberg2  27887  selberg2b  27888  selberg3lem2  27894  selberg3  27895  selberg4  27897  pntrmax  27900  pntrsumo1  27901  pntrsumbnd  27902  selbergr  27904  selberg3r  27905  selberg4r  27906  selberg34r  27907  pntrlog2bndlem1  27913  pntrlog2bndlem4  27916  pnt2  27949  pnt  27950  dmcuts  28186  lrrecpo  28336  noxpordpo  28345  noxpordfr  28346  noxpordse  28347  n0ssno  28715  0n0s  28724  n0cut  28729  n0sge0  28733  zseo  28817  twocut  28818  nohalf  28819  halfcut  28853  bdaypw2n0bndlem  28858  0reno  28891  1reno  28892  istrkg2ld  28931  legval  29056  ttgsub  29465  cchhllem  29473  2wspdisj  30563  2wspiundisj  30564  konigsbergiedgw  30858  ipasslem7  31447  normlem6  31726  opsqrlem4  32754  fpwrelmap  33375  fpwrelmapffs  33376  xrs0  33617  elrgspnlem2  33854  1fldgenq  33934  dfprm3  34135  zringfrac  34136  0mplrim  34196  ccfldsrarelvec  34353  ccfldextdgrr  34354  constrextdg2  34431  iconstr  34448  constrsdrg  34457  2sqr3minply  34462  2sqr3nconstr  34463  cos9thpiminplylem3  34466  cos9thpiminply  34470  cos9thpinconstrlem1  34471  cos9thpinconstrlem2  34472  mdetlap1  34508  circtopn  34519  cnre2csqima  34593  cnvordtrestixx  34595  mndpluscn  34608  xrge0iifcnv  34615  zlm0  34642  zlm1  34643  qqhre  34702  rrhre  34703  esumnul  34730  hasheuni  34767  sxbrsigalem2  34968  oddpwdc  35036  eulerpartlemb  35050  eulerpartgbij  35054  eulerpartlemn  35063  fib0  35081  fib1  35082  ballotlemrinv  35216  signsw0g  35235  circlemethnat  35320  dvelimalcasei  35756  dvelimexcasei  35758  dfscott3  35803  kard0  35890  subfacval2  36070  sinccvglem  36555  circum  36557  antnest  36572  antnestALT  36577  faclim  36635  faclim2  36637  cnndvlem1  37527  bj-alextruim  37660  bj-dvelimv  37889  bj-inrab2  37965  bj-rabtrAUTO  37969  bj-opelidb  38210  bj-iomnnom  38317  sucneqoni  38426  wl-df-3xor  38528  wl-3xorbi123i  38536  wl-df3maxtru1  38552  wl-cbvalnae  38602  wl-equsal  38610  poimirlem30  38705  dvtan  38725  dvasin  38759  dvacos  38760  dvreasin  38761  dvreacos  38762  dfprop2  38783  efald2  39149  lcmineqlem7  43222  3lexlogpow5ineq1  43241  3lexlogpow5ineq5  43247  aks4d1p1p6  43260  cxpi11d  43531  tan3rdpi  43540  asin1half  43545  redvmptabs  43548  readvrec2  43549  readvrec  43550  resuppsinopn  43551  readvcot  43552  re1m1e0m0  43585  re0m0e0  43590  reixi  43611  subresre  43619  3cubeslem4  43836  3cubes  43837  areaquad  44355  clsk1indlem4  45181  clsk1indlem1  45182  ismnushort  45422  lhe4.4ex1a  45450  sbtT  45686  eel0TT  45822  eelTTT  45824  eelT1  45826  eelTT  45889  eelT  45891  eelT0  45893  isosctrlem1ALT  46052  disjsnxp  46223  infxr  46514  nfxneg  46607  limsup0  46840  0cnv  46888  limsup10ex  46919  liminf10ex  46920  liminfvalxr  46929  liminf0  46939  dvsinax  47059  itgsin0pilem1  47096  iblempty  47111  stowei  47210  wallispilem5  47215  wallispi  47216  stirlinglem1  47220  stirlinglem12  47231  stirlinglem13  47232  stirlinglem14  47233  stirlingr  47236  dirkertrigeqlem1  47244  fourierdlem62  47314  fourierdlem73  47325  fourierdlem76  47328  fourierdlem77  47329  fourierdlem103  47355  fourierdlem104  47356  fourierclim  47370  fourier  47371  fouriersw  47377  etransclem41  47421  etransclem46  47426  salexct2  47485  salexct3  47488  salgencntex  47489  salgensscntex  47490  dmvolsal  47492  bor1sal  47501  iocborel  47502  sge00  47522  sge0sn  47525  ovolval5lem3  47800  ioosshoi  47815  vonioolem2  47827  smfmullem4  47940  numtowerdt  48052  goldpolyfactor  48063  goldrasin  48065  goldrapos  48066  goldratval  48072  cjnpoly  48075  dfafv2  48338  ichim  48675  grlimedgnedg  49365  rrx2xpref1o  49967  nelsubc3  50321  fucofulem2  50569  fucoisfunc2lem1  50624  setc2othin  50737  setcsnterm  50761  setc1obas  50763  setc1ohomfval  50764  setc1ocofval  50765  setc1oid  50766  termc2  50789  setc1onsubc  50876  parcatid2  50899  parcatid  50900  parmapfunc2  50910  parmapfunc  50911  par2diag  50916  fuconuniqlem  50917  fuconuniqvalslem  50919  onsetrec  51012  dvsec  51067  dvcsc  51068  dvcot  51069  joinlmuladdmuli  51080