Theorem mptru 1567

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

Syntax hints:   → wi 4  ⊤wtru 1561

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 209  df-tru 1563

This theorem is referenced by:  hadbi123i  1616  cadbi123i  1631  nfan  1919  nfbi  1923  spimefv  2233  spime  2420  nfsb  2554  nfmov  2587  nfmo  2589  nfeuw  2620  nfeu  2621  eqabi  2897  eqabri  2904  nfeq  2937  nfel  2938  dvelimc  2949  nfrexw  3310  nfral  3361  nfrex  3362  nfrmo  3412  nfreu  3413  rabbia2  3417  rabeqc  3426  nfrab  3452  reuxfr  3712  reuxfr1  3715  nfsbc1  3763  nfsbcw  3766  nfsbc  3769  sbcbii  3800  csbeq2i  3860  nfcsb1  3875  nfcsbw  3878  nfcsb  3879  eqri  3956  ss2abi  4019  ss2rabi  4029  nfif  4511  nfdisjw  5079  nfdisj  5080  nfbr  5147  nfopab  5169  mpteq1i  5191  mpteq2ia  5195  mpteq12i  5197  ralxfr  5371  issoi  5591  nfiotaw  6481  nfiota  6483  nfriota  7365  nfov  7426  mpoeq123i  7472  mpoeq3ia  7474  opco1i  8104  xpord2indlem  8127  on2recsfn  8637  on2recsov  8638  iseri  8706  nfixpw  8898  nfixp  8899  en2i  8971  en3i  8972  ensymb  8983  entr  8987  1sdom2dom  9198  nfttrcl  9666  djulf1o  9870  djurf1o  9871  r0weon  9968  recmulnq  10922  nrex1  11022  nfneg  11426  negiso  12172  suprzcl2  12939  supxr  13316  xrinf0  13342  fac0  14289  sgn3da  15114  cnrecnv  15192  cau3  15383  cbvsum  15722  cbvsumv  15723  sum0  15748  ackbijnn  15858  flo1  15884  trireciplem  15892  trirecip  15893  ege2le3  16120  rpnnen2lem3  16248  ruclem4  16266  bitsf1ocnv  16478  prmreclem6  16957  prmrec  16958  modxai  17104  strfvn  17222  strss  17242  xpsvsca  17607  mreacs  17690  2oppccomf  17757  setc2obas  18127  setc2ohom  18128  cat1  18130  chnflenfi  18660  chninf  18667  mndprop  18794  grpprop  18994  isgrpi  19001  oppgmndb  19395  oppggrpb  19398  odfval  19572  efgrelexlemb  19790  ablprop  19833  ringprop  20336  opprrngb  20391  opprringb  20393  rlmbas  21257  rlmplusg  21258  rlm0  21259  rlmsub  21260  rlmmulr  21261  rlmsca2  21263  rlmvsca  21264  rlmtopn  21265  rlmds  21266  rlmvneg  21270  cncrng  21442  xrsmcmn  21444  cndrng  21450  cnsrng  21455  absabv  21473  xrs1mnd  21489  xrs10  21490  zringcyg  21518  pzriprngALT  21544  resrng  21670  psrbagsn  22113  evlsval  22136  psr1bas2  22249  psr1bas  22250  psr1plusg  22279  psr1vsca  22280  psr1mulr  22281  ply1plusgfvi  22300  ply1mpl0  22315  ply1mpl1  22317  ordtrestixx  23279  llyidm  23545  nllyidm  23546  toplly  23547  hauslly  23549  hausnlly  23550  lly1stc  23553  kgenf  23598  txswaphmeolem  23861  fmucndlem  24347  nrgtrg  24747  cnfldnm  24835  xrsxmet  24867  divcn  24927  expcn  24931  elcncf1ii  24955  iirevcn  24989  iihalf1cn  24991  iihalf2cn  24993  iimulcn  24997  icopnfcnv  25001  iccpnfcnv  25003  cnrehmeo  25012  tcphsub  25280  tcphphl  25286  iscmet3i  25371  cncmet  25381  rrxprds  25448  vitali  25672  i1f0  25746  itg20  25796  cbvitgv  25836  dvid  25977  dveflem  26038  dvef  26039  dvsincos  26040  ply1divalg2  26196  coe0  26313  iaa  26386  sincn  26504  coscn  26505  reefgim  26510  pilem3  26513  resinf1o  26598  circgrp  26614  circsubm  26615  logi  26649  divlogrlim  26697  dvrelog  26699  logcn  26709  dvlog  26713  advlog  26716  cxpcn  26807  cxpcn2  26808  resqrtcn  26811  sqrtcn  26812  atansopn  26994  dvatan  26997  leibpilem2  27003  leibpi  27004  leibpisum  27005  log2cnv  27006  log2ublem2  27009  log2ub  27011  divsqrtsumlem  27041  emcllem4  27060  emcllem6  27062  emcllem7  27063  lgamf  27103  lgam1  27125  basellem6  27147  basellem7  27148  basellem8  27149  basellem9  27150  vmaf  27180  logfacrlim  27285  lgsdir2lem5  27390  chebbnd1  27533  chtppilim  27536  chto1ub  27537  chebbnd2  27538  chto1lb  27539  chpchtlim  27540  chpo1ub  27541  chpo1ubb  27542  vmadivsum  27543  vmadivsumb  27544  mudivsum  27591  mulogsumlem  27592  mulogsum  27593  logdivsum  27594  vmalogdivsum2  27599  vmalogdivsum  27600  selberglem1  27606  selberglem2  27607  selbergb  27610  selberg2lem  27611  selberg2  27612  selberg2b  27613  selberg3lem2  27619  selberg3  27620  selberg4  27622  pntrmax  27625  pntrsumo1  27626  pntrsumbnd  27627  selbergr  27629  selberg3r  27630  selberg4r  27631  selberg34r  27632  pntrlog2bndlem1  27638  pntrlog2bndlem4  27641  pnt2  27674  pnt  27675  dmcuts  27881  lrrecpo  28031  noxpordpo  28040  noxpordfr  28041  noxpordse  28042  n0ssno  28410  0n0s  28419  n0cut  28424  n0sge0  28428  zseo  28512  twocut  28513  nohalf  28514  halfcut  28548  bdaypw2n0bndlem  28553  0reno  28586  1reno  28587  istrkg2ld  28626  legval  28750  ttgsub  29076  cchhllem  29084  2wspdisj  30162  2wspiundisj  30163  konigsbergiedgw  30447  ipasslem7  31036  normlem6  31315  opsqrlem4  32343  fpwrelmap  32932  fpwrelmapffs  32933  xrs0  33181  elrgspnlem2  33421  1fldgenq  33506  dfprm3  33746  zringfrac  33747  0mplrim  33808  ccfldsrarelvec  33965  ccfldextdgrr  33966  constrextdg2  34043  iconstr  34060  constrsdrg  34069  2sqr3minply  34074  2sqr3nconstr  34075  cos9thpiminplylem3  34078  cos9thpiminply  34082  cos9thpinconstrlem1  34083  cos9thpinconstrlem2  34084  mdetlap1  34120  circtopn  34131  cnre2csqima  34205  cnvordtrestixx  34207  mndpluscn  34220  xrge0iifcnv  34227  zlm0  34254  zlm1  34255  qqhre  34314  rrhre  34315  esumnul  34342  hasheuni  34379  sxbrsigalem2  34580  oddpwdc  34648  eulerpartlemb  34662  eulerpartgbij  34666  eulerpartlemn  34675  fib0  34693  fib1  34694  ballotlemrinv  34828  signsw0g  34847  circlemethnat  34932  dvelimalcasei  35368  dvelimexcasei  35370  subfacval2  35534  sinccvglem  36019  circum  36021  antnest  36036  antnestALT  36041  faclim  36093  faclim2  36095  cnndvlem1  36972  bj-alextruim  37106  bj-dvelimv  37335  bj-inrab2  37410  bj-rabtrAUTO  37414  bj-opelidb  37641  bj-iomnnom  37748  sucneqoni  37857  wl-df-3xor  37959  wl-3xorbi123i  37967  wl-df3maxtru1  37983  wl-cbvalnae  38033  wl-equsal  38041  poimirlem30  38146  dvtan  38166  dvasin  38200  dvacos  38201  dvreasin  38202  dvreacos  38203  efald2  38574  lcmineqlem7  42649  3lexlogpow5ineq1  42668  3lexlogpow5ineq5  42674  aks4d1p1p6  42687  cxpi11d  42949  tan3rdpi  42958  asin1half  42963  redvmptabs  42966  readvrec2  42967  readvrec  42968  resuppsinopn  42969  readvcot  42970  re1m1e0m0  43003  re0m0e0  43008  reixi  43029  subresre  43037  3cubeslem4  43267  3cubes  43268  areaquad  43790  clsk1indlem4  44617  clsk1indlem1  44618  ismnushort  44874  lhe4.4ex1a  44902  sbtT  45140  eel0TT  45276  eelTTT  45278  eelT1  45280  eelTT  45343  eelT  45345  eelT0  45347  isosctrlem1ALT  45506  disjsnxp  45647  infxr  45939  nfxneg  46032  limsup0  46265  0cnv  46313  limsup10ex  46344  liminf10ex  46345  liminfvalxr  46354  liminf0  46364  dvsinax  46484  itgsin0pilem1  46521  iblempty  46536  stowei  46635  wallispilem5  46640  wallispi  46641  stirlinglem1  46645  stirlinglem12  46656  stirlinglem13  46657  stirlinglem14  46658  stirlingr  46661  dirkertrigeqlem1  46669  fourierdlem62  46739  fourierdlem73  46750  fourierdlem76  46753  fourierdlem77  46754  fourierdlem103  46780  fourierdlem104  46781  fourierclim  46795  fourier  46796  fouriersw  46802  etransclem41  46846  etransclem46  46851  salexct2  46910  salexct3  46913  salgencntex  46914  salgensscntex  46915  dmvolsal  46917  bor1sal  46926  iocborel  46927  sge00  46947  sge0sn  46950  ovolval5lem3  47225  ioosshoi  47240  vonioolem2  47252  smfmullem4  47365  nthrucw  47459  goldrasin  47473  goldrapos  47474  cjnpoly  47480  dfafv2  47723  ichim  48060  grlimedgnedg  48750  nelsubc3  49689  fucofulem2  49929  setc2othin  50084  setcsnterm  50108  setc1obas  50110  setc1ohomfval  50111  setc1ocofval  50112  setc1oid  50113  termc2  50136  setc1onsubc  50220  onsetrec  50326  joinlmuladdmuli  50391