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

Theorem biantrud 507
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
Hypothesis
Ref Expression
biantrud.1
Assertion
Ref Expression
biantrud

Proof of Theorem biantrud
StepHypRef Expression
1 biantrud.1 . 2
2 iba 503 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  raldifeq  3917  posn  5073  elrnmpt1  5256  fliftf  6213  eroveu  7425  ixpfi2  7838  funsnfsupp  7873  elfi2  7894  dffi3  7911  cfss  8666  wunex2  9137  nn2ge  10586  nnle1eq1  10589  nn0le0eq0  10849  nn0lt10bOLD  10951  ixxun  11574  ioopos  11630  injresinj  11926  cnpart  13073  fz1f1o  13532  nndivdvds  13992  dvdsmultr2  14021  bitsmod  14086  sadadd  14117  sadass  14121  smuval2  14132  smumul  14143  pcmpt  14411  pcmpt2  14412  prmreclem2  14435  prmreclem5  14438  ramcl  14547  mrcidb2  15015  acsfn  15056  latleeqj1  15693  pgpssslw  16634  subgdmdprd  17081  lssle0  17596  islpir2  17899  islinds3  18869  iscld4  19566  discld  19590  cncnpi  19779  cnprest2  19791  lmss  19799  iscon2  19915  dfcon2  19920  subislly  19982  lly1stc  19997  elptr  20074  txcn  20127  hauseqlcld  20147  xkoinjcn  20188  tsmsresOLD  20645  tsmsres  20646  isxmet2d  20830  xmetgt0  20861  prdsxmetlem  20871  imasdsf1olem  20876  xblss2  20905  stdbdbl  21020  prdsxmslem2  21032  xrtgioo  21311  xrsxmet  21314  cncffvrn  21402  cnmpt2pc  21428  elpi1i  21546  minveclem7  21850  elovolmr  21887  ismbf  22037  mbfmax  22056  itg1val2  22091  mbfi1fseqlem4  22125  itgresr  22185  iblrelem  22197  iblpos  22199  itgfsum  22233  rlimcnp  23295  rlimcnp2  23296  chpchtsum  23494  dchreq  23533  lgsneg  23594  lgsdilem  23597  lgsquadlem2  23630  lmiinv  24158  isusgra0  24347  usgraop  24350  dfconngra1  24671  eupath2lem2  24978  frgra3vlem2  25001  numclwwlk2lem1  25102  minvecolem7  25799  shle0  26360  mdsl2bi  27242  dmdbr5ati  27341  cdj3lem1  27353  eulerpartlemr  28313  subfacp1lem3  28626  dfres3  29188  hfext  29840  mblfinlem3  30053  mblfinlem4  30054  mbfresfi  30061  itg2addnclem  30066  itg2addnc  30069  cover2  30204  heiborlem10  30316  mrefg3  30640  acsfn1p  31148  radcnvrat  31195  funressnfv  32213  dfdfat2  32216  2ffzoeq  32341  fncnvimaeqv  32626  bj-issetwt  34435  ople0  34912  atlle0  35030  cdlemg10c  36365  cdlemg33c  36434  hdmap14lem13  37610  xpcogend  37773
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