Theorem mptru 1545

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

Syntax hints:   → wi 4  ⊤wtru 1539

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 1541

This theorem is referenced by:  hadbi123i  1597  cadbi123i  1613  nfan  1900  nfbi  1904  spimefv  2196  spime  2396  nfsb  2542  nfmov  2578  nfmo  2580  nfeuw  2613  nfeu  2614  abeq2i  2887  abbi2i  2891  nfeq  2932  nfel  2933  dvelimc  2944  nfralw  3153  nfral  3154  nfrex  3233  nfrexg  3234  nfreuw  3292  nfrmow  3293  nfreu  3294  nfrmo  3295  nfrabw  3303  nfrab  3304  rabbia2  3389  reuxfr  3665  reuxfr1  3668  nfsbc1  3717  nfsbcw  3720  nfsbc  3723  sbcbii  3755  csbeq2i  3815  nfcsb1  3830  nfcsbw  3833  nfcsb  3834  eqri  3914  vn0  4239  nfif  4453  nfdisjw  5013  nfdisj  5014  nfbr  5083  mpteq12i  5129  ralxfr  5287  issoi  5480  nfiotaw  6303  nfiota  6305  nfriota  7126  nfov  7186  mpoeq123i  7230  mpoeq3ia  7232  iseri  8332  nfixpw  8511  nfixp  8512  en2i  8578  en3i  8579  ensymb  8588  entr  8592  djulf1o  9387  djurf1o  9388  r0weon  9485  recmulnq  10437  nrex1  10537  nfneg  10933  negiso  11670  suprzcl2  12391  supxr  12760  xrinf0  12785  fac0  13699  cnrecnv  14585  cau3  14776  cbvsum  15113  sum0  15139  ackbijnn  15244  flo1  15270  trireciplem  15278  trirecip  15279  ege2le3  15504  rpnnen2lem3  15630  ruclem4  15648  bitsf1ocnv  15856  prmreclem6  16326  prmrec  16327  modxai  16473  strfvn  16577  strss  16606  xpsvsca  16922  mreacs  17001  2oppccomf  17067  mndprop  18017  grpprop  18200  isgrpi  18207  oppgmndb  18564  oppggrpb  18567  odfval  18741  efgrelexlemb  18957  ablprop  18999  ringprop  19419  opprringb  19467  rlmbas  20049  rlmplusg  20050  rlm0  20051  rlmsub  20052  rlmmulr  20053  rlmsca2  20055  rlmvsca  20056  rlmtopn  20057  rlmds  20058  rlmvneg  20062  cncrng  20201  xrsmcmn  20203  cndrng  20209  cnsrng  20214  xrs1mnd  20218  xrs10  20219  absabv  20237  zringcyg  20273  recrng  20400  psrbagsn  20838  evlsval  20863  psr1bas2  20928  psr1bas  20929  psr1plusg  20960  psr1vsca  20961  psr1mulr  20962  ply1plusgfvi  20980  ply1mpl0  20993  ply1mpl1  20995  ordtrestixx  21936  llyidm  22202  nllyidm  22203  toplly  22204  hauslly  22206  hausnlly  22207  lly1stc  22210  kgenf  22255  txswaphmeolem  22518  fmucndlem  23006  nrgtrg  23406  cnfldnm  23494  xrsxmet  23524  divcn  23583  expcn  23587  elcncf1ii  23611  iirevcn  23645  iihalf1cn  23647  iihalf2cn  23649  iimulcn  23653  icopnfcnv  23657  iccpnfcnv  23659  cnrehmeo  23668  tcphsub  23935  tcphphl  23941  iscmet3i  24026  cncmet  24036  rrxprds  24103  vitali  24327  i1f0  24401  itg20  24451  dvid  24631  dveflem  24692  dvef  24693  dvsincos  24694  ply1divalg2  24852  coe0  24966  iaa  25034  sincn  25152  coscn  25153  reefgim  25158  pilem3  25161  resinf1o  25241  circgrp  25257  circsubm  25258  divlogrlim  25339  dvrelog  25341  logcn  25351  dvlog  25355  advlog  25358  cxpcn  25447  cxpcn2  25448  resqrtcn  25451  sqrtcn  25452  atansopn  25631  dvatan  25634  leibpilem2  25640  leibpi  25641  leibpisum  25642  log2cnv  25643  log2ublem2  25646  log2ub  25648  divsqrtsumlem  25678  emcllem4  25697  emcllem6  25699  emcllem7  25700  lgamf  25740  lgam1  25762  basellem6  25784  basellem7  25785  basellem8  25786  basellem9  25787  vmaf  25817  logfacrlim  25921  lgsdir2lem5  26026  chebbnd1  26169  chtppilim  26172  chto1ub  26173  chebbnd2  26174  chto1lb  26175  chpchtlim  26176  chpo1ub  26177  chpo1ubb  26178  vmadivsum  26179  vmadivsumb  26180  mudivsum  26227  mulogsumlem  26228  mulogsum  26229  logdivsum  26230  vmalogdivsum2  26235  vmalogdivsum  26236  selberglem1  26242  selberglem2  26243  selbergb  26246  selberg2lem  26247  selberg2  26248  selberg2b  26249  selberg3lem2  26255  selberg3  26256  selberg4  26258  pntrmax  26261  pntrsumo1  26262  pntrsumbnd  26263  selbergr  26265  selberg3r  26266  selberg4r  26267  selberg34r  26268  pntrlog2bndlem1  26274  pntrlog2bndlem4  26277  pnt2  26310  pnt  26311  istrkg2ld  26367  legval  26491  ttgsub  26786  cchhllem  26794  trlsfval  27598  pthsfval  27623  spthsfval  27624  clwlks  27674  crcts  27690  cycls  27691  2wspdisj  27861  2wspiundisj  27862  eupths  28098  konigsbergiedgw  28146  ipasslem7  28732  normlem6  29011  opsqrlem4  30039  fpwrelmap  30605  fpwrelmapffs  30606  xrs0  30823  ccfldsrarelvec  31275  ccfldextdgrr  31276  mdetlap1  31310  circtopn  31321  cnre2csqima  31395  cnvordtrestixx  31397  mndpluscn  31410  xrge0iifcnv  31417  zlm0  31444  zlm1  31445  qqhre  31502  rrhre  31503  esumnul  31548  hasheuni  31585  sxbrsigalem2  31785  oddpwdc  31853  eulerpartlemb  31867  eulerpartgbij  31871  eulerpartlemn  31880  fib0  31898  fib1  31899  ballotlemrinv  32032  sgn3da  32040  signsw0g  32067  circlemethnat  32153  subfacval2  32678  sinccvglem  33159  circum  33161  logi  33228  faclim  33240  faclim2  33242  xpord2ind  33362  xpord3ind  33368  on2recsfn  33424  on2recsov  33425  dmscut  33601  lrrecpo  33681  noxpordpo  33690  noxpordfr  33691  noxpordse  33692  no3indslem  33698  cnndvlem1  34301  bj-dvelimv  34608  bj-inrab2  34686  bj-rabtrAUTO  34690  bj-opelidb  34882  bj-iomnnom  34989  sucneqoni  35098  wl-df-3xor  35200  wl-3xorbi123i  35208  wl-df3maxtru1  35224  wl-cbvalnae  35253  wl-equsal  35260  poimirlem30  35402  dvtan  35422  dvasin  35456  dvacos  35457  dvreasin  35458  dvreacos  35459  efald2  35831  lcmineqlem7  39637  3lexlogpow5ineq1  39656  3lexlogpow5ineq5  39662  aks4d1p1p6  39674  re1m1e0m0  39922  re0m0e0  39927  reixi  39946  subresre  39954  3cubeslem4  40048  3cubes  40049  areaquad  40584  clsk1indlem4  41165  clsk1indlem1  41166  lhe4.4ex1a  41451  sbtT  41691  eel0TT  41828  eelTTT  41830  eelT1  41832  eelTT  41895  eelT  41897  eelT0  41899  isosctrlem1ALT  42058  disjsnxp  42122  infxr  42412  nfxneg  42511  limsup0  42747  0cnv  42795  limsup10ex  42826  liminf10ex  42827  liminfvalxr  42836  liminf0  42846  dvsinax  42966  itgsin0pilem1  43003  iblempty  43018  stowei  43117  wallispilem5  43122  wallispi  43123  stirlinglem1  43127  stirlinglem12  43138  stirlinglem13  43139  stirlinglem14  43140  stirlingr  43143  dirkertrigeqlem1  43151  fourierdlem62  43221  fourierdlem73  43232  fourierdlem76  43235  fourierdlem77  43236  fourierdlem103  43262  fourierdlem104  43263  fourierclim  43277  fourier  43278  fouriersw  43284  etransclem41  43328  etransclem46  43333  salexct2  43390  salexct3  43393  salgencntex  43394  salgensscntex  43395  dmvolsal  43397  bor1sal  43406  iocborel  43407  sge00  43426  sge0sn  43429  ovolval5lem3  43704  ioosshoi  43719  vonioolem2  43731  smfmullem4  43837  dfafv2  44115  ichim  44401  onsetrec  45734  joinlmuladdmuli  45798