Theorem mptru 1547

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

Syntax hints:   → wi 4  ⊤wtru 1541

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 1543

This theorem is referenced by:  hadbi123i  1596  cadbi123i  1611  nfan  1899  nfbi  1903  spimefv  2199  spime  2387  nfsb  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  eqabi  2863  eqabri  2871  nfeq  2905  nfel  2906  dvelimc  2917  nfrexw  3284  nfral  3345  nfrex  3346  nfrmo  3400  nfreu  3401  rabbia2  3405  rabeqc  3415  nfrabw  3440  nfrab  3442  reuxfr  3717  reuxfr1  3720  nfsbc1  3769  nfsbcw  3772  nfsbc  3775  sbcbii  3807  csbeq2i  3867  nfcsb1  3882  nfcsbw  3885  nfcsb  3886  eqri  3964  vn0  4304  nfif  4515  nfdisjw  5081  nfdisj  5082  nfbr  5149  nfopab  5171  mpteq1i  5193  mpteq2ia  5197  mpteq12i  5199  ralxfr  5364  issoi  5575  nfiotaw  6456  nfiota  6458  nfriota  7338  nfov  7399  mpoeq123i  7445  mpoeq3ia  7447  opco1i  8081  xpord2indlem  8103  on2recsfn  8608  on2recsov  8609  iseri  8675  nfixpw  8866  nfixp  8867  en2i  8938  en3i  8939  ensymb  8950  entr  8954  1sdom2dom  9170  nfttrcl  9640  djulf1o  9841  djurf1o  9842  r0weon  9941  recmulnq  10893  nrex1  10993  nfneg  11393  negiso  12139  suprzcl2  12873  supxr  13249  xrinf0  13275  fac0  14217  cnrecnv  15107  cau3  15298  cbvsum  15637  cbvsumv  15638  sum0  15663  ackbijnn  15770  flo1  15796  trireciplem  15804  trirecip  15805  ege2le3  16032  rpnnen2lem3  16160  ruclem4  16178  bitsf1ocnv  16390  prmreclem6  16868  prmrec  16869  modxai  17015  strfvn  17132  strss  17152  xpsvsca  17516  mreacs  17595  2oppccomf  17662  setc2obas  18032  setc2ohom  18033  cat1  18035  mndprop  18663  grpprop  18860  isgrpi  18867  oppgmndb  19263  oppggrpb  19266  odfval  19438  efgrelexlemb  19656  ablprop  19699  ringprop  20175  opprrngb  20231  opprringb  20233  rlmbas  21076  rlmplusg  21077  rlm0  21078  rlmsub  21079  rlmmulr  21080  rlmsca2  21082  rlmvsca  21083  rlmtopn  21084  rlmds  21085  rlmvneg  21089  dfcnfldOLD  21256  cncrng  21276  cncrngOLD  21277  xrsmcmn  21279  cndrng  21286  cndrngOLD  21287  cnsrng  21293  xrs1mnd  21297  xrs10  21298  absabv  21317  zringcyg  21355  pzriprngALT  21381  resrng  21506  psrbagsn  21946  evlsval  21969  psr1bas2  22050  psr1bas  22051  psr1plusg  22081  psr1vsca  22082  psr1mulr  22083  ply1plusgfvi  22102  ply1mpl0  22117  ply1mpl1  22119  ordtrestixx  23085  llyidm  23351  nllyidm  23352  toplly  23353  hauslly  23355  hausnlly  23356  lly1stc  23359  kgenf  23404  txswaphmeolem  23667  fmucndlem  24154  nrgtrg  24554  cnfldnm  24642  xrsxmet  24674  divcnOLD  24733  divcn  24735  expcn  24739  expcnOLD  24741  elcncf1ii  24765  iirevcn  24800  iihalf1cn  24802  iihalf1cnOLD  24803  iihalf2cn  24805  iihalf2cnOLD  24806  iimulcn  24810  iimulcnOLD  24811  icopnfcnv  24816  iccpnfcnv  24818  cnrehmeo  24827  cnrehmeoOLD  24828  tcphsub  25097  tcphphl  25103  iscmet3i  25188  cncmet  25198  rrxprds  25265  vitali  25490  i1f0  25564  itg20  25614  cbvitgv  25654  dvid  25795  dveflem  25859  dvef  25860  dvsincos  25861  ply1divalg2  26020  coe0  26137  iaa  26209  sincn  26330  coscn  26331  reefgim  26336  pilem3  26339  resinf1o  26421  circgrp  26437  circsubm  26438  logi  26472  divlogrlim  26520  dvrelog  26522  logcn  26532  dvlog  26536  advlog  26539  cxpcn  26630  cxpcnOLD  26631  cxpcn2  26632  resqrtcn  26635  sqrtcn  26636  atansopn  26818  dvatan  26821  leibpilem2  26827  leibpi  26828  leibpisum  26829  log2cnv  26830  log2ublem2  26833  log2ub  26835  divsqrtsumlem  26866  emcllem4  26885  emcllem6  26887  emcllem7  26888  lgamf  26928  lgam1  26950  basellem6  26972  basellem7  26973  basellem8  26974  basellem9  26975  vmaf  27005  logfacrlim  27111  lgsdir2lem5  27216  chebbnd1  27359  chtppilim  27362  chto1ub  27363  chebbnd2  27364  chto1lb  27365  chpchtlim  27366  chpo1ub  27367  chpo1ubb  27368  vmadivsum  27369  vmadivsumb  27370  mudivsum  27417  mulogsumlem  27418  mulogsum  27419  logdivsum  27420  vmalogdivsum2  27425  vmalogdivsum  27426  selberglem1  27432  selberglem2  27433  selbergb  27436  selberg2lem  27437  selberg2  27438  selberg2b  27439  selberg3lem2  27445  selberg3  27446  selberg4  27448  pntrmax  27451  pntrsumo1  27452  pntrsumbnd  27453  selbergr  27455  selberg3r  27456  selberg4r  27457  selberg34r  27458  pntrlog2bndlem1  27464  pntrlog2bndlem4  27467  pnt2  27500  pnt  27501  dmscut  27699  lrrecpo  27824  noxpordpo  27833  noxpordfr  27834  noxpordse  27835  n0sex  28186  n0ssno  28189  0n0s  28198  n0scut  28202  n0sge0  28206  1p1e2s  28278  zseo  28284  twocut  28285  nohalf  28286  halfcut  28309  0reno  28324  istrkg2ld  28363  legval  28487  ttgsub  28782  cchhllem  28790  2wspdisj  29865  2wspiundisj  29866  konigsbergiedgw  30150  ipasslem7  30738  normlem6  31017  opsqrlem4  32045  fpwrelmap  32629  fpwrelmapffs  32630  sgn3da  32732  xrs0  32917  elrgspnlem2  33167  1fldgenq  33245  dfprm3  33497  zringfrac  33498  ccfldsrarelvec  33639  ccfldextdgrr  33640  constrextdg2  33712  iconstr  33729  constrsdrg  33738  2sqr3minply  33743  2sqr3nconstr  33744  cos9thpiminplylem3  33747  cos9thpiminply  33751  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  mdetlap1  33789  circtopn  33800  cnre2csqima  33874  cnvordtrestixx  33876  mndpluscn  33889  xrge0iifcnv  33896  zlm0  33923  zlm1  33924  qqhre  33983  rrhre  33984  esumnul  34011  hasheuni  34048  sxbrsigalem2  34250  oddpwdc  34318  eulerpartlemb  34332  eulerpartgbij  34336  eulerpartlemn  34345  fib0  34363  fib1  34364  ballotlemrinv  34498  signsw0g  34520  circlemethnat  34605  dvelimalcasei  35039  dvelimexcasei  35041  subfacval2  35147  sinccvglem  35632  circum  35634  antnest  35649  antnestALT  35654  faclim  35706  faclim2  35708  cnndvlem1  36498  bj-dvelimv  36814  bj-inrab2  36889  bj-rabtrAUTO  36893  bj-opelidb  37113  bj-iomnnom  37220  sucneqoni  37327  wl-df-3xor  37429  wl-3xorbi123i  37437  wl-df3maxtru1  37453  wl-cbvalnae  37494  wl-equsal  37502  poimirlem30  37617  dvtan  37637  dvasin  37671  dvacos  37672  dvreasin  37673  dvreacos  37674  efald2  38045  lcmineqlem7  41996  3lexlogpow5ineq1  42015  3lexlogpow5ineq5  42021  aks4d1p1p6  42034  cxpi11d  42304  tan3rdpi  42313  asin1half  42318  redvmptabs  42321  readvrec2  42322  readvrec  42323  resuppsinopn  42324  readvcot  42325  re1m1e0m0  42358  re0m0e0  42363  reixi  42384  subresre  42392  3cubeslem4  42650  3cubes  42651  areaquad  43178  clsk1indlem4  44006  clsk1indlem1  44007  ismnushort  44263  lhe4.4ex1a  44291  sbtT  44530  eel0TT  44666  eelTTT  44668  eelT1  44670  eelTT  44733  eelT  44735  eelT0  44737  isosctrlem1ALT  44896  disjsnxp  45037  infxr  45336  nfxneg  45430  limsup0  45665  0cnv  45713  limsup10ex  45744  liminf10ex  45745  liminfvalxr  45754  liminf0  45764  dvsinax  45884  itgsin0pilem1  45921  iblempty  45936  stowei  46035  wallispilem5  46040  wallispi  46041  stirlinglem1  46045  stirlinglem12  46056  stirlinglem13  46057  stirlinglem14  46058  stirlingr  46061  dirkertrigeqlem1  46069  fourierdlem62  46139  fourierdlem73  46150  fourierdlem76  46153  fourierdlem77  46154  fourierdlem103  46180  fourierdlem104  46181  fourierclim  46195  fourier  46196  fouriersw  46202  etransclem41  46246  etransclem46  46251  salexct2  46310  salexct3  46313  salgencntex  46314  salgensscntex  46315  dmvolsal  46317  bor1sal  46326  iocborel  46327  sge00  46347  sge0sn  46350  ovolval5lem3  46625  ioosshoi  46640  vonioolem2  46652  smfmullem4  46765  upwrdfi  46858  cjnpoly  46863  dfafv2  47106  ichim  47431  nelsubc3  49033  fucofulem2  49273  setc2othin  49428  setcsnterm  49452  setc1obas  49454  setc1ohomfval  49455  setc1ocofval  49456  setc1oid  49457  termc2  49480  setc1onsubc  49564  onsetrec  49670  joinlmuladdmuli  49735