Theorem trud 1388

Description: Eliminate T. as an antecedent. A proposition implied by T. is true. (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 1383	. 2 |- T.
2		trud.1	. 2 |- ( T. -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   -> wi 4   T. wtru 1380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-tru 1382

This theorem is referenced by:  hadbi123i  1435  cadbi123i  1436  nfbi  1881  spime  1977  nfeu  2294  nfmo  2295  eubii  2300  mobii  2301  abeq2i  2594  nfceqi  2625  nfeq  2640  nfel  2642  dvelimc  2653  nfral  2850  nfrex  2927  rexbiiOLD  2975  ralbiiOLD  2976  nfreu  3036  nfrmo  3037  nfrab  3043  nfsbc1  3350  nfsbc  3353  sbcbii  3391  nfcsb1  3450  nfcsb  3453  csbeq2i  3836  nfif  3968  nfdisj  4429  ssbri  4489  nfbr  4491  mpteq12i  4531  ralxfr  4665  reuxfr2  4671  reuxfr  4673  issoi  4831  nfiota  5555  nfriota  6254  nfov  6307  mpt2eq123i  6344  mpt2eq3ia  6346  eqer  7344  0er  7346  ecopover  7415  nfixp  7488  en2i  7553  en3i  7554  ener  7562  ensymb  7563  entr  7567  r0weon  8390  recmulnq  9342  axcnex  9524  nfneg  9816  negiso  10519  suprzcl2  11172  supxr  11504  xrinfm0  11528  cnrecnv  12961  cau3  13151  cbvsum  13480  sum0  13506  ackbijnn  13603  flo1  13629  trireciplem  13636  trirecip  13637  ege2le3  13687  rpnnen2lem3  13811  bitsf1ocnv  13953  prmreclem6  14298  prmrec  14299  modxai  14413  strfvn  14507  strss  14527  xpssca  14833  xpsvsca  14834  mreacs  14913  2oppccomf  14981  mndprop  15766  grpprop  15879  isgrpi  15886  gicer  16129  oppgmndb  16195  oppggrpb  16198  efgrelexlemb  16574  ablprop  16615  rngprop  17033  opprrngb  17082  rlmbas  17641  rlmplusg  17642  rlm0  17643  rlmsub  17644  rlmmulr  17645  rlmsca2  17647  rlmvsca  17648  rlmtopn  17649  rlmds  17650  rlmvneg  17653  psrbagsn  17959  evlsval  17987  psr1bas2  18028  psr1bas  18029  psr1plusg  18062  psr1vsca  18063  psr1mulr  18064  ply1plusgfvi  18082  ply1mpl0  18095  ply1mpl1  18097  cncrng  18238  xrsmcmn  18240  cndrng  18246  cnsrng  18251  xrs1mnd  18252  xrs10  18253  absabv  18271  zringcyg  18308  zcyg  18313  recrng  18452  ordtrestixx  19517  llyidm  19783  nllyidm  19784  toplly  19785  hauslly  19787  hausnlly  19788  lly1stc  19791  kgenf  19805  hmpher  20048  txswaphmeolem  20068  fmucndlem  20557  nrgtrg  20961  cnfldnm  21049  xrsxmet  21077  divcn  21135  expcn  21139  elcncf1ii  21163  iirevcn  21193  iihalf1cn  21195  iihalf2cn  21197  iimulcn  21201  icopnfcnv  21205  iccpnfcnv  21207  cnrehmeo  21216  phtpcer  21258  tchsub  21427  tchphl  21433  iscmet3i  21513  cncmet  21524  rrxprds  21584  vitalilem1  21780  vitali  21785  i1f0  21857  itg20  21907  dvid  22084  dveflem  22143  dvef  22144  dvsincos  22145  ply1divalg2  22302  coe0  22415  iaa  22483  sincn  22601  coscn  22602  reefgim  22607  pilem3  22610  resinf1o  22684  divlogrlim  22772  dvrelog  22774  logcn  22784  dvlog  22788  advlog  22791  cxpcn  22875  cxpcn2  22876  resqrtcn  22879  sqrtcn  22880  atansopn  23019  dvatan  23022  leibpilem2  23028  leibpi  23029  leibpisum  23030  log2cnv  23031  log2ublem2  23034  log2ub  23036  divsqrtsumlem  23065  emcllem4  23084  emcllem6  23086  emcllem7  23087  basellem6  23115  basellem7  23116  basellem8  23117  basellem9  23118  vmaf  23149  logfacrlim  23255  lgsdir2lem5  23358  chebbnd1  23413  chtppilim  23416  chto1ub  23417  chebbnd2  23418  chto1lb  23419  chpchtlim  23420  chpo1ub  23421  chpo1ubb  23422  vmadivsum  23423  vmadivsumb  23424  mudivsum  23471  mulogsumlem  23472  mulogsum  23473  logdivsum  23474  vmalogdivsum2  23479  vmalogdivsum  23480  selberglem1  23486  selberglem2  23487  selbergb  23490  selberg2lem  23491  selberg2  23492  selberg2b  23493  selberg3lem2  23499  selberg3  23500  selberg4  23502  pntrmax  23505  pntrsumo1  23506  pntrsumbnd  23507  selbergr  23509  selberg3r  23510  selberg4r  23511  selberg34r  23512  pntrlog2bndlem1  23518  pntrlog2bndlem4  23521  pnt2  23554  pnt  23555  istrkg2ld  23614  legval  23726  ttgsub  23886  cchhllem  23894  erclwwlkn  24532  vdegp1ai  24688  vdegp1bi  24689  isgrp2i  24942  circgrp  25080  rngosn  25110  ipasslem7  25455  normlem6  25736  opsqrlem4  26766  eqri  27113  fpwrelmap  27256  fpwrelmapffs  27257  xrs0  27353  cnre2csqima  27557  cnvordtrestixx  27559  mndpluscn  27572  xrge0iifcnv  27579  zlm0  27607  zlm1  27608  qqhre  27662  rrhre  27663  circtopn  27666  esumnul  27727  hasheuni  27759  sxbrsigalem2  27925  oddpwdc  27961  eulerpartlemb  27975  eulerpartgbij  27979  eulerpartlemn  27988  fib0  28006  fib1  28007  ballotlemrinv  28140  sgn3da  28148  signsw0g  28181  lgamf  28252  lgam1  28274  subfacval2  28299  sinccvglem  28541  circum  28543  faclim  28776  faclim2  28778  wl-cbvalnae  29591  wl-equsal  29598  dvtanlem  29669  dvtan  29670  dvasin  29708  dvacos  29709  dvreasin  29710  dvreacos  29711  efald2  30106  areaquad  30817  lhe4.4ex1a  30862  dvsinax  31269  itgsin0pilem1  31295  iblempty  31311  stowei  31392  wallispilem5  31397  wallispi  31398  stirlinglem1  31402  stirlinglem12  31413  stirlinglem13  31414  stirlinglem14  31415  stirlingr  31418  dirkertrigeqlem1  31426  fourierdlem62  31497  fourierdlem73  31508  fourierdlem76  31511  fourierdlem77  31512  fourierdlem103  31538  fourierdlem104  31539  fourierclim  31553  fourier  31554  fouriersw  31560  joinlmuladdmuli  32287  sbtT  32441  eel0TT  32590  eelTTT  32592  eelT1  32597  eelTT  32666  eelT  32668  eelT0  32670  isosctrlem1ALT  32832  bj-spimev  33381  bj-inrab2  33595  bj-rabtrAUTO  33598