Theorem trud 1371

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

Syntax hints:   -> wi 4   T. wtru 1363

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 1365

This theorem is referenced by:  hadbi123i  1428  cadbi123i  1429  nfbi  1865  spime  1951  nfeu  2270  nfmo  2271  eubii  2276  mobii  2277  dvelimc  2590  ralbii  2729  rexbii  2730  nfral  2759  nfreu  2885  nfrmo  2886  nfrab  2892  nfsbc1  3193  nfsbc  3196  sbcbii  3234  nfcsb1  3291  nfcsb  3294  csbeq2i  3676  nfif  3806  nfdisj  4262  ssbri  4322  nfbr  4324  mpteq12i  4364  ralxfr  4498  reuxfr2  4504  reuxfr  4506  issoi  4659  nfiota  5373  nfriota  6049  nfov  6103  mpt2eq123i  6138  mpt2eq3ia  6140  eqer  7122  0er  7124  ecopover  7192  nfixp  7270  en2i  7335  en3i  7336  ener  7344  ensymb  7345  entr  7349  r0weon  8167  recmulnq  9121  axcnex  9302  nfneg  9594  negiso  10294  suprzcl2  10933  supxr  11263  xrinfm0  11287  cnrecnv  12638  cau3  12827  cbvsum  13156  sum0  13182  ackbijnn  13274  flo1  13300  trireciplem  13307  trirecip  13308  ege2le3  13358  rpnnen2lem3  13482  bitsf1ocnv  13623  prmreclem6  13965  prmrec  13966  modxai  14080  strfvn  14174  strss  14194  xpssca  14499  xpsvsca  14500  mreacs  14579  2oppccomf  14647  mndprop  15431  grpprop  15537  isgrpi  15544  gicer  15784  oppgmndb  15850  oppggrpb  15853  efgrelexlemb  16227  ablprop  16268  rngprop  16614  opprrngb  16658  rlmbas  17198  rlmplusg  17199  rlm0  17200  rlmsub  17201  rlmmulr  17202  rlmsca2  17204  rlmvsca  17205  rlmtopn  17206  rlmds  17207  rlmvneg  17210  psrbagsn  17509  psr1bas2  17545  psr1bas  17546  psr1plusg  17575  psr1vsca  17576  psr1mulr  17577  ply1plusgfvi  17595  ply1mpl0  17608  ply1mpl1  17609  cncrng  17681  xrsmcmn  17683  cndrng  17689  cnsrng  17694  xrs1mnd  17695  xrs10  17696  absabv  17714  zringcyg  17749  zcyg  17754  recrng  17893  ordtrestixx  18668  llyidm  18934  nllyidm  18935  toplly  18936  hauslly  18938  hausnlly  18939  lly1stc  18942  kgenf  18956  hmpher  19199  txswaphmeolem  19219  fmucndlem  19708  nrgtrg  20112  cnfldnm  20200  xrsxmet  20228  divcn  20286  expcn  20290  elcncf1ii  20314  iirevcn  20344  iihalf1cn  20346  iihalf2cn  20348  iimulcn  20352  icopnfcnv  20356  iccpnfcnv  20358  cnrehmeo  20367  phtpcer  20409  tchsub  20578  tchphl  20584  iscmet3i  20664  cncmet  20675  rrxprds  20735  vitalilem1  20930  vitali  20935  i1f0  21007  itg20  21057  dvid  21234  dveflem  21293  dvef  21294  dvsincos  21295  evlsval  21371  ply1divalg2  21495  coe0  21608  iaa  21676  sincn  21794  coscn  21795  reefgim  21800  pilem3  21803  resinf1o  21877  divlogrlim  21965  dvrelog  21967  logcn  21977  dvlog  21981  advlog  21984  cxpcn  22068  cxpcn2  22069  resqrcn  22072  sqrcn  22073  atansopn  22212  dvatan  22215  leibpilem2  22221  leibpi  22222  leibpisum  22223  log2cnv  22224  log2ublem2  22227  log2ub  22229  divsqrsumlem  22258  emcllem4  22277  emcllem6  22279  emcllem7  22280  basellem6  22308  basellem7  22309  basellem8  22310  basellem9  22311  vmaf  22342  logfacrlim  22448  lgsdir2lem5  22551  chebbnd1  22606  chtppilim  22609  chto1ub  22610  chebbnd2  22611  chto1lb  22612  chpchtlim  22613  chpo1ub  22614  chpo1ubb  22615  vmadivsum  22616  vmadivsumb  22617  mudivsum  22664  mulogsumlem  22665  mulogsum  22666  logdivsum  22667  vmalogdivsum2  22672  vmalogdivsum  22673  selberglem1  22679  selberglem2  22680  selbergb  22683  selberg2lem  22684  selberg2  22685  selberg2b  22686  selberg3lem2  22692  selberg3  22693  selberg4  22695  pntrmax  22698  pntrsumo1  22699  pntrsumbnd  22700  selbergr  22702  selberg3r  22703  selberg4r  22704  selberg34r  22705  pntrlog2bndlem1  22711  pntrlog2bndlem4  22714  pnt2  22747  pnt  22748  legval  22891  ttgsub  22948  cchhllem  22956  vdegp1ai  23428  vdegp1bi  23429  isgrp2i  23546  circgrp  23684  rngosn  23714  ipasslem7  24059  normlem6  24340  opsqrlem4  25370  eqri  25718  fpwrelmap  25858  fpwrelmapffs  25859  xrs0  25959  cnre2csqima  26195  cnvordtrestixx  26197  mndpluscn  26210  xrge0iifcnv  26217  zlm0  26245  zlm1  26246  qqhre  26300  rrhre  26301  esumnul  26356  hasheuni  26388  sxbrsigalem2  26555  oddpwdc  26585  eulerpartlemb  26599  eulerpartgbij  26603  eulerpartlemn  26612  fib0  26630  fib1  26631  ballotlemrinv  26764  sgn3da  26772  signsw0g  26805  lgamf  26876  lgam1  26898  subfacval2  26923  sinccvglem  27164  circum  27166  faclim  27399  faclim2  27401  wl-cbvalnae  28210  wl-equsal  28217  dvtanlem  28285  dvtan  28286  dvasin  28324  dvacos  28325  dvreasin  28326  dvreacos  28327  efald2  28722  lhe4.4ex1a  29448  itgsin0pilem1  29636  stowei  29705  wallispilem5  29710  wallispi  29711  stirlinglem1  29715  stirlinglem12  29726  stirlinglem13  29727  stirlinglem14  29728  stirlingr  29731  erclwwlkn  30348  sbtT  30980  eel0TT  31130  eelTTT  31132  eelT1  31137  eelTT  31206  eelT  31208  eelT0  31210  isosctrlem1ALT  31372  bj-spimev  31848  bj-inrab2  32017  bj-rabtrAUTO  32020