Theorem mptru 1543

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

Syntax hints:   → wi 4  ⊤wtru 1537

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 207  df-tru 1539

This theorem is referenced by:  hadbi123i  1592  cadbi123i  1607  nfan  1896  nfbi  1900  spimefv  2195  spime  2391  nfsb  2525  nfmov  2557  nfmo  2559  nfeuw  2590  nfeu  2591  eqabi  2874  eqabri  2882  nfeq  2916  nfel  2917  dvelimc  2928  nfralwOLD  3309  nfrexw  3310  nfral  3371  nfrex  3372  nfreuwOLD  3422  nfrmowOLD  3423  nfrmo  3430  nfreu  3431  rabbia2  3435  rabeqc  3445  nfrabw  3472  nfrabwOLD  3473  nfrab  3475  reuxfr  3757  reuxfr1  3760  nfsbc1  3809  nfsbcw  3812  nfsbc  3815  sbcbii  3851  csbeq2i  3915  nfcsb1  3931  nfcsbw  3934  nfcsb  3935  eqri  4015  vn0  4350  nfif  4560  nfdisjw  5126  nfdisj  5127  nfbr  5194  nfopab  5216  mpteq1i  5243  mpteq2ia  5250  mpteq12i  5253  ralxfr  5419  issoi  5631  nfiotaw  6519  nfiota  6521  nfriota  7399  nfov  7460  mpoeq123i  7508  mpoeq3ia  7510  opco1i  8148  xpord2indlem  8170  dfwrecsOLD  8336  on2recsfn  8703  on2recsov  8704  iseri  8770  nfixpw  8954  nfixp  8955  en2i  9028  en3i  9029  ensymb  9040  entr  9044  1sdom2dom  9280  nfttrcl  9748  djulf1o  9949  djurf1o  9950  r0weon  10049  recmulnq  11001  nrex1  11101  nfneg  11501  negiso  12245  suprzcl2  12977  supxr  13351  xrinf0  13376  fac0  14311  cnrecnv  15200  cau3  15390  cbvsum  15727  cbvsumv  15728  sum0  15753  ackbijnn  15860  flo1  15886  trireciplem  15894  trirecip  15895  ege2le3  16122  rpnnen2lem3  16248  ruclem4  16266  bitsf1ocnv  16477  prmreclem6  16954  prmrec  16955  modxai  17101  strfvn  17219  strss  17240  xpsvsca  17623  mreacs  17702  2oppccomf  17771  setc2obas  18147  setc2ohom  18148  cat1  18150  mndprop  18785  grpprop  18982  isgrpi  18989  oppgmndb  19388  oppggrpb  19391  odfval  19564  efgrelexlemb  19782  ablprop  19825  ringprop  20303  opprrngb  20362  opprringb  20364  rlmbas  21217  rlmplusg  21218  rlm0  21219  rlmsub  21220  rlmmulr  21221  rlmsca2  21223  rlmvsca  21224  rlmtopn  21225  rlmds  21226  rlmvneg  21230  dfcnfldOLD  21397  cncrng  21418  cncrngOLD  21419  xrsmcmn  21421  cndrng  21428  cndrngOLD  21429  cnsrng  21435  xrs1mnd  21439  xrs10  21440  absabv  21459  zringcyg  21497  pzriprngALT  21523  resrng  21656  psrbagsn  22104  evlsval  22127  psr1bas2  22206  psr1bas  22207  psr1plusg  22237  psr1vsca  22238  psr1mulr  22239  ply1plusgfvi  22258  ply1mpl0  22273  ply1mpl1  22275  ordtrestixx  23245  llyidm  23511  nllyidm  23512  toplly  23513  hauslly  23515  hausnlly  23516  lly1stc  23519  kgenf  23564  txswaphmeolem  23827  fmucndlem  24315  nrgtrg  24726  cnfldnm  24814  xrsxmet  24844  divcnOLD  24903  divcn  24905  expcn  24909  expcnOLD  24911  elcncf1ii  24935  iirevcn  24970  iihalf1cn  24972  iihalf1cnOLD  24973  iihalf2cn  24975  iihalf2cnOLD  24976  iimulcn  24980  iimulcnOLD  24981  icopnfcnv  24986  iccpnfcnv  24988  cnrehmeo  24997  cnrehmeoOLD  24998  tcphsub  25268  tcphphl  25274  iscmet3i  25359  cncmet  25369  rrxprds  25436  vitali  25661  i1f0  25735  itg20  25786  cbvitgv  25826  dvid  25967  dveflem  26031  dvef  26032  dvsincos  26033  ply1divalg2  26192  coe0  26309  iaa  26381  sincn  26502  coscn  26503  reefgim  26508  pilem3  26511  resinf1o  26592  circgrp  26608  circsubm  26609  logi  26643  divlogrlim  26691  dvrelog  26693  logcn  26703  dvlog  26707  advlog  26710  cxpcn  26801  cxpcnOLD  26802  cxpcn2  26803  resqrtcn  26806  sqrtcn  26807  atansopn  26989  dvatan  26992  leibpilem2  26998  leibpi  26999  leibpisum  27000  log2cnv  27001  log2ublem2  27004  log2ub  27006  divsqrtsumlem  27037  emcllem4  27056  emcllem6  27058  emcllem7  27059  lgamf  27099  lgam1  27121  basellem6  27143  basellem7  27144  basellem8  27145  basellem9  27146  vmaf  27176  logfacrlim  27282  lgsdir2lem5  27387  chebbnd1  27530  chtppilim  27533  chto1ub  27534  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ub  27538  chpo1ubb  27539  vmadivsum  27540  vmadivsumb  27541  mudivsum  27588  mulogsumlem  27589  mulogsum  27590  logdivsum  27591  vmalogdivsum2  27596  vmalogdivsum  27597  selberglem1  27603  selberglem2  27604  selbergb  27607  selberg2lem  27608  selberg2  27609  selberg2b  27610  selberg3lem2  27616  selberg3  27617  selberg4  27619  pntrmax  27622  pntrsumo1  27623  pntrsumbnd  27624  selbergr  27626  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntrlog2bndlem1  27635  pntrlog2bndlem4  27638  pnt2  27671  pnt  27672  dmscut  27870  lrrecpo  27988  noxpordpo  27997  noxpordfr  27998  noxpordse  27999  n0sex  28336  n0ssno  28339  0n0s  28348  n0scut  28352  n0sge0  28355  1p1e2s  28414  zseo  28420  nohalf  28421  0reno  28443  istrkg2ld  28482  legval  28606  ttgsub  28905  cchhllem  28915  cchhllemOLD  28916  2wspdisj  29991  2wspiundisj  29992  konigsbergiedgw  30276  ipasslem7  30864  normlem6  31143  opsqrlem4  32171  fpwrelmap  32750  fpwrelmapffs  32751  xrs0  32990  elrgspnlem2  33232  1fldgenq  33303  dfprm3  33560  zringfrac  33561  ccfldsrarelvec  33695  ccfldextdgrr  33696  2sqr3minply  33752  mdetlap1  33786  circtopn  33797  cnre2csqima  33871  cnvordtrestixx  33873  mndpluscn  33886  xrge0iifcnv  33893  zlm0  33920  zlm1  33921  qqhre  33982  rrhre  33983  esumnul  34028  hasheuni  34065  sxbrsigalem2  34267  oddpwdc  34335  eulerpartlemb  34349  eulerpartgbij  34353  eulerpartlemn  34362  fib0  34380  fib1  34381  ballotlemrinv  34514  sgn3da  34522  signsw0g  34549  circlemethnat  34634  dvelimalcasei  35068  dvelimexcasei  35070  subfacval2  35171  sinccvglem  35656  circum  35658  antnest  35673  faclim  35725  faclim2  35727  cnndvlem1  36519  bj-dvelimv  36835  bj-inrab2  36910  bj-rabtrAUTO  36914  bj-opelidb  37134  bj-iomnnom  37241  sucneqoni  37348  wl-df-3xor  37450  wl-3xorbi123i  37458  wl-df3maxtru1  37474  wl-cbvalnae  37513  wl-equsal  37521  poimirlem30  37636  dvtan  37656  dvasin  37690  dvacos  37691  dvreasin  37692  dvreacos  37693  efald2  38064  lcmineqlem7  42016  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1p6  42054  cxpi11d  42357  tan3rdpi  42364  asin1half  42365  redvmptabs  42368  readvrec2  42369  readvrec  42370  re1m1e0m0  42403  re0m0e0  42408  reixi  42428  subresre  42436  3cubeslem4  42676  3cubes  42677  areaquad  43204  clsk1indlem4  44033  clsk1indlem1  44034  ismnushort  44296  lhe4.4ex1a  44324  sbtT  44564  eel0TT  44701  eelTTT  44703  eelT1  44705  eelTT  44768  eelT  44770  eelT0  44772  isosctrlem1ALT  44931  disjsnxp  45009  infxr  45316  nfxneg  45410  limsup0  45649  0cnv  45697  limsup10ex  45728  liminf10ex  45729  liminfvalxr  45738  liminf0  45748  dvsinax  45868  itgsin0pilem1  45905  iblempty  45920  stowei  46019  wallispilem5  46024  wallispi  46025  stirlinglem1  46029  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlingr  46045  dirkertrigeqlem1  46053  fourierdlem62  46123  fourierdlem73  46134  fourierdlem76  46137  fourierdlem77  46138  fourierdlem103  46164  fourierdlem104  46165  fourierclim  46179  fourier  46180  fouriersw  46186  etransclem41  46230  etransclem46  46235  salexct2  46294  salexct3  46297  salgencntex  46298  salgensscntex  46299  dmvolsal  46301  bor1sal  46310  iocborel  46311  sge00  46331  sge0sn  46334  ovolval5lem3  46609  ioosshoi  46624  vonioolem2  46636  smfmullem4  46749  upwrdfi  46840  dfafv2  47081  ichim  47381  setc2othin  48856  onsetrec  48938  joinlmuladdmuli  49003