Theorem trud 1408

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 1403	. 2 |- T.
2		trud.1	. 2 |- ( T. -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   -> wi 4   T. wtru 1400

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 1402

This theorem is referenced by:  hadbi123i  1458  cadbi123i  1459  nfbi  1942  spime  2015  nfeu  2236  nfmo  2237  eubii  2242  mobii  2243  abeq2i  2509  nfceqi  2540  nfeq  2555  nfel  2557  dvelimc  2568  nfral  2768  nfrex  2845  rexbiiOLD  2895  ralbiiOLD  2896  nfreu  2957  nfrmo  2958  nfrab  2964  nfsbc1  3271  nfsbc  3274  sbcbii  3308  nfcsb1  3363  nfcsb  3366  csbeq2i  3760  nfif  3886  nfdisj  4350  ssbri  4409  nfbr  4411  mpteq12i  4451  ralxfr  4580  reuxfr2  4586  reuxfr  4588  issoi  4745  nfiota  5464  nfriota  6167  nfov  6222  mpt2eq123i  6259  mpt2eq3ia  6261  eqer  7262  0er  7264  ecopover  7333  nfixp  7407  en2i  7472  en3i  7473  ener  7481  ensymb  7482  entr  7486  r0weon  8303  recmulnq  9253  axcnex  9435  nfneg  9729  negiso  10435  suprzcl2  11091  supxr  11425  xrinfm0  11449  cnrecnv  13000  cau3  13190  cbvsum  13519  sum0  13545  ackbijnn  13642  flo1  13668  trireciplem  13675  trirecip  13676  ege2le3  13827  rpnnen2lem3  13952  bitsf1ocnv  14096  prmreclem6  14441  prmrec  14442  modxai  14556  strfvn  14651  strss  14673  xpssca  14985  xpsvsca  14986  mreacs  15065  2oppccomf  15131  mndprop  16064  grpprop  16186  isgrpi  16193  gicer  16441  oppgmndb  16507  oppggrpb  16510  efgrelexlemb  16885  ablprop  16926  ringprop  17345  opprringb  17394  rlmbas  17954  rlmplusg  17955  rlm0  17956  rlmsub  17957  rlmmulr  17958  rlmsca2  17960  rlmvsca  17961  rlmtopn  17962  rlmds  17963  rlmvneg  17966  psrbagsn  18273  evlsval  18301  psr1bas2  18342  psr1bas  18343  psr1plusg  18376  psr1vsca  18377  psr1mulr  18378  ply1plusgfvi  18396  ply1mpl0  18409  ply1mpl1  18411  cncrng  18552  xrsmcmn  18554  cndrng  18560  cnsrng  18565  xrs1mnd  18569  xrs10  18570  absabv  18588  zringcyg  18619  recrng  18748  ordtrestixx  19809  llyidm  20074  nllyidm  20075  toplly  20076  hauslly  20078  hausnlly  20079  lly1stc  20082  kgenf  20127  hmpher  20370  txswaphmeolem  20390  fmucndlem  20879  nrgtrg  21283  cnfldnm  21371  xrsxmet  21399  divcn  21457  expcn  21461  elcncf1ii  21485  iirevcn  21515  iihalf1cn  21517  iihalf2cn  21519  iimulcn  21523  icopnfcnv  21527  iccpnfcnv  21529  cnrehmeo  21538  phtpcer  21580  tchsub  21749  tchphl  21755  iscmet3i  21835  cncmet  21846  rrxprds  21906  vitalilem1  22102  vitali  22107  i1f0  22179  itg20  22229  dvid  22406  dveflem  22465  dvef  22466  dvsincos  22467  ply1divalg2  22624  coe0  22738  iaa  22806  sincn  22924  coscn  22925  reefgim  22930  pilem3  22933  resinf1o  23008  circgrp  23024  circsubm  23025  divlogrlim  23103  dvrelog  23105  logcn  23115  dvlog  23119  advlog  23122  cxpcn  23206  cxpcn2  23207  resqrtcn  23210  sqrtcn  23211  atansopn  23379  dvatan  23382  leibpilem2  23388  leibpi  23389  leibpisum  23390  log2cnv  23391  log2ublem2  23394  log2ub  23396  divsqrtsumlem  23426  emcllem4  23445  emcllem6  23447  emcllem7  23448  basellem6  23476  basellem7  23477  basellem8  23478  basellem9  23479  vmaf  23510  logfacrlim  23616  lgsdir2lem5  23719  chebbnd1  23774  chtppilim  23777  chto1ub  23778  chebbnd2  23779  chto1lb  23780  chpchtlim  23781  chpo1ub  23782  chpo1ubb  23783  vmadivsum  23784  vmadivsumb  23785  mudivsum  23832  mulogsumlem  23833  mulogsum  23834  logdivsum  23835  vmalogdivsum2  23840  vmalogdivsum  23841  selberglem1  23847  selberglem2  23848  selbergb  23851  selberg2lem  23852  selberg2  23853  selberg2b  23854  selberg3lem2  23860  selberg3  23861  selberg4  23863  pntrmax  23866  pntrsumo1  23867  pntrsumbnd  23868  selbergr  23870  selberg3r  23871  selberg4r  23872  selberg34r  23873  pntrlog2bndlem1  23879  pntrlog2bndlem4  23882  pnt2  23915  pnt  23916  istrkg2ld  23975  legval  24091  ttgsub  24303  cchhllem  24311  erclwwlkn  24949  vdegp1ai  25105  vdegp1bi  25106  isgrp2i  25355  circgrpOLD  25493  rngosn  25523  ipasslem7  25868  normlem6  26149  opsqrlem4  27178  eqri  27529  aciunf1  27649  fpwrelmap  27706  fpwrelmapffs  27707  xrs0  27816  circtopn  27994  cnre2csqima  28047  cnvordtrestixx  28049  mndpluscn  28062  xrge0iifcnv  28069  zlm0  28096  zlm1  28097  qqhre  28151  rrhre  28152  esumnul  28196  hasheuni  28233  sxbrsigalem2  28413  oddpwdc  28476  eulerpartlemb  28490  eulerpartgbij  28494  eulerpartlemn  28503  fib0  28521  fib1  28522  ballotlemrinv  28655  sgn3da  28663  signsw0g  28696  lgamf  28773  lgam1  28795  subfacval2  28820  sinccvglem  29227  circum  29229  logi  29287  faclim  29337  faclim2  29339  wl-cbvalnae  30151  wl-equsal  30158  dvtanlemOLD  30230  dvtan  30231  dvasin  30269  dvacos  30270  dvreasin  30271  dvreacos  30272  efald2  30641  areaquad  31352  lhe4.4ex1a  31402  dvsinax  31874  itgsin0pilem1  31914  iblempty  31930  stowei  32012  wallispilem5  32017  wallispi  32018  stirlinglem1  32022  stirlinglem12  32033  stirlinglem13  32034  stirlinglem14  32035  stirlingr  32038  dirkertrigeqlem1  32046  fourierdlem62  32117  fourierdlem73  32128  fourierdlem76  32131  fourierdlem77  32132  fourierdlem103  32158  fourierdlem104  32159  fourierclim  32173  fourier  32174  fouriersw  32180  etransclem41  32224  etransclem46  32229  joinlmuladdmuli  33522  sbtT  33683  eel0TT  33832  eelTTT  33834  eelT1  33839  eelTT  33908  eelT  33910  eelT0  33912  isosctrlem1ALT  34081  bj-spimev  34628  bj-inrab2  34843  bj-rabtrAUTO  34847