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

Theorem trud 1533
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 1527 . 2
2 trud.1 . 2 (⊤ → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1524
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 1526
This theorem is referenced by:  hadbi123i  1575  cadbi123i  1590  nfan  1868  nfbi  1873  nfbiOLD  2279  spime  2292  nfeu  2514  nfmo  2515  eubii  2520  mobii  2521  abeq2i  2764  nfceqi  2790  nfeq  2805  nfel  2806  dvelimc  2816  nfral  2974  nfrex  3036  nfreu  3143  nfrmo  3144  nfrab  3153  rabbia2  3218  nfsbc1  3487  nfsbc  3490  sbcbii  3524  nfcsb1  3581  nfcsb  3584  csbeq2i  4026  nfif  4148  nfdisj  4664  nfbr  4732  mpteq12i  4775  ralxfr  4916  reuxfr2  4922  reuxfr  4924  issoi  5095  nfiota  5893  nfriota  6660  nfov  6716  mpt2eq123i  6760  mpt2eq3ia  6762  iseri  7814  nfixp  7969  en2i  8035  en3i  8036  ensymb  8045  entr  8049  r0weon  8873  recmulnq  9824  axcnex  10006  nfneg  10315  negiso  11041  suprzcl2  11816  supxr  12181  xrinf0  12206  cnrecnv  13949  cau3  14139  cbvsum  14469  sum0  14496  ackbijnn  14604  flo1  14630  trireciplem  14638  trirecip  14639  ege2le3  14864  rpnnen2lem3  14989  bitsf1ocnv  15213  prmreclem6  15672  prmrec  15673  modxai  15819  strfvn  15926  strss  15957  xpssca  16285  xpsvsca  16286  mreacs  16366  2oppccomf  16432  mndprop  17364  grpprop  17485  isgrpi  17492  oppgmndb  17831  oppggrpb  17834  efgrelexlemb  18209  ablprop  18250  ringprop  18630  opprringb  18678  rlmbas  19243  rlmplusg  19244  rlm0  19245  rlmsub  19246  rlmmulr  19247  rlmsca2  19249  rlmvsca  19250  rlmtopn  19251  rlmds  19252  rlmvneg  19255  psrbagsn  19543  evlsval  19567  psr1bas2  19608  psr1bas  19609  psr1plusg  19640  psr1vsca  19641  psr1mulr  19642  ply1plusgfvi  19660  ply1mpl0  19673  ply1mpl1  19675  cncrng  19815  xrsmcmn  19817  cndrng  19823  cnsrng  19828  xrs1mnd  19832  xrs10  19833  absabv  19851  zringcyg  19887  recrng  20015  ordtrestixx  21074  llyidm  21339  nllyidm  21340  toplly  21341  hauslly  21343  hausnlly  21344  lly1stc  21347  kgenf  21392  hmpher  21635  txswaphmeolem  21655  fmucndlem  22142  nrgtrg  22541  cnfldnm  22629  xrsxmet  22659  divcn  22718  expcn  22722  elcncf1ii  22746  iirevcn  22776  iihalf1cn  22778  iihalf2cn  22780  iimulcn  22784  icopnfcnv  22788  iccpnfcnv  22790  cnrehmeo  22799  tchsub  23066  tchphl  23072  iscmet3i  23156  cncmet  23165  rrxprds  23223  vitali  23427  i1f0  23499  itg20  23549  dvid  23726  dveflem  23787  dvef  23788  dvsincos  23789  ply1divalg2  23943  coe0  24057  iaa  24125  sincn  24243  coscn  24244  reefgim  24249  pilem3  24252  resinf1o  24327  circgrp  24343  circsubm  24344  divlogrlim  24426  dvrelog  24428  logcn  24438  dvlog  24442  advlog  24445  cxpcn  24531  cxpcn2  24532  resqrtcn  24535  sqrtcn  24536  atansopn  24704  dvatan  24707  leibpilem2  24713  leibpi  24714  leibpisum  24715  log2cnv  24716  log2ublem2  24719  log2ub  24721  divsqrtsumlem  24751  emcllem4  24770  emcllem6  24772  emcllem7  24773  lgamf  24813  lgam1  24835  basellem6  24857  basellem7  24858  basellem8  24859  basellem9  24860  vmaf  24890  logfacrlim  24994  lgsdir2lem5  25099  chebbnd1  25206  chtppilim  25209  chto1ub  25210  chebbnd2  25211  chto1lb  25212  chpchtlim  25213  chpo1ub  25214  chpo1ubb  25215  vmadivsum  25216  vmadivsumb  25217  mudivsum  25264  mulogsumlem  25265  mulogsum  25266  logdivsum  25267  vmalogdivsum2  25272  vmalogdivsum  25273  selberglem1  25279  selberglem2  25280  selbergb  25283  selberg2lem  25284  selberg2  25285  selberg2b  25286  selberg3lem2  25292  selberg3  25293  selberg4  25295  pntrmax  25298  pntrsumo1  25299  pntrsumbnd  25300  selbergr  25302  selberg3r  25303  selberg4r  25304  selberg34r  25305  pntrlog2bndlem1  25311  pntrlog2bndlem4  25314  pnt2  25347  pnt  25348  istrkg2ld  25404  legval  25524  ttgsub  25804  cchhllem  25812  trlsfval  26648  pthsfval  26673  spthsfval  26674  clwlks  26724  crcts  26739  cycls  26740  2wspdisj  26929  2wspiundisj  26930  eupths  27178  konigsbergiedgw  27226  ipasslem7  27819  normlem6  28100  opsqrlem4  29130  eqri  29443  fpwrelmap  29636  fpwrelmapffs  29637  xrs0  29803  mdetlap1  30020  circtopn  30032  cnre2csqima  30085  cnvordtrestixx  30087  mndpluscn  30100  xrge0iifcnv  30107  zlm0  30134  zlm1  30135  qqhre  30192  rrhre  30193  esumnul  30238  hasheuni  30275  sxbrsigalem2  30476  oddpwdc  30544  eulerpartlemb  30558  eulerpartgbij  30562  eulerpartlemn  30571  fib0  30589  fib1  30590  ballotlemrinv  30723  sgn3da  30731  signsw0g  30761  circlemethnat  30847  subfacval2  31295  sinccvglem  31692  circum  31694  logi  31746  faclim  31758  faclim2  31760  dmscut  32043  cnndvlem1  32653  bj-spimev  32845  bj-dvelimv  32961  bj-inrab2  33049  bj-rabtrAUTO  33054  sucneqoni  33344  wl-cbvalnae  33450  wl-equsal  33456  poimirlem30  33569  dvtan  33590  dvasin  33626  dvacos  33627  dvreasin  33628  dvreacos  33629  efald2  34007  areaquad  38119  clsk1indlem4  38659  clsk1indlem1  38660  lhe4.4ex1a  38845  sbtT  39100  eel0TT  39246  eelTTT  39248  eelT1  39250  eelTT  39315  eelT  39317  eelT0  39319  isosctrlem1ALT  39484  disjsnxp  39553  infxr  39896  nfxneg  40004  limsup0  40244  0cnv  40292  limsup10ex  40323  liminf10ex  40324  liminfvalxr  40333  liminf0  40343  dvsinax  40445  itgsin0pilem1  40483  iblempty  40499  stowei  40599  wallispilem5  40604  wallispi  40605  stirlinglem1  40609  stirlinglem12  40620  stirlinglem13  40621  stirlinglem14  40622  stirlingr  40625  dirkertrigeqlem1  40633  fourierdlem62  40703  fourierdlem73  40714  fourierdlem76  40717  fourierdlem77  40718  fourierdlem103  40744  fourierdlem104  40745  fourierclim  40759  fourier  40760  fouriersw  40766  etransclem41  40810  etransclem46  40815  salexct2  40875  salexct3  40878  salgencntex  40879  salgensscntex  40880  dmvolsal  40882  bor1sal  40891  iocborel  40892  sge00  40911  sge0sn  40914  ovolval5lem3  41189  ioosshoi  41204  vonioolem2  41216  smfmullem4  41322  onsetrec  42779  joinlmuladdmuli  42847
  Copyright terms: Public domain W3C validator