Theorem trud 1378

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

Syntax hints:   -> wi 4   T. wtru 1370

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 1372

This theorem is referenced by:  hadbi123i  1425  cadbi123i  1426  nfbi  1867  spime  1952  nfeu  2272  nfmo  2273  eubii  2278  mobii  2279  abeq2i  2554  nfceqi  2585  nfeq  2599  nfel  2601  dvelimc  2612  ralbii  2760  rexbii  2761  nfral  2790  nfreu  2916  nfrmo  2917  nfrab  2923  nfsbc1  3226  nfsbc  3229  sbcbii  3267  nfcsb1  3324  nfcsb  3327  csbeq2i  3709  nfif  3839  nfdisj  4295  ssbri  4355  nfbr  4357  mpteq12i  4397  ralxfr  4531  reuxfr2  4537  reuxfr  4539  issoi  4693  nfiota  5406  nfriota  6082  nfov  6135  mpt2eq123i  6170  mpt2eq3ia  6172  eqer  7155  0er  7157  ecopover  7225  nfixp  7303  en2i  7368  en3i  7369  ener  7377  ensymb  7378  entr  7382  r0weon  8200  recmulnq  9154  axcnex  9335  nfneg  9627  negiso  10327  suprzcl2  10966  supxr  11296  xrinfm0  11320  cnrecnv  12675  cau3  12864  cbvsum  13193  sum0  13219  ackbijnn  13312  flo1  13338  trireciplem  13345  trirecip  13346  ege2le3  13396  rpnnen2lem3  13520  bitsf1ocnv  13661  prmreclem6  14003  prmrec  14004  modxai  14118  strfvn  14212  strss  14232  xpssca  14537  xpsvsca  14538  mreacs  14617  2oppccomf  14685  mndprop  15469  grpprop  15578  isgrpi  15585  gicer  15825  oppgmndb  15891  oppggrpb  15894  efgrelexlemb  16268  ablprop  16309  rngprop  16700  opprrngb  16746  rlmbas  17298  rlmplusg  17299  rlm0  17300  rlmsub  17301  rlmmulr  17302  rlmsca2  17304  rlmvsca  17305  rlmtopn  17306  rlmds  17307  rlmvneg  17310  psrbagsn  17599  evlsval  17627  psr1bas2  17668  psr1bas  17669  psr1plusg  17698  psr1vsca  17699  psr1mulr  17700  ply1plusgfvi  17719  ply1mpl0  17732  ply1mpl1  17733  cncrng  17859  xrsmcmn  17861  cndrng  17867  cnsrng  17872  xrs1mnd  17873  xrs10  17874  absabv  17892  zringcyg  17929  zcyg  17934  recrng  18073  ordtrestixx  18848  llyidm  19114  nllyidm  19115  toplly  19116  hauslly  19118  hausnlly  19119  lly1stc  19122  kgenf  19136  hmpher  19379  txswaphmeolem  19399  fmucndlem  19888  nrgtrg  20292  cnfldnm  20380  xrsxmet  20408  divcn  20466  expcn  20470  elcncf1ii  20494  iirevcn  20524  iihalf1cn  20526  iihalf2cn  20528  iimulcn  20532  icopnfcnv  20536  iccpnfcnv  20538  cnrehmeo  20547  phtpcer  20589  tchsub  20758  tchphl  20764  iscmet3i  20844  cncmet  20855  rrxprds  20915  vitalilem1  21110  vitali  21115  i1f0  21187  itg20  21237  dvid  21414  dveflem  21473  dvef  21474  dvsincos  21475  ply1divalg2  21632  coe0  21745  iaa  21813  sincn  21931  coscn  21932  reefgim  21937  pilem3  21940  resinf1o  22014  divlogrlim  22102  dvrelog  22104  logcn  22114  dvlog  22118  advlog  22121  cxpcn  22205  cxpcn2  22206  resqrcn  22209  sqrcn  22210  atansopn  22349  dvatan  22352  leibpilem2  22358  leibpi  22359  leibpisum  22360  log2cnv  22361  log2ublem2  22364  log2ub  22366  divsqrsumlem  22395  emcllem4  22414  emcllem6  22416  emcllem7  22417  basellem6  22445  basellem7  22446  basellem8  22447  basellem9  22448  vmaf  22479  logfacrlim  22585  lgsdir2lem5  22688  chebbnd1  22743  chtppilim  22746  chto1ub  22747  chebbnd2  22748  chto1lb  22749  chpchtlim  22750  chpo1ub  22751  chpo1ubb  22752  vmadivsum  22753  vmadivsumb  22754  mudivsum  22801  mulogsumlem  22802  mulogsum  22803  logdivsum  22804  vmalogdivsum2  22809  vmalogdivsum  22810  selberglem1  22816  selberglem2  22817  selbergb  22820  selberg2lem  22821  selberg2  22822  selberg2b  22823  selberg3lem2  22829  selberg3  22830  selberg4  22832  pntrmax  22835  pntrsumo1  22836  pntrsumbnd  22837  selbergr  22839  selberg3r  22840  selberg4r  22841  selberg34r  22842  pntrlog2bndlem1  22848  pntrlog2bndlem4  22851  pnt2  22884  pnt  22885  legval  23037  ttgsub  23147  cchhllem  23155  vdegp1ai  23627  vdegp1bi  23628  isgrp2i  23745  circgrp  23883  rngosn  23913  ipasslem7  24258  normlem6  24539  opsqrlem4  25569  eqri  25916  fpwrelmap  26055  fpwrelmapffs  26056  xrs0  26158  cnre2csqima  26363  cnvordtrestixx  26365  mndpluscn  26378  xrge0iifcnv  26385  zlm0  26413  zlm1  26414  qqhre  26468  rrhre  26469  esumnul  26524  hasheuni  26556  sxbrsigalem2  26723  oddpwdc  26759  eulerpartlemb  26773  eulerpartgbij  26777  eulerpartlemn  26786  fib0  26804  fib1  26805  ballotlemrinv  26938  sgn3da  26946  signsw0g  26979  lgamf  27050  lgam1  27072  subfacval2  27097  sinccvglem  27339  circum  27341  faclim  27574  faclim2  27576  wl-cbvalnae  28388  wl-equsal  28395  dvtanlem  28467  dvtan  28468  dvasin  28506  dvacos  28507  dvreasin  28508  dvreacos  28509  efald2  28904  areaquad  29618  lhe4.4ex1a  29629  itgsin0pilem1  29816  stowei  29885  wallispilem5  29890  wallispi  29891  stirlinglem1  29895  stirlinglem12  29906  stirlinglem13  29907  stirlinglem14  29908  stirlingr  29911  erclwwlkn  30528  joinlmuladdmuli  31221  sbtT  31375  eel0TT  31524  eelTTT  31526  eelT1  31531  eelTT  31600  eelT  31602  eelT0  31604  isosctrlem1ALT  31766  bj-spimev  32313  bj-inrab2  32527  bj-rabtrAUTO  32530