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

Theorem trud 1314
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 1312 . 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 1307
This theorem is referenced by:  hadbi123i  1374  cadbi123i  1375  nfn  1777  nfnf  1780  nfim  1781  sbie  1991  eubii  2165  nfeu  2172  nfmo  2173  mobii  2192  dvelimc  2453  ralbii  2580  rexbii  2581  nfral  2609  nfreu  2727  nfrmo  2728  nfrab  2734  nfsbc1  3022  nfsbc  3025  sbcbii  3059  csbeq2i  3120  nfcsb1  3125  nfcsb  3128  nfif  3602  nfdisj  4021  ssbri  4081  nfbr  4083  mpteq12i  4120  issoi  4361  ralxfr  4568  reuxfr2  4574  reuxfr  4576  nfiota  5239  nfov  5897  mpt2eq123i  5927  mpt2eq3ia  5929  nfriota  6330  eqer  6709  0er  6711  ecopover  6778  nfixp  6851  en2i  6915  en3i  6916  ener  6924  ensymb  6925  entr  6929  r0weon  7656  recmulnq  8604  axcnex  8785  nfneg  9064  negiso  9746  suprzcl2  10324  supxr  10647  xrinfm0  10671  cnrecnv  11666  cau3  11855  cbvsum  12184  sum0  12210  ackbijnn  12302  flo1  12329  trireciplem  12336  trirecip  12337  ege2le3  12387  rpnnen2lem3  12511  bitsf1ocnv  12651  prmreclem6  12984  prmrec  12985  modxai  13099  strfvn  13181  strss  13199  xpssca  13496  xpsvsca  13497  mreacs  13576  2oppccomf  13644  mndprop  14416  grpprop  14517  isgrpi  14524  gicer  14756  oppgmndb  14844  oppggrpb  14847  efgrelexlemb  15075  ablprop  15116  rngprop  15390  opprrngb  15430  rlmbas  15964  rlmplusg  15965  rlm0  15966  rlmmulr  15967  rlmsca2  15969  rlmvsca  15970  rlmtopn  15971  rlmds  15972  rlmvneg  15975  psrbagsn  16252  psr1bas2  16285  psr1bas  16286  psr1plusg  16316  psr1vsca  16317  psr1mulr  16318  ply1plusgfvi  16336  ply1mpl0  16349  ply1mpl1  16350  cncrng  16411  xrsmcmn  16413  cndrng  16419  cnsrng  16424  xrs1mnd  16425  xrs10  16426  absabv  16445  zcyg  16461  ordtrestixx  16968  llyidm  17230  nllyidm  17231  toplly  17232  hauslly  17234  hausnlly  17235  lly1stc  17238  kgenf  17252  hmpher  17491  txswaphmeolem  17511  nrgtrg  18216  cnfldnm  18304  xrsxmet  18331  divcn  18388  expcn  18392  elcncf1ii  18416  iirevcn  18444  iihalf1cn  18446  iihalf2cn  18448  iimulcn  18452  icopnfcnv  18456  iccpnfcnv  18458  cnrehmeo  18467  phtpcer  18509  tchphl  18674  iscmet3i  18753  cncmet  18760  vitalilem1  18979  vitali  18984  i1f0  19058  itg20  19108  dvid  19283  dveflem  19342  dvef  19343  dvsincos  19344  evlsval  19419  ply1divalg2  19540  coe0  19653  iaa  19721  sincn  19836  coscn  19837  reefgim  19842  pilem3  19845  resinf1o  19914  divlogrlim  19998  dvrelog  20000  logcn  20010  dvlog  20014  advlog  20017  cxpcn  20101  cxpcn2  20102  resqrcn  20105  sqrcn  20106  atansopn  20244  dvatan  20247  leibpilem2  20253  leibpi  20254  leibpisum  20255  log2cnv  20256  log2ublem2  20259  log2ub  20261  divsqrsumlem  20290  emcllem4  20308  emcllem6  20310  emcllem7  20311  basellem6  20339  basellem7  20340  basellem8  20341  basellem9  20342  vmaf  20373  logfacrlim  20479  lgsdir2lem5  20582  chebbnd1  20637  chtppilim  20640  chto1ub  20641  chebbnd2  20642  chto1lb  20643  chpchtlim  20644  chpo1ub  20645  chpo1ubb  20646  vmadivsum  20647  vmadivsumb  20648  mudivsum  20695  mulogsumlem  20696  mulogsum  20697  logdivsum  20698  vmalogdivsum2  20703  vmalogdivsum  20704  selberglem1  20710  selberglem2  20711  selbergb  20714  selberg2lem  20715  selberg2  20716  selberg2b  20717  selberg3lem2  20723  selberg3  20724  selberg4  20726  pntrmax  20729  pntrsumo1  20730  pntrsumbnd  20731  selbergr  20733  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem1  20742  pntrlog2bndlem4  20745  pnt2  20778  pnt  20779  isgrp2i  20919  circgrp  21057  rngosn  21087  ipasslem7  21430  normlem6  21710  opsqrlem4  22739  ballotlemrinv  23108  eqri  23203  cnre2csqima  23310  cnvordtrestixx  23312  mndpluscn  23314  xrs0  23320  xrge0iifcnv  23330  esumnul  23442  hasheuni  23468  subfacval2  23733  vdegp1ai  23923  vdegp1bi  23924  sinccvglem  24020  circum  24022  faclimlem3  24119  cprod0  24168  dvreasin  25026  dvreacos  25027  trant  25052  unttr  25120  prodeq123i  25420  isibcg  26294  lhe4.4ex1a  27649  itgsin0pilem1  27847  stowei  27916  wallispilem5  27921  wallispi  27922  stirlinglem1  27926  stirlinglem12  27937  stirlinglem13  27938  stirlinglem14  27939  stirlingr  27942  astbstanbst  27980  sbtT  28635  eel0TT  28784  eelTTT  28786  eelT1  28791  eelTT  28860  eelT  28862  eelT0  28864  sbieNEW7  29516  nfnfOLD7  29643
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 177  df-tru 1310
  Copyright terms: Public domain W3C validator