Theorem trud 1404

Description: Eliminate as an antecedent. A proposition implied by is true. (Contributed by Mario Carneiro, 13-Mar-2014.)

Hypothesis

Ref	Expression
trud.1

Assertion

Ref	Expression
trud

Proof of Theorem trud

Step	Hyp	Ref	Expression
1		tru 1399	. 2
2		trud.1	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  ->wi 4  wtru 1396

This theorem is referenced by:  hadbi123i  1451  cadbi123i  1452  nfbi  1934  spime  2008  nfeu  2300  nfmo  2301  eubii  2306  mobii  2307  abeq2i  2584  nfceqi  2615  nfeq  2630  nfel  2632  dvelimc  2643  nfral  2843  nfrex  2920  rexbiiOLD  2970  ralbiiOLD  2971  nfreu  3032  nfrmo  3033  nfrab  3039  nfsbc1  3346  nfsbc  3349  sbcbii  3387  nfcsb1  3449  nfcsb  3452  csbeq2i  3836  nfif  3970  nfdisj  4434  ssbri  4494  nfbr  4496  mpteq12i  4536  ralxfr  4670  reuxfr2  4676  reuxfr  4678  issoi  4836  nfiota  5560  nfriota  6266  nfov  6322  mpt2eq123i  6360  mpt2eq3ia  6362  eqer  7363  0er  7365  ecopover  7434  nfixp  7508  en2i  7573  en3i  7574  ener  7582  ensymb  7583  entr  7587  r0weon  8411  recmulnq  9363  axcnex  9545  nfneg  9839  negiso  10544  suprzcl2  11201  supxr  11533  xrinfm0  11557  cnrecnv  12998  cau3  13188  cbvsum  13517  sum0  13543  ackbijnn  13640  flo1  13666  trireciplem  13673  trirecip  13674  ege2le3  13825  rpnnen2lem3  13950  bitsf1ocnv  14094  prmreclem6  14439  prmrec  14440  modxai  14554  strfvn  14649  strss  14669  xpssca  14975  xpsvsca  14976  mreacs  15055  2oppccomf  15120  mndprop  15947  grpprop  16069  isgrpi  16076  gicer  16324  oppgmndb  16390  oppggrpb  16393  efgrelexlemb  16768  ablprop  16809  ringprop  17232  opprringb  17281  rlmbas  17841  rlmplusg  17842  rlm0  17843  rlmsub  17844  rlmmulr  17845  rlmsca2  17847  rlmvsca  17848  rlmtopn  17849  rlmds  17850  rlmvneg  17853  psrbagsn  18160  evlsval  18188  psr1bas2  18229  psr1bas  18230  psr1plusg  18263  psr1vsca  18264  psr1mulr  18265  ply1plusgfvi  18283  ply1mpl0  18296  ply1mpl1  18298  cncrng  18439  xrsmcmn  18441  cndrng  18447  cnsrng  18452  xrs1mnd  18456  xrs10  18457  absabv  18475  zringcyg  18513  zcyg  18518  recrng  18657  ordtrestixx  19723  llyidm  19989  nllyidm  19990  toplly  19991  hauslly  19993  hausnlly  19994  lly1stc  19997  kgenf  20042  hmpher  20285  txswaphmeolem  20305  fmucndlem  20794  nrgtrg  21198  cnfldnm  21286  xrsxmet  21314  divcn  21372  expcn  21376  elcncf1ii  21400  iirevcn  21430  iihalf1cn  21432  iihalf2cn  21434  iimulcn  21438  icopnfcnv  21442  iccpnfcnv  21444  cnrehmeo  21453  phtpcer  21495  tchsub  21664  tchphl  21670  iscmet3i  21750  cncmet  21761  rrxprds  21821  vitalilem1  22017  vitali  22022  i1f0  22094  itg20  22144  dvid  22321  dveflem  22380  dvef  22381  dvsincos  22382  ply1divalg2  22539  coe0  22653  iaa  22721  sincn  22839  coscn  22840  reefgim  22845  pilem3  22848  resinf1o  22923  circgrp  22939  circsubm  22940  divlogrlim  23016  dvrelog  23018  logcn  23028  dvlog  23032  advlog  23035  cxpcn  23119  cxpcn2  23120  resqrtcn  23123  sqrtcn  23124  atansopn  23263  dvatan  23266  leibpilem2  23272  leibpi  23273  leibpisum  23274  log2cnv  23275  log2ublem2  23278  log2ub  23280  divsqrtsumlem  23309  emcllem4  23328  emcllem6  23330  emcllem7  23331  basellem6  23359  basellem7  23360  basellem8  23361  basellem9  23362  vmaf  23393  logfacrlim  23499  lgsdir2lem5  23602  chebbnd1  23657  chtppilim  23660  chto1ub  23661  chebbnd2  23662  chto1lb  23663  chpchtlim  23664  chpo1ub  23665  chpo1ubb  23666  vmadivsum  23667  vmadivsumb  23668  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  logdivsum  23718  vmalogdivsum2  23723  vmalogdivsum  23724  selberglem1  23730  selberglem2  23731  selbergb  23734  selberg2lem  23735  selberg2  23736  selberg2b  23737  selberg3lem2  23743  selberg3  23744  selberg4  23746  pntrmax  23749  pntrsumo1  23750  pntrsumbnd  23751  selbergr  23753  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntrlog2bndlem1  23762  pntrlog2bndlem4  23765  pnt2  23798  pnt  23799  istrkg2ld  23858  legval  23971  ttgsub  24182  cchhllem  24190  erclwwlkn  24828  vdegp1ai  24984  vdegp1bi  24985  isgrp2i  25238  circgrpOLD  25376  rngosn  25406  ipasslem7  25751  normlem6  26032  opsqrlem4  27062  eqri  27411  fpwrelmap  27556  fpwrelmapffs  27557  xrs0  27663  circtopn  27840  cnre2csqima  27893  cnvordtrestixx  27895  mndpluscn  27908  xrge0iifcnv  27915  zlm0  27943  zlm1  27944  qqhre  27998  rrhre  27999  esumnul  28059  hasheuni  28091  sxbrsigalem2  28257  oddpwdc  28293  eulerpartlemb  28307  eulerpartgbij  28311  eulerpartlemn  28320  fib0  28338  fib1  28339  ballotlemrinv  28472  sgn3da  28480  signsw0g  28513  lgamf  28584  lgam1  28606  subfacval2  28631  sinccvglem  29038  circum  29040  logi  29121  faclim  29171  faclim2  29173  wl-cbvalnae  29986  wl-equsal  29993  dvtanlem  30064  dvtan  30065  dvasin  30103  dvacos  30104  dvreasin  30105  dvreacos  30106  efald2  30475  areaquad  31184  lhe4.4ex1a  31234  dvsinax  31708  itgsin0pilem1  31748  iblempty  31764  stowei  31846  wallispilem5  31851  wallispi  31852  stirlinglem1  31856  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlingr  31872  dirkertrigeqlem1  31880  fourierdlem62  31951  fourierdlem73  31962  fourierdlem76  31965  fourierdlem77  31966  fourierdlem103  31992  fourierdlem104  31993  fourierclim  32007  fourier  32008  fouriersw  32014  etransclem41  32058  etransclem46  32063  joinlmuladdmuli  33188  sbtT  33343  eel0TT  33492  eelTTT  33494  eelT1  33499  eelTT  33568  eelT  33570  eelT0  33572  isosctrlem1ALT  33734  bj-spimev  34281  bj-inrab2  34496  bj-rabtrAUTO  34499

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 1398