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

Theorem trud 1332
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 1330 . 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 1325
This theorem is referenced by:  hadbi123i  1393  cadbi123i  1394  nfn  1811  nfimOLD  1833  nfbi  1856  nfnfOLD  1868  spime  1962  sbieOLD  2152  eubii  2290  nfeu  2297  nfmo  2298  mobii  2317  dvelimc  2593  ralbii  2729  rexbii  2730  nfral  2759  nfreu  2882  nfrmo  2883  nfrab  2889  nfsbc1  3179  nfsbc  3182  sbcbii  3216  csbeq2i  3277  nfcsb1  3282  nfcsb  3285  nfif  3763  nfdisj  4194  ssbri  4254  nfbr  4256  mpteq12i  4293  issoi  4534  ralxfr  4741  reuxfr2  4747  reuxfr  4749  nfiota  5422  nfov  6104  mpt2eq123i  6137  mpt2eq3ia  6139  nfriota  6559  eqer  6938  0er  6940  ecopover  7008  nfixp  7081  en2i  7145  en3i  7146  ener  7154  ensymb  7155  entr  7159  r0weon  7894  recmulnq  8841  axcnex  9022  nfneg  9302  negiso  9984  suprzcl2  10566  supxr  10891  xrinfm0  10915  cnrecnv  11970  cau3  12159  cbvsum  12489  sum0  12515  ackbijnn  12607  flo1  12634  trireciplem  12641  trirecip  12642  ege2le3  12692  rpnnen2lem3  12816  bitsf1ocnv  12956  prmreclem6  13289  prmrec  13290  modxai  13404  strfvn  13486  strss  13504  xpssca  13803  xpsvsca  13804  mreacs  13883  2oppccomf  13951  mndprop  14723  grpprop  14824  isgrpi  14831  gicer  15063  oppgmndb  15151  oppggrpb  15154  efgrelexlemb  15382  ablprop  15423  rngprop  15697  opprrngb  15737  rlmbas  16267  rlmplusg  16268  rlm0  16269  rlmmulr  16270  rlmsca2  16272  rlmvsca  16273  rlmtopn  16274  rlmds  16275  rlmvneg  16278  psrbagsn  16555  psr1bas2  16588  psr1bas  16589  psr1plusg  16616  psr1vsca  16617  psr1mulr  16618  ply1plusgfvi  16636  ply1mpl0  16649  ply1mpl1  16650  cncrng  16722  xrsmcmn  16724  cndrng  16730  cnsrng  16735  xrs1mnd  16736  xrs10  16737  absabv  16756  zcyg  16772  ordtrestixx  17286  llyidm  17551  nllyidm  17552  toplly  17553  hauslly  17555  hausnlly  17556  lly1stc  17559  kgenf  17573  hmpher  17816  txswaphmeolem  17836  fmucndlem  18321  nrgtrg  18725  cnfldnm  18813  xrsxmet  18840  divcn  18898  expcn  18902  elcncf1ii  18926  iirevcn  18955  iihalf1cn  18957  iihalf2cn  18959  iimulcn  18963  icopnfcnv  18967  iccpnfcnv  18969  cnrehmeo  18978  phtpcer  19020  tchphl  19185  iscmet3i  19264  cncmet  19275  vitalilem1  19500  vitali  19505  i1f0  19579  itg20  19629  dvid  19804  dveflem  19863  dvef  19864  dvsincos  19865  evlsval  19940  ply1divalg2  20061  coe0  20174  iaa  20242  sincn  20360  coscn  20361  reefgim  20366  pilem3  20369  resinf1o  20438  divlogrlim  20526  dvrelog  20528  logcn  20538  dvlog  20542  advlog  20545  cxpcn  20629  cxpcn2  20630  resqrcn  20633  sqrcn  20634  atansopn  20772  dvatan  20775  leibpilem2  20781  leibpi  20782  leibpisum  20783  log2cnv  20784  log2ublem2  20787  log2ub  20789  divsqrsumlem  20818  emcllem4  20837  emcllem6  20839  emcllem7  20840  basellem6  20868  basellem7  20869  basellem8  20870  basellem9  20871  vmaf  20902  logfacrlim  21008  lgsdir2lem5  21111  chebbnd1  21166  chtppilim  21169  chto1ub  21170  chebbnd2  21171  chto1lb  21172  chpchtlim  21173  chpo1ub  21174  chpo1ubb  21175  vmadivsum  21176  vmadivsumb  21177  mudivsum  21224  mulogsumlem  21225  mulogsum  21226  logdivsum  21227  vmalogdivsum2  21232  vmalogdivsum  21233  selberglem1  21239  selberglem2  21240  selbergb  21243  selberg2lem  21244  selberg2  21245  selberg2b  21246  selberg3lem2  21252  selberg3  21253  selberg4  21255  pntrmax  21258  pntrsumo1  21259  pntrsumbnd  21260  selbergr  21262  selberg3r  21263  selberg4r  21264  selberg34r  21265  pntrlog2bndlem1  21271  pntrlog2bndlem4  21274  pnt2  21307  pnt  21308  vdegp1ai  21706  vdegp1bi  21707  isgrp2i  21824  circgrp  21962  rngosn  21992  ipasslem7  22337  normlem6  22617  opsqrlem4  23646  eqri  23994  xrs0  24197  cnre2csqima  24309  cnvordtrestixx  24311  mndpluscn  24312  xrge0iifcnv  24319  zlm0  24346  zlm1  24347  qqhre  24386  rrhre  24387  esumnul  24443  hasheuni  24475  sxbrsigalem2  24636  ballotlemrinv  24791  lgamf  24826  lgam1  24848  subfacval2  24873  sinccvglem  25109  circum  25111  faclim  25365  faclim2  25367  dvreasin  26290  dvreacos  26291  lhe4.4ex1a  27523  itgsin0pilem1  27720  stowei  27789  wallispilem5  27794  wallispi  27795  stirlinglem1  27799  stirlinglem12  27810  stirlinglem13  27811  stirlinglem14  27812  stirlingr  27815  sbtT  28657  eel0TT  28807  eelTTT  28809  eelT1  28814  eelTT  28883  eelT  28885  eelT0  28887  isosctrlem1ALT  29046  sbieNEW7  29541  nfnfOLD7  29689
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 178  df-tru 1328
  Copyright terms: Public domain W3C validator