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

Theorem biantrud 493
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 489 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 15 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  posn  4840  elrnmpt1  5010  fliftf  5901  eroveu  6841  ixpfi2  7244  elfi2  7258  dffi3  7274  cantnfrescl  7468  cfss  7981  wunex2  8450  nn2ge  9861  nnle1eq1  9864  nn0le0eq0  10086  nn0lt10b  10170  ixxun  10764  ioopos  10818  cnpart  11821  fz1f1o  12280  nndivdvds  12634  dvdsmultr2  12661  bitsmod  12724  sadadd  12755  sadass  12759  smuval2  12770  smumul  12781  pcmpt  13037  pcmpt2  13038  prmreclem2  13061  prmreclem5  13064  ramcl  13173  mrcidb2  13619  acsfn  13660  latleeqj1  14268  pgpssslw  15024  subgdmdprd  15368  lssle0  15806  islpir2  16102  iscld4  16908  discld  16932  cncnpi  17113  cnprest2  17124  lmss  17132  iscon2  17246  dfcon2  17251  subislly  17313  lly1stc  17328  elptr  17374  txcn  17426  hauseqlcld  17446  xkoinjcn  17487  tsmsres  17928  isxmet2d  17994  xmetgt0  18024  prdsxmetlem  18034  imasdsf1olem  18039  xblss2  18060  stdbdbl  18165  prdsxmslem2  18177  xrtgioo  18414  xrsxmet  18417  cncffvrn  18505  cnmpt2pc  18530  elpi1i  18648  minveclem7  18903  elovolmr  18939  ismbf  19089  mbfmax  19108  itg1val2  19143  mbfi1fseqlem4  19177  itgresr  19237  iblrelem  19249  iblpos  19251  itgfsum  19285  rlimcnp  20371  rlimcnp2  20372  chpchtsum  20570  dchreq  20609  lgsneg  20670  lgsdilem  20673  lgsquadlem2  20706  minvecolem7  21576  shle0  22135  mdsl2bi  23017  dmdbr5ati  23116  cdj3lem1  23128  subfacp1lem3  24117  eupath2lem2  24306  dfres3  24674  hfext  25372  itg2addnclem  25492  itg2addnc  25494  cover2  25682  heiborlem10  25867  mrefg3  26106  islinds3  26627  acsfn1p  26830  funressnfv  27316  dfdfat2  27319  injresinj  27465  isusgra0  27531  dfconngra1  27795  frgra3vlem2  27834  ople0  29446  atlle0  29564  cdlemg10c  30897  cdlemg33c  30966  hdmap14lem13  32142
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 177  df-an 360
  Copyright terms: Public domain W3C validator