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  1765  nfnf  1768  nfim  1769  sbie  1978  eubii  2152  nfeu  2159  nfmo  2160  mobii  2179  dvelimc  2440  ralbii  2567  rexbii  2568  nfral  2596  nfreu  2714  nfrmo  2715  nfrab  2721  nfsbc1  3009  nfsbc  3012  sbcbii  3046  csbeq2i  3107  nfcsb1  3112  nfcsb  3115  nfif  3589  nfdisj  4005  ssbri  4065  nfbr  4067  mpteq12i  4104  issoi  4345  ralxfr  4552  reuxfr2  4558  reuxfr  4560  nfiota  5223  nfov  5881  mpt2eq123i  5911  mpt2eq3ia  5913  nfriota  6314  eqer  6693  0er  6695  ecopover  6762  nfixp  6835  en2i  6899  en3i  6900  ener  6908  ensymb  6909  entr  6913  r0weon  7640  recmulnq  8588  axcnex  8769  nfneg  9048  negiso  9730  suprzcl2  10308  supxr  10631  xrinfm0  10655  cnrecnv  11650  cau3  11839  cbvsum  12168  sum0  12194  ackbijnn  12286  flo1  12313  trireciplem  12320  trirecip  12321  ege2le3  12371  rpnnen2lem3  12495  bitsf1ocnv  12635  prmreclem6  12968  prmrec  12969  modxai  13083  strfvn  13165  strss  13183  xpssca  13480  xpsvsca  13481  mreacs  13560  2oppccomf  13628  mndprop  14400  grpprop  14501  isgrpi  14508  gicer  14740  oppgmndb  14828  oppggrpb  14831  efgrelexlemb  15059  ablprop  15100  rngprop  15374  opprrngb  15414  rlmbas  15948  rlmplusg  15949  rlm0  15950  rlmmulr  15951  rlmsca2  15953  rlmvsca  15954  rlmtopn  15955  rlmds  15956  rlmvneg  15959  psrbagsn  16236  psr1bas2  16269  psr1bas  16270  psr1plusg  16300  psr1vsca  16301  psr1mulr  16302  ply1plusgfvi  16320  ply1mpl0  16333  ply1mpl1  16334  cncrng  16395  xrsmcmn  16397  cndrng  16403  cnsrng  16408  xrs1mnd  16409  xrs10  16410  absabv  16429  zcyg  16445  ordtrestixx  16952  llyidm  17214  nllyidm  17215  toplly  17216  hauslly  17218  hausnlly  17219  lly1stc  17222  kgenf  17236  hmpher  17475  txswaphmeolem  17495  nrgtrg  18200  cnfldnm  18288  xrsxmet  18315  divcn  18372  expcn  18376  elcncf1ii  18400  iirevcn  18428  iihalf1cn  18430  iihalf2cn  18432  iimulcn  18436  icopnfcnv  18440  iccpnfcnv  18442  cnrehmeo  18451  phtpcer  18493  tchphl  18658  iscmet3i  18737  cncmet  18744  vitalilem1  18963  vitali  18968  i1f0  19042  itg20  19092  dvid  19267  dveflem  19326  dvef  19327  dvsincos  19328  evlsval  19403  ply1divalg2  19524  coe0  19637  iaa  19705  sincn  19820  coscn  19821  reefgim  19826  pilem3  19829  resinf1o  19898  divlogrlim  19982  dvrelog  19984  logcn  19994  dvlog  19998  advlog  20001  cxpcn  20085  cxpcn2  20086  resqrcn  20089  sqrcn  20090  atansopn  20228  dvatan  20231  leibpilem2  20237  leibpi  20238  leibpisum  20239  log2cnv  20240  log2ublem2  20243  log2ub  20245  divsqrsumlem  20274  emcllem4  20292  emcllem6  20294  emcllem7  20295  basellem6  20323  basellem7  20324  basellem8  20325  basellem9  20326  vmaf  20357  logfacrlim  20463  lgsdir2lem5  20566  chebbnd1  20621  chtppilim  20624  chto1ub  20625  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  chpo1ub  20629  chpo1ubb  20630  vmadivsum  20631  vmadivsumb  20632  mudivsum  20679  mulogsumlem  20680  mulogsum  20681  logdivsum  20682  vmalogdivsum2  20687  vmalogdivsum  20688  selberglem1  20694  selberglem2  20695  selbergb  20698  selberg2lem  20699  selberg2  20700  selberg2b  20701  selberg3lem2  20707  selberg3  20708  selberg4  20710  pntrmax  20713  pntrsumo1  20714  pntrsumbnd  20715  selbergr  20717  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntrlog2bndlem1  20726  pntrlog2bndlem4  20729  pnt2  20762  pnt  20763  isgrp2i  20903  circgrp  21041  rngosn  21071  ipasslem7  21414  normlem6  21694  opsqrlem4  22723  ballotlemrinv  23092  eqri  23187  cnre2csqima  23295  cnvordtrestixx  23297  mndpluscn  23299  xrs0  23305  xrge0iifcnv  23315  esumnul  23427  hasheuni  23453  subfacval2  23718  vdegp1ai  23908  vdegp1bi  23909  sinccvglem  24005  circum  24007  dvreasin  24923  dvreacos  24924  trant  24949  unttr  25017  prodeq123i  25317  isibcg  26191  lhe4.4ex1a  27546  itgsin0pilem1  27744  stowei  27813  wallispilem5  27818  wallispi  27819  stirlinglem1  27823  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlingr  27839  astbstanbst  27877  sbtT  28336  eel0TT  28479  eelTTT  28481  eelT1  28485  eelTT  28546  eelT  28548  eelT0  28550
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