MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantrurd Unicode version

Theorem biantrurd 508
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
biantrud.1
Assertion
Ref Expression
biantrurd

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2
2 ibar 504 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  3anibar  1164  3biant1d  1337  elrab3t  3256  rmob2  3432  n0moeu  3798  eldifvsn  4162  reusv7OLD  4664  reuxfrd  4677  opbrop  5084  opelresi  5290  xpco  5552  funcnv3  5654  fnssresb  5698  dff1o5  5830  fneqeql2  5996  dffo3  6046  fmptco  6064  fconst4  6136  riota2df  6278  eloprabga  6389  fnwelem  6915  mptsuppd  6942  mptelixpg  7526  boxcutc  7532  inficl  7905  wemapso2OLD  7998  wemapso2lem  7999  cantnfle  8111  cantnflem1  8129  cantnfleOLD  8141  bnd2  8332  iscard2  8378  alephinit  8497  kmlem2  8552  cfss  8666  fpwwe2lem9  9037  axgroth2  9224  elnnnn0  10864  znnsub  10935  znn0sub  10936  uzin  11142  xsubge0  11482  supxrre1  11551  ixxun  11574  divelunit  11691  elfz5  11709  uzsplit  11779  injresinj  11926  hashf1lem1  12504  swrdspsleq  12673  repswsymball  12751  repswsymballbi  12752  2shfti  12913  cnpart  13073  sqrtneglem  13100  rexuz3  13181  rlim  13318  rlim2  13319  clim2c  13328  ello12  13339  elo12  13350  fsumss  13547  fsumcom2  13589  cvgcmp  13630  fprodss  13755  fprodcom2  13788  bitsmod  14086  bitscmp  14088  pc2dvds  14402  prmreclem4  14437  1arith  14445  ramval  14526  imasleval  14938  xpsfrnel  14960  xpsfrnel2  14962  latleeqm1  15709  latnlemlt  15714  latnle  15715  pospropd  15764  ipole  15788  gsumval2a  15906  ghmeqker  16293  gastacos  16348  isslw  16628  slwpss  16632  pgpssslw  16634  fislw  16645  sylow3lem6  16652  dprd2d2  17093  lsslss  17607  lspsnel5  17641  lsmspsn  17730  mplvalOLD  18085  coe1mul2lem1  18308  zndvds  18588  znleval2  18594  elfilspd  18838  islinds2  18848  islindf2  18849  eltg3  19463  leordtvallem1  19711  leordtvallem2  19712  lmbrf  19761  cnrest2  19787  cnprest  19790  cnprest2  19791  cnt0  19847  1stccn  19964  kgencn  20057  xkoccn  20120  qtopcn  20215  ordthmeolem  20302  isfbas  20330  fbunfip  20370  fixufil  20423  fbflim  20477  isflf  20494  cnflf  20503  fclscf  20526  cnfcf  20543  alexsubALTlem4  20550  ismet2  20836  elbl2ps  20892  elbl2  20893  xblpnfps  20898  xblpnf  20899  metcn  21046  txmetcn  21051  blval2  21078  metuel2  21082  dscopn  21094  cnbl0  21281  cnblcld  21282  xrtgioo  21311  mulc1cncf  21409  lmmbrf  21701  iscauf  21719  caucfil  21722  lmclim  21741  lmclimf  21742  evthicc2  21872  ovolfioo  21879  ovolficc  21880  ovoliun  21916  ismbl2  21938  volsup  21966  ioombl1lem4  21971  ismbf  22037  ismbfcn  22038  mbfmulc2lem  22054  mbfmax  22056  mbfposr  22059  ismbf3d  22061  mbfimaopnlem  22062  mbfaddlem  22067  mbfsup  22071  i1fpos  22113  mbfi1fseqlem4  22125  xrge0f  22138  itg2seq  22149  itg2monolem1  22157  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  i1fibl  22214  ditgneg  22261  lhop1  22415  fta1  22704  ulm2  22780  pilem1  22846  sineq0  22914  ellogrn  22947  rlimcnp  23295  wilthlem1  23342  sqff1o  23456  logfaclbnd  23497  bposlem1  23559  lgsdilem  23597  lgsabs1  23609  lgsdchrval  23622  lgsquadlem1  23629  lgsquadlem2  23630  iscgrgd  23905  trgcgrg  23906  tgellng  23940  ltgov  23983  ishlg  23986  israg  24074  islnopp  24113  iscgra  24169  ttgelitv  24186  cusgra3v  24464  wlkdvspthlem  24609  clwlkisclwwlk2  24790  el2spthonot0  24871  el2wlksotot  24882  rusgranumwlkl1  24947  numclwlk1lem2f1  25094  isgrpo2  25199  nmoo0  25706  ubthlem1  25786  ch0pss  26363  pjnorm2  26645  adjval  26809  leop  27042  atcv0eq  27298  reuxfr4d  27389  xppreima  27487  fmptcof2  27502  negelrp  27564  xrdifh  27591  isinftm  27725  ismntoplly  28003  ismntop  28004  brfae  28220  eulerpartlemr  28313  eulerpartlemn  28320  subfacp1lem5  28628  preduz  29280  nofulllem2  29463  heicant  30049  mbfposadd  30062  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  iblabsnclem  30078  ftc1anclem1  30090  ftc1anclem5  30094  areacirclem5  30111  areacirc  30112  filnetlem4  30199  lmclim2  30251  caures  30253  rrnheibor  30333  isdmn3  30471  isnacs2  30638  rabrenfdioph  30748  rmxycomplete  30853  expdioph  30965  pwfi2f1o  31044  islnr3  31064  isdomn3  31164  clim2cf  31656  ismhm0  32493  dfiso2  32568  isrnghmmul  32699  lco0  33028  lindslinindsimp2lem5  33063  snlindsntor  33072  bnj1173  34058  lrelat  34739  lcvbr  34746  lsatcv0eq  34772  ellkr2  34816  lkr0f  34819  lkreqN  34895  opltn0  34915  op1le  34917  leatb  35017  atlltn0  35031  hlrelat5N  35125  hlrelat  35126  cvrval5  35139  cvrexchlem  35143  atcvr0eq  35150  athgt  35180  1cvrco  35196  islpln5  35259  islvol5  35303  elpadd2at2  35531  cdleme0ex2N  35949  cdleme3  35962  cdleme7  35974  cdlemg33e  36436  dochfln0  37204  lcfl1  37219  lcfls1N  37262  lspindp5  37497  taupilem3  37694
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-an 371
  Copyright terms: Public domain W3C validator