Theorem mptru 1529

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

Syntax hints:   → wi 4  ⊤wtru 1523

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 208  df-tru 1525

This theorem is referenced by:  hadbi123i  1578  cadbi123i  1593  nfan  1881  nfbi  1885  spimefv  2163  spime  2363  nfmov  2600  nfmo  2602  nfeu  2639  abeq2i  2917  abbi2i  2922  nfceqiOLD  2946  nfeq  2960  nfel  2961  dvelimc  2974  nfral  3191  nfrex  3271  nfreu  3335  nfrmo  3336  nfrab  3345  rabbia2  3423  reuxfr  3674  reuxfr1  3677  nfsbc1  3725  nfsbc  3728  sbcbii  3757  csbeq2i  3819  nfcsb1  3832  nfcsb  3835  nfif  4410  nfdisj  4942  nfbr  5009  mpteq12i  5053  ralxfr  5206  issoi  5395  nfiota  6193  nfriota  6986  nfov  7046  mpoeq123i  7088  mpoeq3ia  7090  iseri  8166  nfixp  8329  en2i  8395  en3i  8396  ensymb  8405  entr  8409  djulf1o  9187  djurf1o  9188  r0weon  9284  recmulnq  10232  nrex1  10332  nfneg  10729  negiso  11469  suprzcl2  12187  supxr  12556  xrinf0  12581  fac0  13486  cnrecnv  14358  cau3  14549  cbvsum  14885  sum0  14911  ackbijnn  15016  flo1  15042  trireciplem  15050  trirecip  15051  ege2le3  15276  rpnnen2lem3  15402  ruclem4  15420  bitsf1ocnv  15626  prmreclem6  16086  prmrec  16087  modxai  16233  strfvn  16334  strss  16363  xpsvsca  16679  mreacs  16758  2oppccomf  16824  mndprop  17756  grpprop  17877  isgrpi  17884  oppgmndb  18224  oppggrpb  18227  odfval  18391  efgrelexlemb  18603  ablprop  18644  ringprop  19024  opprringb  19072  rlmbas  19657  rlmplusg  19658  rlm0  19659  rlmsub  19660  rlmmulr  19661  rlmsca2  19663  rlmvsca  19664  rlmtopn  19665  rlmds  19666  rlmvneg  19669  psrbagsn  19962  evlsval  19986  psr1bas2  20041  psr1bas  20042  psr1plusg  20073  psr1vsca  20074  psr1mulr  20075  ply1plusgfvi  20093  ply1mpl0  20106  ply1mpl1  20108  cncrng  20248  xrsmcmn  20250  cndrng  20256  cnsrng  20261  xrs1mnd  20265  xrs10  20266  absabv  20284  zringcyg  20320  recrng  20447  ordtrestixx  21514  llyidm  21780  nllyidm  21781  toplly  21782  hauslly  21784  hausnlly  21785  lly1stc  21788  kgenf  21833  txswaphmeolem  22096  fmucndlem  22583  nrgtrg  22982  cnfldnm  23070  xrsxmet  23100  divcn  23159  expcn  23163  elcncf1ii  23187  iirevcn  23217  iihalf1cn  23219  iihalf2cn  23221  iimulcn  23225  icopnfcnv  23229  iccpnfcnv  23231  cnrehmeo  23240  tcphsub  23507  tcphphl  23513  iscmet3i  23598  cncmet  23608  rrxprds  23675  vitali  23897  i1f0  23971  itg20  24021  dvid  24198  dveflem  24259  dvef  24260  dvsincos  24261  ply1divalg2  24415  coe0  24529  iaa  24597  sincn  24715  coscn  24716  reefgim  24721  pilem3  24724  resinf1o  24801  circgrp  24817  circsubm  24818  divlogrlim  24899  dvrelog  24901  logcn  24911  dvlog  24915  advlog  24918  cxpcn  25007  cxpcn2  25008  resqrtcn  25011  sqrtcn  25012  atansopn  25191  dvatan  25194  leibpilem2  25201  leibpi  25202  leibpisum  25203  log2cnv  25204  log2ublem2  25207  log2ub  25209  divsqrtsumlem  25239  emcllem4  25258  emcllem6  25260  emcllem7  25261  lgamf  25301  lgam1  25323  basellem6  25345  basellem7  25346  basellem8  25347  basellem9  25348  vmaf  25378  logfacrlim  25482  lgsdir2lem5  25587  chebbnd1  25730  chtppilim  25733  chto1ub  25734  chebbnd2  25735  chto1lb  25736  chpchtlim  25737  chpo1ub  25738  chpo1ubb  25739  vmadivsum  25740  vmadivsumb  25741  mudivsum  25788  mulogsumlem  25789  mulogsum  25790  logdivsum  25791  vmalogdivsum2  25796  vmalogdivsum  25797  selberglem1  25803  selberglem2  25804  selbergb  25807  selberg2lem  25808  selberg2  25809  selberg2b  25810  selberg3lem2  25816  selberg3  25817  selberg4  25819  pntrmax  25822  pntrsumo1  25823  pntrsumbnd  25824  selbergr  25826  selberg3r  25827  selberg4r  25828  selberg34r  25829  pntrlog2bndlem1  25835  pntrlog2bndlem4  25838  pnt2  25871  pnt  25872  istrkg2ld  25928  legval  26052  ttgsub  26348  cchhllem  26356  trlsfval  27162  pthsfval  27189  spthsfval  27190  clwlks  27240  crcts  27256  cycls  27257  2wspdisj  27428  2wspiundisj  27429  eupths  27666  konigsbergiedgw  27717  ipasslem7  28304  normlem6  28583  opsqrlem4  29611  eqri  29923  fpwrelmap  30157  fpwrelmapffs  30158  xrs0  30336  ccfldsrarelvec  30660  ccfldextdgrr  30661  mdetlap1  30706  circtopn  30718  cnre2csqima  30771  cnvordtrestixx  30773  mndpluscn  30786  xrge0iifcnv  30793  zlm0  30820  zlm1  30821  qqhre  30878  rrhre  30879  esumnul  30924  hasheuni  30961  sxbrsigalem2  31161  oddpwdc  31229  eulerpartlemb  31243  eulerpartgbij  31247  eulerpartlemn  31256  fib0  31274  fib1  31275  ballotlemrinv  31408  sgn3da  31416  signsw0g  31443  circlemethnat  31529  subfacval2  32042  sinccvglem  32523  circum  32525  logi  32574  faclim  32586  faclim2  32588  dmscut  32881  cnndvlem1  33485  bj-dvelimv  33747  bj-inrab2  33817  bj-rabtrAUTO  33821  bj-iomnnom  34099  sucneqoni  34178  wl-cbvalnae  34305  wl-equsal  34312  poimirlem30  34453  dvtan  34473  dvasin  34509  dvacos  34510  dvreasin  34511  dvreacos  34512  efald2  34888  areaquad  39308  clsk1indlem4  39879  clsk1indlem1  39880  lhe4.4ex1a  40199  sbtT  40440  eel0TT  40577  eelTTT  40579  eelT1  40581  eelTT  40644  eelT  40646  eelT0  40648  isosctrlem1ALT  40807  disjsnxp  40871  infxr  41176  nfxneg  41279  limsup0  41517  0cnv  41565  limsup10ex  41596  liminf10ex  41597  liminfvalxr  41606  liminf0  41616  dvsinax  41738  itgsin0pilem1  41776  iblempty  41791  stowei  41891  wallispilem5  41896  wallispi  41897  stirlinglem1  41901  stirlinglem12  41912  stirlinglem13  41913  stirlinglem14  41914  stirlingr  41917  dirkertrigeqlem1  41925  fourierdlem62  41995  fourierdlem73  42006  fourierdlem76  42009  fourierdlem77  42010  fourierdlem103  42036  fourierdlem104  42037  fourierclim  42051  fourier  42052  fouriersw  42058  etransclem41  42102  etransclem46  42107  salexct2  42164  salexct3  42167  salgencntex  42168  salgensscntex  42169  dmvolsal  42171  bor1sal  42180  iocborel  42181  sge00  42200  sge0sn  42203  ovolval5lem3  42478  ioosshoi  42493  vonioolem2  42505  smfmullem4  42611  dfafv2  42847  onsetrec  44290  joinlmuladdmuli  44354