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

Theorem trud 1642
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 1636 . 2
2 trud.1 . 2 (⊤ → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1633
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 1635
This theorem is referenced by:  hadbi123i  1684  cadbi123i  1699  nfan  1977  nfbi  1982  nfbiOLD  2388  spime  2401  nfeu  2623  nfmo  2624  eubii  2629  mobii  2630  abeq2i  2873  nfceqi  2899  nfeq  2914  nfel  2915  dvelimc  2925  nfral  3083  nfrex  3145  nfreu  3252  nfrmo  3253  nfrab  3262  rabbia2  3327  nfsbc1  3595  nfsbc  3598  sbcbii  3632  nfcsb1  3689  nfcsb  3692  csbeq2i  4136  nfif  4259  nfdisj  4784  nfbr  4851  mpteq12i  4894  ralxfr  5035  reuxfr2  5041  reuxfr  5043  issoi  5218  nfiota  6016  nfriota  6783  nfov  6839  mpt2eq123i  6883  mpt2eq3ia  6885  iseri  7938  nfixp  8093  en2i  8159  en3i  8160  ensymb  8169  entr  8173  djulf1o  8946  djurf1o  8947  r0weon  9025  recmulnq  9978  axcnex  10160  nfneg  10469  negiso  11195  suprzcl2  11971  supxr  12336  xrinf0  12361  cnrecnv  14104  cau3  14294  cbvsum  14624  sum0  14651  ackbijnn  14759  flo1  14785  trireciplem  14793  trirecip  14794  ege2le3  15019  rpnnen2lem3  15144  bitsf1ocnv  15368  prmreclem6  15827  prmrec  15828  modxai  15974  strfvn  16081  strss  16112  xpssca  16440  xpsvsca  16441  mreacs  16520  2oppccomf  16586  mndprop  17518  grpprop  17639  isgrpi  17646  oppgmndb  17985  oppggrpb  17988  efgrelexlemb  18363  ablprop  18404  ringprop  18784  opprringb  18832  rlmbas  19397  rlmplusg  19398  rlm0  19399  rlmsub  19400  rlmmulr  19401  rlmsca2  19403  rlmvsca  19404  rlmtopn  19405  rlmds  19406  rlmvneg  19409  psrbagsn  19697  evlsval  19721  psr1bas2  19762  psr1bas  19763  psr1plusg  19794  psr1vsca  19795  psr1mulr  19796  ply1plusgfvi  19814  ply1mpl0  19827  ply1mpl1  19829  cncrng  19969  xrsmcmn  19971  cndrng  19977  cnsrng  19982  xrs1mnd  19986  xrs10  19987  absabv  20005  zringcyg  20041  recrng  20169  ordtrestixx  21228  llyidm  21493  nllyidm  21494  toplly  21495  hauslly  21497  hausnlly  21498  lly1stc  21501  kgenf  21546  hmpher  21789  txswaphmeolem  21809  fmucndlem  22296  nrgtrg  22695  cnfldnm  22783  xrsxmet  22813  divcn  22872  expcn  22876  elcncf1ii  22900  iirevcn  22930  iihalf1cn  22932  iihalf2cn  22934  iimulcn  22938  icopnfcnv  22942  iccpnfcnv  22944  cnrehmeo  22953  tchsub  23220  tchphl  23226  iscmet3i  23310  cncmet  23319  rrxprds  23377  vitali  23581  i1f0  23653  itg20  23703  dvid  23880  dveflem  23941  dvef  23942  dvsincos  23943  ply1divalg2  24097  coe0  24211  iaa  24279  sincn  24397  coscn  24398  reefgim  24403  pilem3  24406  resinf1o  24481  circgrp  24497  circsubm  24498  divlogrlim  24580  dvrelog  24582  logcn  24592  dvlog  24596  advlog  24599  cxpcn  24685  cxpcn2  24686  resqrtcn  24689  sqrtcn  24690  atansopn  24858  dvatan  24861  leibpilem2  24867  leibpi  24868  leibpisum  24869  log2cnv  24870  log2ublem2  24873  log2ub  24875  divsqrtsumlem  24905  emcllem4  24924  emcllem6  24926  emcllem7  24927  lgamf  24967  lgam1  24989  basellem6  25011  basellem7  25012  basellem8  25013  basellem9  25014  vmaf  25044  logfacrlim  25148  lgsdir2lem5  25253  chebbnd1  25360  chtppilim  25363  chto1ub  25364  chebbnd2  25365  chto1lb  25366  chpchtlim  25367  chpo1ub  25368  chpo1ubb  25369  vmadivsum  25370  vmadivsumb  25371  mudivsum  25418  mulogsumlem  25419  mulogsum  25420  logdivsum  25421  vmalogdivsum2  25426  vmalogdivsum  25427  selberglem1  25433  selberglem2  25434  selbergb  25437  selberg2lem  25438  selberg2  25439  selberg2b  25440  selberg3lem2  25446  selberg3  25447  selberg4  25449  pntrmax  25452  pntrsumo1  25453  pntrsumbnd  25454  selbergr  25456  selberg3r  25457  selberg4r  25458  selberg34r  25459  pntrlog2bndlem1  25465  pntrlog2bndlem4  25468  pnt2  25501  pnt  25502  istrkg2ld  25558  legval  25678  ttgsub  25958  cchhllem  25966  trlsfval  26802  pthsfval  26827  spthsfval  26828  clwlks  26878  crcts  26894  cycls  26895  2wspdisj  27084  2wspiundisj  27085  eupths  27352  konigsbergiedgw  27400  ipasslem7  28000  normlem6  28281  opsqrlem4  29311  eqri  29624  fpwrelmap  29817  fpwrelmapffs  29818  xrs0  29984  mdetlap1  30201  circtopn  30213  cnre2csqima  30266  cnvordtrestixx  30268  mndpluscn  30281  xrge0iifcnv  30288  zlm0  30315  zlm1  30316  qqhre  30373  rrhre  30374  esumnul  30419  hasheuni  30456  sxbrsigalem2  30657  oddpwdc  30725  eulerpartlemb  30739  eulerpartgbij  30743  eulerpartlemn  30752  fib0  30770  fib1  30771  ballotlemrinv  30904  sgn3da  30912  signsw0g  30942  circlemethnat  31028  subfacval2  31476  sinccvglem  31873  circum  31875  logi  31927  faclim  31939  faclim2  31941  dmscut  32224  cnndvlem1  32834  bj-spimev  33026  bj-dvelimv  33142  bj-inrab2  33230  bj-rabtrAUTO  33235  sucneqoni  33525  wl-cbvalnae  33633  wl-equsal  33639  poimirlem30  33752  dvtan  33773  dvasin  33809  dvacos  33810  dvreasin  33811  dvreacos  33812  efald2  34190  areaquad  38304  clsk1indlem4  38844  clsk1indlem1  38845  lhe4.4ex1a  39030  sbtT  39285  eel0TT  39431  eelTTT  39433  eelT1  39435  eelTT  39500  eelT  39502  eelT0  39504  isosctrlem1ALT  39669  disjsnxp  39738  infxr  40081  nfxneg  40189  limsup0  40429  0cnv  40477  limsup10ex  40508  liminf10ex  40509  liminfvalxr  40518  liminf0  40528  dvsinax  40630  itgsin0pilem1  40668  iblempty  40684  stowei  40784  wallispilem5  40789  wallispi  40790  stirlinglem1  40794  stirlinglem12  40805  stirlinglem13  40806  stirlinglem14  40807  stirlingr  40810  dirkertrigeqlem1  40818  fourierdlem62  40888  fourierdlem73  40899  fourierdlem76  40902  fourierdlem77  40903  fourierdlem103  40929  fourierdlem104  40930  fourierclim  40944  fourier  40945  fouriersw  40951  etransclem41  40995  etransclem46  41000  salexct2  41060  salexct3  41063  salgencntex  41064  salgensscntex  41065  dmvolsal  41067  bor1sal  41076  iocborel  41077  sge00  41096  sge0sn  41099  ovolval5lem3  41374  ioosshoi  41389  vonioolem2  41401  smfmullem4  41507  onsetrec  42964  joinlmuladdmuli  43032
  Copyright terms: Public domain W3C validator