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

Theorem trud 1484
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 1479 . 2
2 trud.1 . 2 (⊤ → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1476
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 196  df-tru 1478
This theorem is referenced by:  hadbi123i  1526  cadbi123i  1541  nfim  1813  nfan  1816  nfbi  1821  nfbiOLD  2231  spime  2244  nfeu  2474  nfmo  2475  eubii  2480  mobii  2481  abeq2i  2722  nfceqi  2748  nfeq  2762  nfel  2763  dvelimc  2773  nfral  2929  nfrex  2990  nfreu  3093  nfrmo  3094  nfrab  3100  nfsbc1  3421  nfsbc  3424  sbcbii  3458  nfcsb1  3514  nfcsb  3517  csbeq2i  3945  nfif  4065  nfdisj  4565  ssbri  4627  nfbr  4629  mpteq12i  4670  ralxfr  4812  reuxfr2  4818  reuxfr  4820  issoi  4990  nfiota  5772  nfriota  6520  nfov  6575  mpt2eq123i  6616  mpt2eq3ia  6618  iseri  7656  eqerOLD  7665  0erOLD  7668  ecopoverOLD  7739  nfixp  7813  en2i  7879  en3i  7880  enerOLD  7889  ensymb  7890  entr  7894  r0weon  8718  recmulnq  9665  axcnex  9847  nfneg  10156  negiso  10880  suprzcl2  11654  supxr  12015  xrinf0  12039  cnrecnv  13753  cau3  13943  cbvsum  14273  sum0  14299  ackbijnn  14399  flo1  14425  trireciplem  14433  trirecip  14434  ege2le3  14659  rpnnen2lem3  14784  bitsf1ocnv  15004  prmreclem6  15463  prmrec  15464  modxai  15610  strfvn  15712  strss  15738  xpssca  16061  xpsvsca  16062  mreacs  16142  2oppccomf  16208  mndprop  17140  grpprop  17261  isgrpi  17268  gicerOLD  17542  oppgmndb  17608  oppggrpb  17611  efgrelexlemb  17986  ablprop  18027  ringprop  18407  opprringb  18455  rlmbas  19016  rlmplusg  19017  rlm0  19018  rlmsub  19019  rlmmulr  19020  rlmsca2  19022  rlmvsca  19023  rlmtopn  19024  rlmds  19025  rlmvneg  19028  psrbagsn  19316  evlsval  19340  psr1bas2  19381  psr1bas  19382  psr1plusg  19413  psr1vsca  19414  psr1mulr  19415  ply1plusgfvi  19433  ply1mpl0  19446  ply1mpl1  19448  cncrng  19586  xrsmcmn  19588  cndrng  19594  cnsrng  19599  xrs1mnd  19603  xrs10  19604  absabv  19622  zringcyg  19658  recrng  19786  ordtrestixx  20836  llyidm  21101  nllyidm  21102  toplly  21103  hauslly  21105  hausnlly  21106  lly1stc  21109  kgenf  21154  hmpher  21397  txswaphmeolem  21417  fmucndlem  21905  nrgtrg  22304  cnfldnm  22392  xrsxmet  22420  divcn  22479  expcn  22483  elcncf1ii  22507  iirevcn  22537  iihalf1cn  22539  iihalf2cn  22541  iimulcn  22545  icopnfcnv  22549  iccpnfcnv  22551  cnrehmeo  22560  phtpcerOLD  22603  tchsub  22828  tchphl  22834  iscmet3i  22918  cncmet  22927  rrxprds  22985  vitalilem1OLD  23183  vitali  23188  i1f0  23260  itg20  23310  dvid  23487  dveflem  23546  dvef  23547  dvsincos  23548  ply1divalg2  23702  coe0  23816  iaa  23884  sincn  24002  coscn  24003  reefgim  24008  pilem3  24011  resinf1o  24086  circgrp  24102  circsubm  24103  divlogrlim  24181  dvrelog  24183  logcn  24193  dvlog  24197  advlog  24200  cxpcn  24286  cxpcn2  24287  resqrtcn  24290  sqrtcn  24291  atansopn  24459  dvatan  24462  leibpilem2  24468  leibpi  24469  leibpisum  24470  log2cnv  24471  log2ublem2  24474  log2ub  24476  divsqrtsumlem  24506  emcllem4  24525  emcllem6  24527  emcllem7  24528  lgamf  24568  lgam1  24590  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  vmaf  24645  logfacrlim  24749  lgsdir2lem5  24854  chebbnd1  24961  chtppilim  24964  chto1ub  24965  chebbnd2  24966  chto1lb  24967  chpchtlim  24968  chpo1ub  24969  chpo1ubb  24970  vmadivsum  24971  vmadivsumb  24972  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  logdivsum  25022  vmalogdivsum2  25027  vmalogdivsum  25028  selberglem1  25034  selberglem2  25035  selbergb  25038  selberg2lem  25039  selberg2  25040  selberg2b  25041  selberg3lem2  25047  selberg3  25048  selberg4  25050  pntrmax  25053  pntrsumo1  25054  pntrsumbnd  25055  selbergr  25057  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntrlog2bndlem1  25066  pntrlog2bndlem4  25069  pnt2  25102  pnt  25103  istrkg2ld  25159  legval  25279  ttgsub  25559  cchhllem  25567  vdegp1ai  26511  vdegp1bi  26512  ipasslem7  27075  normlem6  27356  opsqrlem4  28386  eqri  28735  aciunf1  28845  fpwrelmap  28896  fpwrelmapffs  28897  xrs0  29006  mdetlap1  29220  circtopn  29232  cnre2csqima  29285  cnvordtrestixx  29287  mndpluscn  29300  xrge0iifcnv  29307  zlm0  29334  zlm1  29335  qqhre  29392  rrhre  29393  esumnul  29437  hasheuni  29474  sxbrsigalem2  29675  oddpwdc  29743  eulerpartlemb  29757  eulerpartgbij  29761  eulerpartlemn  29770  fib0  29788  fib1  29789  ballotlemrinv  29922  sgn3da  29930  signsw0g  29959  subfacval2  30423  sinccvglem  30820  circum  30822  logi  30873  faclim  30885  faclim2  30887  cnndvlem1  31698  bj-spimev  31907  bj-dvelimv  32029  bj-inrab2  32116  bj-rabtrAUTO  32121  bj-sspwpwab  32239  sucneqoni  32390  wl-cbvalnae  32499  wl-equsal  32505  poimirlem30  32609  dvtan  32630  dvasin  32666  dvacos  32667  dvreasin  32668  dvreacos  32669  efald2  33047  areaquad  36821  clsk1indlem4  37362  clsk1indlem1  37363  lhe4.4ex1a  37550  sbtT  37804  eel0TT  37950  eelTTT  37952  eelT1  37954  eelTT  38019  eelT  38021  eelT0  38023  isosctrlem1ALT  38192  disjsnxp  38265  rabbia2  38309  infxr  38524  dvsinax  38801  itgsin0pilem1  38841  iblempty  38857  stowei  38957  wallispilem5  38962  wallispi  38963  stirlinglem1  38967  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlingr  38983  dirkertrigeqlem1  38991  fourierdlem62  39061  fourierdlem73  39072  fourierdlem76  39075  fourierdlem77  39076  fourierdlem103  39102  fourierdlem104  39103  fourierclim  39117  fourier  39118  fouriersw  39124  etransclem41  39168  etransclem46  39173  salexct2  39233  salexct3  39236  salgencntex  39237  salgensscntex  39238  dmvolsal  39240  bor1sal  39249  iocborel  39250  sge00  39269  sge0sn  39272  ovolval5lem3  39544  ioosshoi  39560  vonioolem2  39572  smfmullem4  39679  konigsbergiedgw  41416  onsetrec  42250  joinlmuladdmuli  42328
  Copyright terms: Public domain W3C validator