Theorem trud 1464

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

Syntax hints:   -> wi 4   T. wtru 1456

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 190  df-tru 1458

This theorem is referenced by:  hadbi123i  1510  cadbi123i  1525  nfbi  2028  spime  2111  nfeu  2326  nfmo  2327  eubii  2332  mobii  2333  abeq2i  2574  nfceqi  2600  nfeq  2614  nfel  2615  dvelimc  2625  nfral  2786  nfrex  2862  rexbiiOLD  2915  ralbiiOLD  2916  nfreu  2977  nfrmo  2978  nfrab  2984  nfsbc1  3298  nfsbc  3301  sbcbii  3335  nfcsb1  3390  nfcsb  3393  csbeq2i  3794  nfif  3922  nfdisj  4399  ssbri  4459  nfbr  4461  mpteq12i  4501  ralxfr  4632  reuxfr2  4638  reuxfr  4640  issoi  4805  nfiota  5569  nfriota  6286  nfov  6341  mpt2eq123i  6381  mpt2eq3ia  6383  eqer  7422  0er  7424  ecopover  7493  nfixp  7567  en2i  7633  en3i  7634  ener  7642  ensymb  7643  entr  7647  r0weon  8469  recmulnq  9415  axcnex  9597  nfneg  9897  negiso  10615  suprzcl2  11283  supxr  11627  xrinf0  11652  xrinfm0OLD  11656  cnrecnv  13277  cau3  13467  cbvsum  13810  sum0  13836  ackbijnn  13935  flo1  13961  trireciplem  13969  trirecip  13970  ege2le3  14193  rpnnen2lem3  14318  bitsf1ocnv  14467  prmreclem6  14914  prmrec  14915  modxai  15089  strfvn  15187  strss  15209  xpssca  15533  xpsvsca  15534  mreacs  15613  2oppccomf  15679  mndprop  16612  grpprop  16734  isgrpi  16741  gicer  16989  oppgmndb  17055  oppggrpb  17058  efgrelexlemb  17449  ablprop  17490  ringprop  17863  opprringb  17909  rlmbas  18467  rlmplusg  18468  rlm0  18469  rlmsub  18470  rlmmulr  18471  rlmsca2  18473  rlmvsca  18474  rlmtopn  18475  rlmds  18476  rlmvneg  18479  psrbagsn  18767  evlsval  18791  psr1bas2  18832  psr1bas  18833  psr1plusg  18864  psr1vsca  18865  psr1mulr  18866  ply1plusgfvi  18884  ply1mpl0  18897  ply1mpl1  18899  cncrng  19038  xrsmcmn  19040  cndrng  19046  cnsrng  19051  xrs1mnd  19055  xrs10  19056  absabv  19074  zringcyg  19109  recrng  19238  ordtrestixx  20287  llyidm  20552  nllyidm  20553  toplly  20554  hauslly  20556  hausnlly  20557  lly1stc  20560  kgenf  20605  hmpher  20848  txswaphmeolem  20868  fmucndlem  21355  nrgtrg  21741  cnfldnm  21848  xrsxmet  21876  divcn  21949  expcn  21953  elcncf1ii  21977  iirevcn  22007  iihalf1cn  22009  iihalf2cn  22011  iimulcn  22015  icopnfcnv  22019  iccpnfcnv  22021  cnrehmeo  22030  phtpcer  22075  tchsub  22244  tchphl  22250  iscmet3i  22330  cncmet  22339  rrxprds  22397  vitalilem1  22615  vitali  22620  i1f0  22694  itg20  22744  dvid  22921  dveflem  22980  dvef  22981  dvsincos  22982  ply1divalg2  23138  coe0  23259  iaa  23330  sincn  23448  coscn  23449  reefgim  23454  pilem3  23458  pilem3OLD  23459  resinf1o  23534  circgrp  23550  circsubm  23551  divlogrlim  23629  dvrelog  23631  logcn  23641  dvlog  23645  advlog  23648  cxpcn  23734  cxpcn2  23735  resqrtcn  23738  sqrtcn  23739  atansopn  23907  dvatan  23910  leibpilem2  23916  leibpi  23917  leibpisum  23918  log2cnv  23919  log2ublem2  23922  log2ub  23924  divsqrtsumlem  23954  emcllem4  23973  emcllem6  23975  emcllem7  23976  lgamf  24016  lgam1  24038  basellem6  24061  basellem7  24062  basellem8  24063  basellem9  24064  vmaf  24095  logfacrlim  24201  lgsdir2lem5  24304  chebbnd1  24359  chtppilim  24362  chto1ub  24363  chebbnd2  24364  chto1lb  24365  chpchtlim  24366  chpo1ub  24367  chpo1ubb  24368  vmadivsum  24369  vmadivsumb  24370  mudivsum  24417  mulogsumlem  24418  mulogsum  24419  logdivsum  24420  vmalogdivsum2  24425  vmalogdivsum  24426  selberglem1  24432  selberglem2  24433  selbergb  24436  selberg2lem  24437  selberg2  24438  selberg2b  24439  selberg3lem2  24445  selberg3  24446  selberg4  24448  pntrmax  24451  pntrsumo1  24452  pntrsumbnd  24453  selbergr  24455  selberg3r  24456  selberg4r  24457  selberg34r  24458  pntrlog2bndlem1  24464  pntrlog2bndlem4  24467  pnt2  24500  pnt  24501  istrkg2ld  24557  legval  24678  ttgsub  24958  cchhllem  24966  erclwwlkn  25605  vdegp1ai  25761  vdegp1bi  25762  isgrp2i  26013  circgrpOLD  26151  rngosn  26181  ipasslem7  26526  normlem6  26817  opsqrlem4  27845  eqri  28196  aciunf1  28314  fpwrelmap  28367  fpwrelmapffs  28368  xrs0  28486  mdetlap1  28701  circtopn  28713  cnre2csqima  28766  cnvordtrestixx  28768  mndpluscn  28781  xrge0iifcnv  28788  zlm0  28815  zlm1  28816  qqhre  28873  rrhre  28874  esumnul  28918  hasheuni  28955  sxbrsigalem2  29157  oddpwdc  29236  eulerpartlemb  29250  eulerpartgbij  29254  eulerpartlemn  29263  fib0  29281  fib1  29282  ballotlemrinv  29415  ballotlemrinvOLD  29453  sgn3da  29461  signsw0g  29494  subfacval2  29959  sinccvglem  30365  circum  30367  logi  30419  faclim  30431  faclim2  30433  bj-spimev  31366  bj-inrab2  31576  bj-rabtrAUTO  31581  sucneqoni  31814  wl-cbvalnae  31911  wl-equsal  31918  poimirlem30  32015  dvtanlemOLD  32036  dvtan  32037  dvasin  32073  dvacos  32074  dvreasin  32075  dvreacos  32076  efald2  32356  areaquad  36146  lhe4.4ex1a  36722  sbtT  36979  eel0TT  37127  eelTTT  37129  eelT1  37133  eelTT  37198  eelT  37200  eelT0  37202  isosctrlem1ALT  37371  disjsnxp  37451  dvsinax  37821  itgsin0pilem1  37864  iblempty  37880  stowei  37964  wallispilem5  37969  wallispi  37970  stirlinglem1  37974  stirlinglem12  37985  stirlinglem13  37986  stirlinglem14  37987  stirlingr  37990  dirkertrigeqlem1  37998  fourierdlem62  38070  fourierdlem73  38081  fourierdlem76  38084  fourierdlem77  38085  fourierdlem103  38111  fourierdlem104  38112  fourierclim  38126  fourier  38127  fouriersw  38133  etransclem41  38178  etransclem46  38183  salexct2  38236  salexct3  38239  salgencntex  38240  salgensscntex  38241  sge00  38256  sge0sn  38259  1wlksv  39683  joinlmuladdmuli  40785