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

Theorem trud 1333
Description: Eliminate  T. as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypothesis
Ref Expression
trud.1  |-  (  T. 
->  ph )
Assertion
Ref Expression
trud  |-  ph

Proof of Theorem trud
StepHypRef Expression
1 tru 1331 . 2  |-  T.
2 trud.1 . 2  |-  (  T. 
->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    T. wtru 1326
This theorem is referenced by:  hadbi123i  1394  cadbi123i  1395  nfn  1812  nfimOLD  1834  nfbi  1857  nfnfOLD  1869  spime  1963  sbieOLD  2154  eubii  2292  nfeu  2299  nfmo  2300  mobii  2319  dvelimc  2595  ralbii  2731  rexbii  2732  nfral  2761  nfreu  2884  nfrmo  2885  nfrab  2891  nfsbc1  3181  nfsbc  3184  sbcbii  3218  csbeq2i  3279  nfcsb1  3284  nfcsb  3287  nfif  3765  nfdisj  4196  ssbri  4256  nfbr  4258  mpteq12i  4295  issoi  4536  ralxfr  4743  reuxfr2  4749  reuxfr  4751  nfiota  5424  nfov  6106  mpt2eq123i  6139  mpt2eq3ia  6141  nfriota  6561  eqer  6940  0er  6942  ecopover  7010  nfixp  7083  en2i  7147  en3i  7148  ener  7156  ensymb  7157  entr  7161  r0weon  7896  recmulnq  8843  axcnex  9024  nfneg  9304  negiso  9986  suprzcl2  10568  supxr  10893  xrinfm0  10917  cnrecnv  11972  cau3  12161  cbvsum  12491  sum0  12517  ackbijnn  12609  flo1  12636  trireciplem  12643  trirecip  12644  ege2le3  12694  rpnnen2lem3  12818  bitsf1ocnv  12958  prmreclem6  13291  prmrec  13292  modxai  13406  strfvn  13488  strss  13506  xpssca  13805  xpsvsca  13806  mreacs  13885  2oppccomf  13953  mndprop  14725  grpprop  14826  isgrpi  14833  gicer  15065  oppgmndb  15153  oppggrpb  15156  efgrelexlemb  15384  ablprop  15425  rngprop  15699  opprrngb  15739  rlmbas  16269  rlmplusg  16270  rlm0  16271  rlmmulr  16272  rlmsca2  16274  rlmvsca  16275  rlmtopn  16276  rlmds  16277  rlmvneg  16280  psrbagsn  16557  psr1bas2  16590  psr1bas  16591  psr1plusg  16618  psr1vsca  16619  psr1mulr  16620  ply1plusgfvi  16638  ply1mpl0  16651  ply1mpl1  16652  cncrng  16724  xrsmcmn  16726  cndrng  16732  cnsrng  16737  xrs1mnd  16738  xrs10  16739  absabv  16758  zcyg  16774  ordtrestixx  17288  llyidm  17553  nllyidm  17554  toplly  17555  hauslly  17557  hausnlly  17558  lly1stc  17561  kgenf  17575  hmpher  17818  txswaphmeolem  17838  fmucndlem  18323  nrgtrg  18727  cnfldnm  18815  xrsxmet  18842  divcn  18900  expcn  18904  elcncf1ii  18928  iirevcn  18957  iihalf1cn  18959  iihalf2cn  18961  iimulcn  18965  icopnfcnv  18969  iccpnfcnv  18971  cnrehmeo  18980  phtpcer  19022  tchphl  19187  iscmet3i  19266  cncmet  19277  vitalilem1  19502  vitali  19507  i1f0  19581  itg20  19631  dvid  19806  dveflem  19865  dvef  19866  dvsincos  19867  evlsval  19942  ply1divalg2  20063  coe0  20176  iaa  20244  sincn  20362  coscn  20363  reefgim  20368  pilem3  20371  resinf1o  20440  divlogrlim  20528  dvrelog  20530  logcn  20540  dvlog  20544  advlog  20547  cxpcn  20631  cxpcn2  20632  resqrcn  20635  sqrcn  20636  atansopn  20774  dvatan  20777  leibpilem2  20783  leibpi  20784  leibpisum  20785  log2cnv  20786  log2ublem2  20789  log2ub  20791  divsqrsumlem  20820  emcllem4  20839  emcllem6  20841  emcllem7  20842  basellem6  20870  basellem7  20871  basellem8  20872  basellem9  20873  vmaf  20904  logfacrlim  21010  lgsdir2lem5  21113  chebbnd1  21168  chtppilim  21171  chto1ub  21172  chebbnd2  21173  chto1lb  21174  chpchtlim  21175  chpo1ub  21176  chpo1ubb  21177  vmadivsum  21178  vmadivsumb  21179  mudivsum  21226  mulogsumlem  21227  mulogsum  21228  logdivsum  21229  vmalogdivsum2  21234  vmalogdivsum  21235  selberglem1  21241  selberglem2  21242  selbergb  21245  selberg2lem  21246  selberg2  21247  selberg2b  21248  selberg3lem2  21254  selberg3  21255  selberg4  21257  pntrmax  21260  pntrsumo1  21261  pntrsumbnd  21262  selbergr  21264  selberg3r  21265  selberg4r  21266  selberg34r  21267  pntrlog2bndlem1  21273  pntrlog2bndlem4  21276  pnt2  21309  pnt  21310  vdegp1ai  21708  vdegp1bi  21709  isgrp2i  21826  circgrp  21964  rngosn  21994  ipasslem7  22339  normlem6  22619  opsqrlem4  23648  eqri  23996  xrs0  24199  cnre2csqima  24311  cnvordtrestixx  24313  mndpluscn  24314  xrge0iifcnv  24321  zlm0  24348  zlm1  24349  qqhre  24388  rrhre  24389  esumnul  24445  hasheuni  24477  sxbrsigalem2  24638  ballotlemrinv  24793  lgamf  24828  lgam1  24850  subfacval2  24875  sinccvglem  25111  circum  25113  faclim  25367  faclim2  25369  dvreasin  26292  dvreacos  26293  lhe4.4ex1a  27525  itgsin0pilem1  27722  stowei  27791  wallispilem5  27796  wallispi  27797  stirlinglem1  27801  stirlinglem12  27812  stirlinglem13  27813  stirlinglem14  27814  stirlingr  27817  sbtT  28719  eel0TT  28869  eelTTT  28871  eelT1  28876  eelTT  28945  eelT  28947  eelT0  28949  isosctrlem1ALT  29108  sbieNEW7  29603  nfnfOLD7  29751
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-tru 1329
  Copyright terms: Public domain W3C validator