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

Theorem biantrud 494
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  |-  ( ph  ->  ps )
Assertion
Ref Expression
biantrud  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )

Proof of Theorem biantrud
StepHypRef Expression
1 biantrud.1 . 2  |-  ( ph  ->  ps )
2 iba 490 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  posn  4905  elrnmpt1  5078  fliftf  5996  eroveu  6958  ixpfi2  7363  elfi2  7377  dffi3  7394  cantnfrescl  7588  cfss  8101  wunex2  8569  nn2ge  9981  nnle1eq1  9984  nn0le0eq0  10206  nn0lt10b  10292  ixxun  10888  ioopos  10943  injresinj  11155  cnpart  12000  fz1f1o  12459  nndivdvds  12813  dvdsmultr2  12840  bitsmod  12903  sadadd  12934  sadass  12938  smuval2  12949  smumul  12960  pcmpt  13216  pcmpt2  13217  prmreclem2  13240  prmreclem5  13243  ramcl  13352  mrcidb2  13798  acsfn  13839  latleeqj1  14447  pgpssslw  15203  subgdmdprd  15547  lssle0  15981  islpir2  16277  iscld4  17084  discld  17108  cncnpi  17296  cnprest2  17308  lmss  17316  iscon2  17430  dfcon2  17435  subislly  17497  lly1stc  17512  elptr  17558  txcn  17611  hauseqlcld  17631  xkoinjcn  17672  tsmsres  18126  isxmet2d  18310  xmetgt0  18341  prdsxmetlem  18351  imasdsf1olem  18356  xblss2  18385  stdbdbl  18500  prdsxmslem2  18512  xrtgioo  18790  xrsxmet  18793  cncffvrn  18881  cnmpt2pc  18906  elpi1i  19024  minveclem7  19289  elovolmr  19325  ismbf  19475  mbfmax  19494  itg1val2  19529  mbfi1fseqlem4  19563  itgresr  19623  iblrelem  19635  iblpos  19637  itgfsum  19671  rlimcnp  20757  rlimcnp2  20758  chpchtsum  20956  dchreq  20995  lgsneg  21056  lgsdilem  21059  lgsquadlem2  21092  isusgra0  21329  dfconngra1  21611  eupath2lem2  21653  minvecolem7  22338  shle0  22897  mdsl2bi  23779  dmdbr5ati  23878  cdj3lem1  23890  subfacp1lem3  24821  dfres3  25330  hfext  26028  mblfinlem2  26144  mblfinlem3  26145  mbfresfi  26152  itg2addnclem  26155  itg2addnc  26158  cover2  26305  heiborlem10  26419  mrefg3  26652  islinds3  27172  acsfn1p  27375  funressnfv  27859  dfdfat2  27862  frgra3vlem2  28105  ople0  29670  atlle0  29788  cdlemg10c  31121  cdlemg33c  31190  hdmap14lem13  32366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator