Theorem mptru 1546

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

Syntax hints:   → wi 4  ⊤wtru 1540

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 1542

This theorem is referenced by:  hadbi123i  1595  cadbi123i  1610  nfan  1898  nfbi  1902  spimefv  2197  spime  2392  nfsb  2526  nfmov  2558  nfmo  2560  nfeuw  2591  nfeu  2592  eqabi  2869  eqabri  2877  nfeq  2911  nfel  2912  dvelimc  2923  nfralwOLD  3296  nfrexw  3297  nfral  3358  nfrex  3359  nfreuwOLD  3410  nfrmowOLD  3411  nfrmo  3418  nfreu  3419  rabbia2  3423  rabeqc  3433  nfrabw  3459  nfrabwOLD  3460  nfrab  3462  reuxfr  3739  reuxfr1  3742  nfsbc1  3791  nfsbcw  3794  nfsbc  3797  sbcbii  3829  csbeq2i  3889  nfcsb1  3904  nfcsbw  3907  nfcsb  3908  eqri  3986  vn0  4327  nfif  4538  nfdisjw  5104  nfdisj  5105  nfbr  5172  nfopab  5194  mpteq1i  5220  mpteq2ia  5227  mpteq12i  5230  ralxfr  5396  issoi  5610  nfiotaw  6499  nfiota  6501  nfriota  7383  nfov  7444  mpoeq123i  7492  mpoeq3ia  7494  opco1i  8133  xpord2indlem  8155  dfwrecsOLD  8321  on2recsfn  8688  on2recsov  8689  iseri  8755  nfixpw  8939  nfixp  8940  en2i  9013  en3i  9014  ensymb  9025  entr  9029  1sdom2dom  9266  nfttrcl  9734  djulf1o  9935  djurf1o  9936  r0weon  10035  recmulnq  10987  nrex1  11087  nfneg  11487  negiso  12231  suprzcl2  12963  supxr  13338  xrinf0  13363  fac0  14298  cnrecnv  15187  cau3  15377  cbvsum  15714  cbvsumv  15715  sum0  15740  ackbijnn  15847  flo1  15873  trireciplem  15881  trirecip  15882  ege2le3  16109  rpnnen2lem3  16235  ruclem4  16253  bitsf1ocnv  16464  prmreclem6  16942  prmrec  16943  modxai  17089  strfvn  17206  strss  17226  xpsvsca  17598  mreacs  17677  2oppccomf  17744  setc2obas  18115  setc2ohom  18116  cat1  18118  mndprop  18747  grpprop  18944  isgrpi  18951  oppgmndb  19347  oppggrpb  19350  odfval  19523  efgrelexlemb  19741  ablprop  19784  ringprop  20260  opprrngb  20319  opprringb  20321  rlmbas  21167  rlmplusg  21168  rlm0  21169  rlmsub  21170  rlmmulr  21171  rlmsca2  21173  rlmvsca  21174  rlmtopn  21175  rlmds  21176  rlmvneg  21180  dfcnfldOLD  21347  cncrng  21368  cncrngOLD  21369  xrsmcmn  21371  cndrng  21378  cndrngOLD  21379  cnsrng  21385  xrs1mnd  21389  xrs10  21390  absabv  21409  zringcyg  21447  pzriprngALT  21473  resrng  21606  psrbagsn  22054  evlsval  22077  psr1bas2  22158  psr1bas  22159  psr1plusg  22189  psr1vsca  22190  psr1mulr  22191  ply1plusgfvi  22210  ply1mpl0  22225  ply1mpl1  22227  ordtrestixx  23195  llyidm  23461  nllyidm  23462  toplly  23463  hauslly  23465  hausnlly  23466  lly1stc  23469  kgenf  23514  txswaphmeolem  23777  fmucndlem  24264  nrgtrg  24666  cnfldnm  24754  xrsxmet  24786  divcnOLD  24845  divcn  24847  expcn  24851  expcnOLD  24853  elcncf1ii  24877  iirevcn  24912  iihalf1cn  24914  iihalf1cnOLD  24915  iihalf2cn  24917  iihalf2cnOLD  24918  iimulcn  24922  iimulcnOLD  24923  icopnfcnv  24928  iccpnfcnv  24930  cnrehmeo  24939  cnrehmeoOLD  24940  tcphsub  25210  tcphphl  25216  iscmet3i  25301  cncmet  25311  rrxprds  25378  vitali  25603  i1f0  25677  itg20  25727  cbvitgv  25767  dvid  25908  dveflem  25972  dvef  25973  dvsincos  25974  ply1divalg2  26133  coe0  26250  iaa  26322  sincn  26443  coscn  26444  reefgim  26449  pilem3  26452  resinf1o  26533  circgrp  26549  circsubm  26550  logi  26584  divlogrlim  26632  dvrelog  26634  logcn  26644  dvlog  26648  advlog  26651  cxpcn  26742  cxpcnOLD  26743  cxpcn2  26744  resqrtcn  26747  sqrtcn  26748  atansopn  26930  dvatan  26933  leibpilem2  26939  leibpi  26940  leibpisum  26941  log2cnv  26942  log2ublem2  26945  log2ub  26947  divsqrtsumlem  26978  emcllem4  26997  emcllem6  26999  emcllem7  27000  lgamf  27040  lgam1  27062  basellem6  27084  basellem7  27085  basellem8  27086  basellem9  27087  vmaf  27117  logfacrlim  27223  lgsdir2lem5  27328  chebbnd1  27471  chtppilim  27474  chto1ub  27475  chebbnd2  27476  chto1lb  27477  chpchtlim  27478  chpo1ub  27479  chpo1ubb  27480  vmadivsum  27481  vmadivsumb  27482  mudivsum  27529  mulogsumlem  27530  mulogsum  27531  logdivsum  27532  vmalogdivsum2  27537  vmalogdivsum  27538  selberglem1  27544  selberglem2  27545  selbergb  27548  selberg2lem  27549  selberg2  27550  selberg2b  27551  selberg3lem2  27557  selberg3  27558  selberg4  27560  pntrmax  27563  pntrsumo1  27564  pntrsumbnd  27565  selbergr  27567  selberg3r  27568  selberg4r  27569  selberg34r  27570  pntrlog2bndlem1  27576  pntrlog2bndlem4  27579  pnt2  27612  pnt  27613  dmscut  27811  lrrecpo  27929  noxpordpo  27938  noxpordfr  27939  noxpordse  27940  n0sex  28277  n0ssno  28280  0n0s  28289  n0scut  28293  n0sge0  28296  1p1e2s  28355  zseo  28361  nohalf  28362  0reno  28384  istrkg2ld  28423  legval  28547  ttgsub  28843  cchhllem  28851  2wspdisj  29929  2wspiundisj  29930  konigsbergiedgw  30214  ipasslem7  30802  normlem6  31081  opsqrlem4  32109  fpwrelmap  32691  fpwrelmapffs  32692  xrs0  32954  elrgspnlem2  33193  1fldgenq  33270  dfprm3  33522  zringfrac  33523  ccfldsrarelvec  33662  ccfldextdgrr  33663  constrextdg2  33731  2sqr3minply  33732  mdetlap1  33766  circtopn  33777  cnre2csqima  33851  cnvordtrestixx  33853  mndpluscn  33866  xrge0iifcnv  33873  zlm0  33900  zlm1  33901  qqhre  33962  rrhre  33963  esumnul  33990  hasheuni  34027  sxbrsigalem2  34229  oddpwdc  34297  eulerpartlemb  34311  eulerpartgbij  34315  eulerpartlemn  34324  fib0  34342  fib1  34343  ballotlemrinv  34477  sgn3da  34485  signsw0g  34512  circlemethnat  34597  dvelimalcasei  35031  dvelimexcasei  35033  subfacval2  35133  sinccvglem  35618  circum  35620  antnest  35635  faclim  35687  faclim2  35689  cnndvlem1  36479  bj-dvelimv  36795  bj-inrab2  36870  bj-rabtrAUTO  36874  bj-opelidb  37094  bj-iomnnom  37201  sucneqoni  37308  wl-df-3xor  37410  wl-3xorbi123i  37418  wl-df3maxtru1  37434  wl-cbvalnae  37475  wl-equsal  37483  poimirlem30  37598  dvtan  37618  dvasin  37652  dvacos  37653  dvreasin  37654  dvreacos  37655  efald2  38026  lcmineqlem7  41977  3lexlogpow5ineq1  41996  3lexlogpow5ineq5  42002  aks4d1p1p6  42015  cxpi11d  42324  tan3rdpi  42331  asin1half  42332  redvmptabs  42335  readvrec2  42336  readvrec  42337  resuppsinopn  42338  readvcot  42339  re1m1e0m0  42372  re0m0e0  42377  reixi  42397  subresre  42405  3cubeslem4  42645  3cubes  42646  areaquad  43173  clsk1indlem4  44002  clsk1indlem1  44003  ismnushort  44265  lhe4.4ex1a  44293  sbtT  44532  eel0TT  44669  eelTTT  44671  eelT1  44673  eelTT  44736  eelT  44738  eelT0  44740  isosctrlem1ALT  44899  disjsnxp  45020  infxr  45323  nfxneg  45417  limsup0  45654  0cnv  45702  limsup10ex  45733  liminf10ex  45734  liminfvalxr  45743  liminf0  45753  dvsinax  45873  itgsin0pilem1  45910  iblempty  45925  stowei  46024  wallispilem5  46029  wallispi  46030  stirlinglem1  46034  stirlinglem12  46045  stirlinglem13  46046  stirlinglem14  46047  stirlingr  46050  dirkertrigeqlem1  46058  fourierdlem62  46128  fourierdlem73  46139  fourierdlem76  46142  fourierdlem77  46143  fourierdlem103  46169  fourierdlem104  46170  fourierclim  46184  fourier  46185  fouriersw  46191  etransclem41  46235  etransclem46  46240  salexct2  46299  salexct3  46302  salgencntex  46303  salgensscntex  46304  dmvolsal  46306  bor1sal  46315  iocborel  46316  sge00  46336  sge0sn  46339  ovolval5lem3  46614  ioosshoi  46629  vonioolem2  46641  smfmullem4  46754  upwrdfi  46847  dfafv2  47090  ichim  47390  fucofulem2  48970  setc2othin  49079  setcsnterm  49102  termc2  49117  onsetrec  49223  joinlmuladdmuli  49288