Theorem trud 1446

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

Syntax hints:   -> wi 4   T. wtru 1438

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 188  df-tru 1440

This theorem is referenced by:  hadbi123i  1494  cadbi123i  1509  nfbi  1992  spime  2064  nfeu  2284  nfmo  2285  eubii  2290  mobii  2291  abeq2i  2556  nfceqi  2587  nfeq  2602  nfel  2604  dvelimc  2615  nfral  2818  nfrex  2895  rexbiiOLD  2948  ralbiiOLD  2949  nfreu  3010  nfrmo  3011  nfrab  3017  nfsbc1  3324  nfsbc  3327  sbcbii  3361  nfcsb1  3416  nfcsb  3419  csbeq2i  3816  nfif  3944  nfdisj  4409  ssbri  4468  nfbr  4470  mpteq12i  4510  ralxfr  4640  reuxfr2  4646  reuxfr  4648  issoi  4806  nfiota  5569  nfriota  6276  nfov  6331  mpt2eq123i  6368  mpt2eq3ia  6370  eqer  7404  0er  7406  ecopover  7475  nfixp  7549  en2i  7614  en3i  7615  ener  7623  ensymb  7624  entr  7628  r0weon  8442  recmulnq  9388  axcnex  9570  nfneg  9870  negiso  10587  suprzcl2  11254  supxr  11598  xrinf0  11623  xrinfm0OLD  11627  cnrecnv  13207  cau3  13397  cbvsum  13739  sum0  13765  ackbijnn  13864  flo1  13890  trireciplem  13898  trirecip  13899  ege2le3  14122  rpnnen2lem3  14247  bitsf1ocnv  14392  prmreclem6  14819  prmrec  14820  modxai  14994  strfvn  15092  strss  15114  xpssca  15426  xpsvsca  15427  mreacs  15506  2oppccomf  15572  mndprop  16505  grpprop  16627  isgrpi  16634  gicer  16882  oppgmndb  16948  oppggrpb  16951  efgrelexlemb  17326  ablprop  17367  ringprop  17740  opprringb  17786  rlmbas  18344  rlmplusg  18345  rlm0  18346  rlmsub  18347  rlmmulr  18348  rlmsca2  18350  rlmvsca  18351  rlmtopn  18352  rlmds  18353  rlmvneg  18356  psrbagsn  18644  evlsval  18668  psr1bas2  18709  psr1bas  18710  psr1plusg  18741  psr1vsca  18742  psr1mulr  18743  ply1plusgfvi  18761  ply1mpl0  18774  ply1mpl1  18776  cncrng  18915  xrsmcmn  18917  cndrng  18923  cnsrng  18928  xrs1mnd  18932  xrs10  18933  absabv  18951  zringcyg  18982  recrng  19111  ordtrestixx  20160  llyidm  20425  nllyidm  20426  toplly  20427  hauslly  20429  hausnlly  20430  lly1stc  20433  kgenf  20478  hmpher  20721  txswaphmeolem  20741  fmucndlem  21228  nrgtrg  21614  cnfldnm  21701  xrsxmet  21729  divcn  21787  expcn  21791  elcncf1ii  21815  iirevcn  21845  iihalf1cn  21847  iihalf2cn  21849  iimulcn  21853  icopnfcnv  21857  iccpnfcnv  21859  cnrehmeo  21868  phtpcer  21910  tchsub  22079  tchphl  22085  iscmet3i  22165  cncmet  22174  rrxprds  22232  vitalilem1  22434  vitali  22439  i1f0  22513  itg20  22563  dvid  22740  dveflem  22799  dvef  22800  dvsincos  22801  ply1divalg2  22955  coe0  23069  iaa  23137  sincn  23255  coscn  23256  reefgim  23261  pilem3  23265  pilem3OLD  23266  resinf1o  23341  circgrp  23357  circsubm  23358  divlogrlim  23436  dvrelog  23438  logcn  23448  dvlog  23452  advlog  23455  cxpcn  23541  cxpcn2  23542  resqrtcn  23545  sqrtcn  23546  atansopn  23714  dvatan  23717  leibpilem2  23723  leibpi  23724  leibpisum  23725  log2cnv  23726  log2ublem2  23729  log2ub  23731  divsqrtsumlem  23761  emcllem4  23780  emcllem6  23782  emcllem7  23783  lgamf  23823  lgam1  23845  basellem6  23866  basellem7  23867  basellem8  23868  basellem9  23869  vmaf  23900  logfacrlim  24006  lgsdir2lem5  24109  chebbnd1  24164  chtppilim  24167  chto1ub  24168  chebbnd2  24169  chto1lb  24170  chpchtlim  24171  chpo1ub  24172  chpo1ubb  24173  vmadivsum  24174  vmadivsumb  24175  mudivsum  24222  mulogsumlem  24223  mulogsum  24224  logdivsum  24225  vmalogdivsum2  24230  vmalogdivsum  24231  selberglem1  24237  selberglem2  24238  selbergb  24241  selberg2lem  24242  selberg2  24243  selberg2b  24244  selberg3lem2  24250  selberg3  24251  selberg4  24253  pntrmax  24256  pntrsumo1  24257  pntrsumbnd  24258  selbergr  24260  selberg3r  24261  selberg4r  24262  selberg34r  24263  pntrlog2bndlem1  24269  pntrlog2bndlem4  24272  pnt2  24305  pnt  24306  istrkg2ld  24362  legval  24480  ttgsub  24746  cchhllem  24754  erclwwlkn  25392  vdegp1ai  25548  vdegp1bi  25549  isgrp2i  25800  circgrpOLD  25938  rngosn  25968  ipasslem7  26313  normlem6  26594  opsqrlem4  27622  eqri  27974  aciunf1  28096  fpwrelmap  28152  fpwrelmapffs  28153  xrs0  28265  mdetlap1  28482  circtopn  28494  cnre2csqima  28547  cnvordtrestixx  28549  mndpluscn  28562  xrge0iifcnv  28569  zlm0  28596  zlm1  28597  qqhre  28654  rrhre  28655  esumnul  28699  hasheuni  28736  sxbrsigalem2  28938  oddpwdc  29004  eulerpartlemb  29018  eulerpartgbij  29022  eulerpartlemn  29031  fib0  29049  fib1  29050  ballotlemrinv  29183  sgn3da  29191  signsw0g  29224  subfacval2  29689  sinccvglem  30095  circum  30097  logi  30148  faclim  30160  faclim2  30162  bj-spimev  31052  bj-inrab2  31272  bj-rabtrAUTO  31276  wl-cbvalnae  31564  wl-equsal  31571  poimirlem30  31664  dvtanlemOLD  31685  dvtan  31686  dvasin  31722  dvacos  31723  dvreasin  31724  dvreacos  31725  efald2  32005  areaquad  35790  lhe4.4ex1a  36305  sbtT  36564  eel0TT  36713  eelTTT  36715  eelT1  36720  eelTT  36788  eelT  36790  eelT0  36792  isosctrlem1ALT  36961  dvsinax  37345  itgsin0pilem1  37385  iblempty  37401  stowei  37485  wallispilem5  37490  wallispi  37491  stirlinglem1  37495  stirlinglem12  37506  stirlinglem13  37507  stirlinglem14  37508  stirlingr  37511  dirkertrigeqlem1  37519  fourierdlem62  37590  fourierdlem73  37601  fourierdlem76  37604  fourierdlem77  37605  fourierdlem103  37631  fourierdlem104  37632  fourierclim  37646  fourier  37647  fouriersw  37653  etransclem41  37697  etransclem46  37702  sge00  37742  sge0sn  37745  joinlmuladdmuli  39263