Theorem trud 1329

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

Step	Hyp	Ref	Expression
1		tru 1327	. 2 |- T.
2		trud.1	. 2 |- ( T. -> ph )
3	1, 2	ax-mp 8	1 |- ph

Syntax hints:   -> wi 4   T. wtru 1322

This theorem is referenced by:  hadbi123i  1390  cadbi123i  1391  nfn  1807  nfimOLD  1829  nfbi  1852  nfnfOLD  1864  spime  1960  sbie  2087  eubii  2263  nfeu  2270  nfmo  2271  mobii  2290  dvelimc  2561  ralbii  2690  rexbii  2691  nfral  2719  nfreu  2842  nfrmo  2843  nfrab  2849  nfsbc1  3139  nfsbc  3142  sbcbii  3176  csbeq2i  3237  nfcsb1  3242  nfcsb  3245  nfif  3723  nfdisj  4154  ssbri  4214  nfbr  4216  mpteq12i  4253  issoi  4494  ralxfr  4700  reuxfr2  4706  reuxfr  4708  nfiota  5381  nfov  6063  mpt2eq123i  6096  mpt2eq3ia  6098  nfriota  6518  eqer  6897  0er  6899  ecopover  6967  nfixp  7040  en2i  7104  en3i  7105  ener  7113  ensymb  7114  entr  7118  r0weon  7850  recmulnq  8797  axcnex  8978  nfneg  9258  negiso  9940  suprzcl2  10522  supxr  10847  xrinfm0  10871  cnrecnv  11925  cau3  12114  cbvsum  12444  sum0  12470  ackbijnn  12562  flo1  12589  trireciplem  12596  trirecip  12597  ege2le3  12647  rpnnen2lem3  12771  bitsf1ocnv  12911  prmreclem6  13244  prmrec  13245  modxai  13359  strfvn  13441  strss  13459  xpssca  13758  xpsvsca  13759  mreacs  13838  2oppccomf  13906  mndprop  14678  grpprop  14779  isgrpi  14786  gicer  15018  oppgmndb  15106  oppggrpb  15109  efgrelexlemb  15337  ablprop  15378  rngprop  15652  opprrngb  15692  rlmbas  16222  rlmplusg  16223  rlm0  16224  rlmmulr  16225  rlmsca2  16227  rlmvsca  16228  rlmtopn  16229  rlmds  16230  rlmvneg  16233  psrbagsn  16510  psr1bas2  16543  psr1bas  16544  psr1plusg  16571  psr1vsca  16572  psr1mulr  16573  ply1plusgfvi  16591  ply1mpl0  16604  ply1mpl1  16605  cncrng  16677  xrsmcmn  16679  cndrng  16685  cnsrng  16690  xrs1mnd  16691  xrs10  16692  absabv  16711  zcyg  16727  ordtrestixx  17240  llyidm  17504  nllyidm  17505  toplly  17506  hauslly  17508  hausnlly  17509  lly1stc  17512  kgenf  17526  hmpher  17769  txswaphmeolem  17789  fmucndlem  18274  nrgtrg  18678  cnfldnm  18766  xrsxmet  18793  divcn  18851  expcn  18855  elcncf1ii  18879  iirevcn  18908  iihalf1cn  18910  iihalf2cn  18912  iimulcn  18916  icopnfcnv  18920  iccpnfcnv  18922  cnrehmeo  18931  phtpcer  18973  tchphl  19138  iscmet3i  19217  cncmet  19228  vitalilem1  19453  vitali  19458  i1f0  19532  itg20  19582  dvid  19757  dveflem  19816  dvef  19817  dvsincos  19818  evlsval  19893  ply1divalg2  20014  coe0  20127  iaa  20195  sincn  20313  coscn  20314  reefgim  20319  pilem3  20322  resinf1o  20391  divlogrlim  20479  dvrelog  20481  logcn  20491  dvlog  20495  advlog  20498  cxpcn  20582  cxpcn2  20583  resqrcn  20586  sqrcn  20587  atansopn  20725  dvatan  20728  leibpilem2  20734  leibpi  20735  leibpisum  20736  log2cnv  20737  log2ublem2  20740  log2ub  20742  divsqrsumlem  20771  emcllem4  20790  emcllem6  20792  emcllem7  20793  basellem6  20821  basellem7  20822  basellem8  20823  basellem9  20824  vmaf  20855  logfacrlim  20961  lgsdir2lem5  21064  chebbnd1  21119  chtppilim  21122  chto1ub  21123  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  chpo1ub  21127  chpo1ubb  21128  vmadivsum  21129  vmadivsumb  21130  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  logdivsum  21180  vmalogdivsum2  21185  vmalogdivsum  21186  selberglem1  21192  selberglem2  21193  selbergb  21196  selberg2lem  21197  selberg2  21198  selberg2b  21199  selberg3lem2  21205  selberg3  21206  selberg4  21208  pntrmax  21211  pntrsumo1  21212  pntrsumbnd  21213  selbergr  21215  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem1  21224  pntrlog2bndlem4  21227  pnt2  21260  pnt  21261  vdegp1ai  21659  vdegp1bi  21660  isgrp2i  21777  circgrp  21915  rngosn  21945  ipasslem7  22290  normlem6  22570  opsqrlem4  23599  eqri  23947  xrs0  24150  cnre2csqima  24262  cnvordtrestixx  24264  mndpluscn  24265  xrge0iifcnv  24272  zlm0  24299  zlm1  24300  qqhre  24339  rrhre  24340  esumnul  24396  hasheuni  24428  sxbrsigalem2  24589  ballotlemrinv  24744  lgamf  24779  lgam1  24801  subfacval2  24826  sinccvglem  25062  circum  25064  prod0  25222  faclim  25313  faclim2  25315  dvreasin  26179  dvreacos  26180  lhe4.4ex1a  27414  itgsin0pilem1  27611  stowei  27680  wallispilem5  27685  wallispi  27686  stirlinglem1  27690  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlingr  27706  sbtT  28368  eel0TT  28516  eelTTT  28518  eelT1  28523  eelTT  28592  eelT  28594  eelT0  28596  sbieNEW7  29245  nfnfOLD7  29373

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 1325