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  1492  cadbi123i  1507  nfbi  1994  spime  2067  nfeu  2287  nfmo  2288  eubii  2293  mobii  2294  abeq2i  2535  nfceqi  2561  nfeq  2575  nfel  2576  dvelimc  2586  nfral  2746  nfrex  2822  rexbiiOLD  2875  ralbiiOLD  2876  nfreu  2937  nfrmo  2938  nfrab  2944  nfsbc1  3256  nfsbc  3259  sbcbii  3293  nfcsb1  3348  nfcsb  3351  csbeq2i  3750  nfif  3878  nfdisj  4344  ssbri  4404  nfbr  4406  mpteq12i  4446  ralxfr  4577  reuxfr2  4583  reuxfr  4585  issoi  4743  nfiota  5507  nfriota  6215  nfov  6270  mpt2eq123i  6307  mpt2eq3ia  6309  eqer  7346  0er  7348  ecopover  7417  nfixp  7491  en2i  7556  en3i  7557  ener  7565  ensymb  7566  entr  7570  r0weon  8390  recmulnq  9335  axcnex  9517  nfneg  9817  negiso  10533  suprzcl2  11200  supxr  11544  xrinf0  11569  xrinfm0OLD  11573  cnrecnv  13167  cau3  13357  cbvsum  13699  sum0  13725  ackbijnn  13824  flo1  13850  trireciplem  13858  trirecip  13859  ege2le3  14082  rpnnen2lem3  14207  bitsf1ocnv  14356  prmreclem6  14803  prmrec  14804  modxai  14978  strfvn  15076  strss  15098  xpssca  15422  xpsvsca  15423  mreacs  15502  2oppccomf  15568  mndprop  16501  grpprop  16623  isgrpi  16630  gicer  16878  oppgmndb  16944  oppggrpb  16947  efgrelexlemb  17338  ablprop  17379  ringprop  17752  opprringb  17798  rlmbas  18356  rlmplusg  18357  rlm0  18358  rlmsub  18359  rlmmulr  18360  rlmsca2  18362  rlmvsca  18363  rlmtopn  18364  rlmds  18365  rlmvneg  18368  psrbagsn  18656  evlsval  18680  psr1bas2  18721  psr1bas  18722  psr1plusg  18753  psr1vsca  18754  psr1mulr  18755  ply1plusgfvi  18773  ply1mpl0  18786  ply1mpl1  18788  cncrng  18927  xrsmcmn  18929  cndrng  18935  cnsrng  18940  xrs1mnd  18944  xrs10  18945  absabv  18963  zringcyg  18997  recrng  19126  ordtrestixx  20175  llyidm  20440  nllyidm  20441  toplly  20442  hauslly  20444  hausnlly  20445  lly1stc  20448  kgenf  20493  hmpher  20736  txswaphmeolem  20756  fmucndlem  21243  nrgtrg  21629  cnfldnm  21736  xrsxmet  21764  divcn  21837  expcn  21841  elcncf1ii  21865  iirevcn  21895  iihalf1cn  21897  iihalf2cn  21899  iimulcn  21903  icopnfcnv  21907  iccpnfcnv  21909  cnrehmeo  21918  phtpcer  21963  tchsub  22132  tchphl  22138  iscmet3i  22218  cncmet  22227  rrxprds  22285  vitalilem1  22503  vitali  22508  i1f0  22582  itg20  22632  dvid  22809  dveflem  22868  dvef  22869  dvsincos  22870  ply1divalg2  23026  coe0  23147  iaa  23218  sincn  23336  coscn  23337  reefgim  23342  pilem3  23346  pilem3OLD  23347  resinf1o  23422  circgrp  23438  circsubm  23439  divlogrlim  23517  dvrelog  23519  logcn  23529  dvlog  23533  advlog  23536  cxpcn  23622  cxpcn2  23623  resqrtcn  23626  sqrtcn  23627  atansopn  23795  dvatan  23798  leibpilem2  23804  leibpi  23805  leibpisum  23806  log2cnv  23807  log2ublem2  23810  log2ub  23812  divsqrtsumlem  23842  emcllem4  23861  emcllem6  23863  emcllem7  23864  lgamf  23904  lgam1  23926  basellem6  23949  basellem7  23950  basellem8  23951  basellem9  23952  vmaf  23983  logfacrlim  24089  lgsdir2lem5  24192  chebbnd1  24247  chtppilim  24250  chto1ub  24251  chebbnd2  24252  chto1lb  24253  chpchtlim  24254  chpo1ub  24255  chpo1ubb  24256  vmadivsum  24257  vmadivsumb  24258  mudivsum  24305  mulogsumlem  24306  mulogsum  24307  logdivsum  24308  vmalogdivsum2  24313  vmalogdivsum  24314  selberglem1  24320  selberglem2  24321  selbergb  24324  selberg2lem  24325  selberg2  24326  selberg2b  24327  selberg3lem2  24333  selberg3  24334  selberg4  24336  pntrmax  24339  pntrsumo1  24340  pntrsumbnd  24341  selbergr  24343  selberg3r  24344  selberg4r  24345  selberg34r  24346  pntrlog2bndlem1  24352  pntrlog2bndlem4  24355  pnt2  24388  pnt  24389  istrkg2ld  24445  legval  24566  ttgsub  24846  cchhllem  24854  erclwwlkn  25493  vdegp1ai  25649  vdegp1bi  25650  isgrp2i  25901  circgrpOLD  26039  rngosn  26069  ipasslem7  26414  normlem6  26705  opsqrlem4  27733  eqri  28085  aciunf1  28206  fpwrelmap  28263  fpwrelmapffs  28264  xrs0  28383  mdetlap1  28599  circtopn  28611  cnre2csqima  28664  cnvordtrestixx  28666  mndpluscn  28679  xrge0iifcnv  28686  zlm0  28713  zlm1  28714  qqhre  28771  rrhre  28772  esumnul  28816  hasheuni  28853  sxbrsigalem2  29055  oddpwdc  29134  eulerpartlemb  29148  eulerpartgbij  29152  eulerpartlemn  29161  fib0  29179  fib1  29180  ballotlemrinv  29313  ballotlemrinvOLD  29351  sgn3da  29359  signsw0g  29392  subfacval2  29857  sinccvglem  30263  circum  30265  logi  30316  faclim  30328  faclim2  30330  bj-spimev  31222  bj-inrab2  31442  bj-rabtrAUTO  31447  sucneqoni  31676  wl-cbvalnae  31773  wl-equsal  31780  poimirlem30  31877  dvtanlemOLD  31898  dvtan  31899  dvasin  31935  dvacos  31936  dvreasin  31937  dvreacos  31938  efald2  32218  areaquad  36014  lhe4.4ex1a  36591  sbtT  36850  eel0TT  36999  eelTTT  37001  eelT1  37006  eelTT  37074  eelT  37076  eelT0  37078  isosctrlem1ALT  37247  disjsnxp  37330  dvsinax  37666  itgsin0pilem1  37709  iblempty  37725  stowei  37809  wallispilem5  37814  wallispi  37815  stirlinglem1  37819  stirlinglem12  37830  stirlinglem13  37831  stirlinglem14  37832  stirlingr  37835  dirkertrigeqlem1  37843  fourierdlem62  37915  fourierdlem73  37926  fourierdlem76  37929  fourierdlem77  37930  fourierdlem103  37956  fourierdlem104  37957  fourierclim  37971  fourier  37972  fouriersw  37978  etransclem41  38023  etransclem46  38028  sge00  38069  sge0sn  38072  joinlmuladdmuli  40105