Theorem trud 1493

Description: Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. (Contributed by Mario Carneiro, 13-Mar-2014.)

Hypothesis

Ref	Expression
trud.1	⊢ (⊤ → 𝜑)

Assertion

Ref	Expression
trud	⊢ 𝜑

Proof of Theorem trud

Step	Hyp	Ref	Expression
1		tru 1487	. 2 ⊢ ⊤
2		trud.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1484

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 197  df-tru 1486

This theorem is referenced by:  hadbi123i  1535  cadbi123i  1550  nfan  1828  nfbi  1833  nfbiOLD  2243  spime  2256  nfeu  2486  nfmo  2487  eubii  2492  mobii  2493  abeq2i  2735  nfceqi  2761  nfeq  2776  nfel  2777  dvelimc  2787  nfral  2945  nfrex  3007  nfreu  3114  nfrmo  3115  nfrab  3123  rabbia2  3187  nfsbc1  3454  nfsbc  3457  sbcbii  3491  nfcsb1  3548  nfcsb  3551  csbeq2i  3993  nfif  4115  nfdisj  4632  ssbri  4697  nfbr  4699  mpteq12i  4742  ralxfr  4886  reuxfr2  4892  reuxfr  4894  issoi  5066  nfiota  5855  nfriota  6620  nfov  6676  mpt2eq123i  6718  mpt2eq3ia  6720  iseri  7769  eqerOLD  7778  0erOLD  7781  ecopoverOLD  7852  nfixp  7927  en2i  7993  en3i  7994  enerOLD  8003  ensymb  8004  entr  8008  r0weon  8835  recmulnq  9786  axcnex  9968  nfneg  10277  negiso  11003  suprzcl2  11778  supxr  12143  xrinf0  12168  cnrecnv  13905  cau3  14095  cbvsum  14425  sum0  14452  ackbijnn  14560  flo1  14586  trireciplem  14594  trirecip  14595  ege2le3  14820  rpnnen2lem3  14945  bitsf1ocnv  15166  prmreclem6  15625  prmrec  15626  modxai  15772  strfvn  15879  strss  15910  xpssca  16238  xpsvsca  16239  mreacs  16319  2oppccomf  16385  mndprop  17317  grpprop  17438  isgrpi  17445  gicerOLD  17719  oppgmndb  17785  oppggrpb  17788  efgrelexlemb  18163  ablprop  18204  ringprop  18584  opprringb  18632  rlmbas  19195  rlmplusg  19196  rlm0  19197  rlmsub  19198  rlmmulr  19199  rlmsca2  19201  rlmvsca  19202  rlmtopn  19203  rlmds  19204  rlmvneg  19207  psrbagsn  19495  evlsval  19519  psr1bas2  19560  psr1bas  19561  psr1plusg  19592  psr1vsca  19593  psr1mulr  19594  ply1plusgfvi  19612  ply1mpl0  19625  ply1mpl1  19627  cncrng  19767  xrsmcmn  19769  cndrng  19775  cnsrng  19780  xrs1mnd  19784  xrs10  19785  absabv  19803  zringcyg  19839  recrng  19967  ordtrestixx  21026  llyidm  21291  nllyidm  21292  toplly  21293  hauslly  21295  hausnlly  21296  lly1stc  21299  kgenf  21344  hmpher  21587  txswaphmeolem  21607  fmucndlem  22095  nrgtrg  22494  cnfldnm  22582  xrsxmet  22612  divcn  22671  expcn  22675  elcncf1ii  22699  iirevcn  22729  iihalf1cn  22731  iihalf2cn  22733  iimulcn  22737  icopnfcnv  22741  iccpnfcnv  22743  cnrehmeo  22752  phtpcerOLD  22795  tchsub  23020  tchphl  23026  iscmet3i  23110  cncmet  23119  rrxprds  23177  vitalilem1OLD  23377  vitali  23382  i1f0  23454  itg20  23504  dvid  23681  dveflem  23742  dvef  23743  dvsincos  23744  ply1divalg2  23898  coe0  24012  iaa  24080  sincn  24198  coscn  24199  reefgim  24204  pilem3  24207  resinf1o  24282  circgrp  24298  circsubm  24299  divlogrlim  24381  dvrelog  24383  logcn  24393  dvlog  24397  advlog  24400  cxpcn  24486  cxpcn2  24487  resqrtcn  24490  sqrtcn  24491  atansopn  24659  dvatan  24662  leibpilem2  24668  leibpi  24669  leibpisum  24670  log2cnv  24671  log2ublem2  24674  log2ub  24676  divsqrtsumlem  24706  emcllem4  24725  emcllem6  24727  emcllem7  24728  lgamf  24768  lgam1  24790  basellem6  24812  basellem7  24813  basellem8  24814  basellem9  24815  vmaf  24845  logfacrlim  24949  lgsdir2lem5  25054  chebbnd1  25161  chtppilim  25164  chto1ub  25165  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  chpo1ubb  25170  vmadivsum  25171  vmadivsumb  25172  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  logdivsum  25222  vmalogdivsum2  25227  vmalogdivsum  25228  selberglem1  25234  selberglem2  25235  selbergb  25238  selberg2lem  25239  selberg2  25240  selberg2b  25241  selberg3lem2  25247  selberg3  25248  selberg4  25250  pntrmax  25253  pntrsumo1  25254  pntrsumbnd  25255  selbergr  25257  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntrlog2bndlem1  25266  pntrlog2bndlem4  25269  pnt2  25302  pnt  25303  istrkg2ld  25359  legval  25479  ttgsub  25759  cchhllem  25767  trlsfval  26592  pthsfval  26617  spthsfval  26618  clwlks  26668  crcts  26683  cycls  26684  2wspdisj  26855  2wspiundisj  26856  eupths  27060  konigsbergiedgw  27108  ipasslem7  27691  normlem6  27972  opsqrlem4  29002  eqri  29315  aciunf1  29463  fpwrelmap  29508  fpwrelmapffs  29509  xrs0  29675  mdetlap1  29892  circtopn  29904  cnre2csqima  29957  cnvordtrestixx  29959  mndpluscn  29972  xrge0iifcnv  29979  zlm0  30006  zlm1  30007  qqhre  30064  rrhre  30065  esumnul  30110  hasheuni  30147  sxbrsigalem2  30348  oddpwdc  30416  eulerpartlemb  30430  eulerpartgbij  30434  eulerpartlemn  30443  fib0  30461  fib1  30462  ballotlemrinv  30595  sgn3da  30603  signsw0g  30633  circlemethnat  30719  subfacval2  31169  sinccvglem  31566  circum  31568  logi  31620  faclim  31632  faclim2  31634  dmscut  31918  cnndvlem1  32528  bj-spimev  32720  bj-dvelimv  32836  bj-inrab2  32924  bj-rabtrAUTO  32929  sucneqoni  33214  wl-cbvalnae  33320  wl-equsal  33326  poimirlem30  33439  dvtan  33460  dvasin  33496  dvacos  33497  dvreasin  33498  dvreacos  33499  efald2  33877  areaquad  37802  clsk1indlem4  38342  clsk1indlem1  38343  lhe4.4ex1a  38528  sbtT  38783  eel0TT  38929  eelTTT  38931  eelT1  38933  eelTT  38998  eelT  39000  eelT0  39002  isosctrlem1ALT  39170  disjsnxp  39239  infxr  39583  nfxneg  39691  limsup0  39926  0cnv  39974  limsup10ex  40005  liminf10ex  40006  liminfvalxr  40015  liminf0  40025  dvsinax  40127  itgsin0pilem1  40165  iblempty  40181  stowei  40281  wallispilem5  40286  wallispi  40287  stirlinglem1  40291  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlingr  40307  dirkertrigeqlem1  40315  fourierdlem62  40385  fourierdlem73  40396  fourierdlem76  40399  fourierdlem77  40400  fourierdlem103  40426  fourierdlem104  40427  fourierclim  40441  fourier  40442  fouriersw  40448  etransclem41  40492  etransclem46  40497  salexct2  40557  salexct3  40560  salgencntex  40561  salgensscntex  40562  dmvolsal  40564  bor1sal  40573  iocborel  40574  sge00  40593  sge0sn  40596  ovolval5lem3  40868  ioosshoi  40883  vonioolem2  40895  smfmullem4  41001  onsetrec  42451  joinlmuladdmuli  42519