MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trud Structured version   Visualization version   GIF version

Theorem trud 1490
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
StepHypRef Expression
1 tru 1484 . 2
2 trud.1 . 2 (⊤ → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1481
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 1483
This theorem is referenced by:  hadbi123i  1532  cadbi123i  1547  nfan  1825  nfbi  1830  nfbiOLD  2242  spime  2255  nfeu  2485  nfmo  2486  eubii  2491  mobii  2492  abeq2i  2732  nfceqi  2758  nfeq  2772  nfel  2773  dvelimc  2783  nfral  2941  nfrex  3003  nfreu  3108  nfrmo  3109  nfrab  3116  rabbia2  3179  nfsbc1  3441  nfsbc  3444  sbcbii  3478  nfcsb1  3534  nfcsb  3537  csbeq2i  3971  nfif  4093  nfdisj  4605  ssbri  4667  nfbr  4669  mpteq12i  4712  ralxfr  4856  reuxfr2  4862  reuxfr  4864  issoi  5036  nfiota  5824  nfriota  6585  nfov  6641  mpt2eq123i  6683  mpt2eq3ia  6685  iseri  7729  eqerOLD  7738  0erOLD  7741  ecopoverOLD  7812  nfixp  7887  en2i  7953  en3i  7954  enerOLD  7963  ensymb  7964  entr  7968  r0weon  8795  recmulnq  9746  axcnex  9928  nfneg  10237  negiso  10963  suprzcl2  11738  supxr  12102  xrinf0  12126  cnrecnv  13855  cau3  14045  cbvsum  14375  sum0  14401  ackbijnn  14504  flo1  14530  trireciplem  14538  trirecip  14539  ege2le3  14764  rpnnen2lem3  14889  bitsf1ocnv  15109  prmreclem6  15568  prmrec  15569  modxai  15715  strfvn  15820  strss  15850  xpssca  16178  xpsvsca  16179  mreacs  16259  2oppccomf  16325  mndprop  17257  grpprop  17378  isgrpi  17385  gicerOLD  17659  oppgmndb  17725  oppggrpb  17728  efgrelexlemb  18103  ablprop  18144  ringprop  18524  opprringb  18572  rlmbas  19135  rlmplusg  19136  rlm0  19137  rlmsub  19138  rlmmulr  19139  rlmsca2  19141  rlmvsca  19142  rlmtopn  19143  rlmds  19144  rlmvneg  19147  psrbagsn  19435  evlsval  19459  psr1bas2  19500  psr1bas  19501  psr1plusg  19532  psr1vsca  19533  psr1mulr  19534  ply1plusgfvi  19552  ply1mpl0  19565  ply1mpl1  19567  cncrng  19707  xrsmcmn  19709  cndrng  19715  cnsrng  19720  xrs1mnd  19724  xrs10  19725  absabv  19743  zringcyg  19779  recrng  19907  ordtrestixx  20966  llyidm  21231  nllyidm  21232  toplly  21233  hauslly  21235  hausnlly  21236  lly1stc  21239  kgenf  21284  hmpher  21527  txswaphmeolem  21547  fmucndlem  22035  nrgtrg  22434  cnfldnm  22522  xrsxmet  22552  divcn  22611  expcn  22615  elcncf1ii  22639  iirevcn  22669  iihalf1cn  22671  iihalf2cn  22673  iimulcn  22677  icopnfcnv  22681  iccpnfcnv  22683  cnrehmeo  22692  phtpcerOLD  22735  tchsub  22960  tchphl  22966  iscmet3i  23050  cncmet  23059  rrxprds  23117  vitalilem1OLD  23317  vitali  23322  i1f0  23394  itg20  23444  dvid  23621  dveflem  23680  dvef  23681  dvsincos  23682  ply1divalg2  23836  coe0  23950  iaa  24018  sincn  24136  coscn  24137  reefgim  24142  pilem3  24145  resinf1o  24220  circgrp  24236  circsubm  24237  divlogrlim  24315  dvrelog  24317  logcn  24327  dvlog  24331  advlog  24334  cxpcn  24420  cxpcn2  24421  resqrtcn  24424  sqrtcn  24425  atansopn  24593  dvatan  24596  leibpilem2  24602  leibpi  24603  leibpisum  24604  log2cnv  24605  log2ublem2  24608  log2ub  24610  divsqrtsumlem  24640  emcllem4  24659  emcllem6  24661  emcllem7  24662  lgamf  24702  lgam1  24724  basellem6  24746  basellem7  24747  basellem8  24748  basellem9  24749  vmaf  24779  logfacrlim  24883  lgsdir2lem5  24988  chebbnd1  25095  chtppilim  25098  chto1ub  25099  chebbnd2  25100  chto1lb  25101  chpchtlim  25102  chpo1ub  25103  chpo1ubb  25104  vmadivsum  25105  vmadivsumb  25106  mudivsum  25153  mulogsumlem  25154  mulogsum  25155  logdivsum  25156  vmalogdivsum2  25161  vmalogdivsum  25162  selberglem1  25168  selberglem2  25169  selbergb  25172  selberg2lem  25173  selberg2  25174  selberg2b  25175  selberg3lem2  25181  selberg3  25182  selberg4  25184  pntrmax  25187  pntrsumo1  25188  pntrsumbnd  25189  selbergr  25191  selberg3r  25192  selberg4r  25193  selberg34r  25194  pntrlog2bndlem1  25200  pntrlog2bndlem4  25203  pnt2  25236  pnt  25237  istrkg2ld  25293  legval  25413  ttgsub  25693  cchhllem  25701  trlsfval  26495  pthsfval  26520  spthsfval  26521  clwlks  26571  crcts  26586  cycls  26587  eupths  26960  konigsbergiedgw  27008  ipasslem7  27579  normlem6  27860  opsqrlem4  28890  eqri  29239  aciunf1  29346  fpwrelmap  29392  fpwrelmapffs  29393  xrs0  29502  mdetlap1  29716  circtopn  29728  cnre2csqima  29781  cnvordtrestixx  29783  mndpluscn  29796  xrge0iifcnv  29803  zlm0  29830  zlm1  29831  qqhre  29888  rrhre  29889  esumnul  29933  hasheuni  29970  sxbrsigalem2  30171  oddpwdc  30239  eulerpartlemb  30253  eulerpartgbij  30257  eulerpartlemn  30266  fib0  30284  fib1  30285  ballotlemrinv  30418  sgn3da  30426  signsw0g  30455  subfacval2  30930  sinccvglem  31327  circum  31329  logi  31381  faclim  31393  faclim2  31395  cnndvlem1  32223  bj-spimev  32415  bj-dvelimv  32534  bj-inrab2  32624  bj-rabtrAUTO  32629  sucneqoni  32885  wl-cbvalnae  32991  wl-equsal  32997  poimirlem30  33110  dvtan  33131  dvasin  33167  dvacos  33168  dvreasin  33169  dvreacos  33170  efald2  33548  areaquad  37322  clsk1indlem4  37863  clsk1indlem1  37864  lhe4.4ex1a  38049  sbtT  38304  eel0TT  38450  eelTTT  38452  eelT1  38454  eelTT  38519  eelT  38521  eelT0  38523  isosctrlem1ALT  38692  disjsnxp  38761  infxr  39082  limsup0  39362  dvsinax  39463  itgsin0pilem1  39502  iblempty  39518  stowei  39618  wallispilem5  39623  wallispi  39624  stirlinglem1  39628  stirlinglem12  39639  stirlinglem13  39640  stirlinglem14  39641  stirlingr  39644  dirkertrigeqlem1  39652  fourierdlem62  39722  fourierdlem73  39733  fourierdlem76  39736  fourierdlem77  39737  fourierdlem103  39763  fourierdlem104  39764  fourierclim  39778  fourier  39779  fouriersw  39785  etransclem41  39829  etransclem46  39834  salexct2  39894  salexct3  39897  salgencntex  39898  salgensscntex  39899  dmvolsal  39901  bor1sal  39910  iocborel  39911  sge00  39930  sge0sn  39933  ovolval5lem3  40205  ioosshoi  40220  vonioolem2  40232  smfmullem4  40338  onsetrec  41774  joinlmuladdmuli  41852
  Copyright terms: Public domain W3C validator