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  4758  elrnmpt1  4928  fliftf  5814  eroveu  6753  ixpfi2  7154  elfi2  7168  dffi3  7184  cantnfrescl  7378  cfss  7891  wunex2  8360  nn2ge  9771  nnle1eq1  9774  nn0le0eq0  9994  nn0lt10b  10078  ixxun  10672  ioopos  10726  cnpart  11725  fz1f1o  12183  nndivdvds  12537  dvdsmultr2  12564  bitsmod  12627  sadadd  12658  sadass  12662  smuval2  12673  smumul  12684  pcmpt  12940  pcmpt2  12941  prmreclem2  12964  prmreclem5  12967  ramcl  13076  mrcidb2  13520  acsfn  13561  latleeqj1  14169  pgpssslw  14925  subgdmdprd  15269  lssle0  15707  islpir2  16003  iscld4  16802  discld  16826  cncnpi  17007  cnprest2  17018  lmss  17026  iscon2  17140  dfcon2  17145  subislly  17207  lly1stc  17222  elptr  17268  txcn  17320  hauseqlcld  17340  xkoinjcn  17381  tsmsres  17826  isxmet2d  17892  xmetgt0  17922  prdsxmetlem  17932  imasdsf1olem  17937  xblss2  17958  stdbdbl  18063  prdsxmslem2  18075  xrtgioo  18312  xrsxmet  18315  cncffvrn  18402  cnmpt2pc  18426  elpi1i  18544  minveclem7  18799  elovolmr  18835  ismbf  18985  mbfmax  19004  itg1val2  19039  mbfi1fseqlem4  19073  itgresr  19133  iblrelem  19145  iblpos  19147  itgfsum  19181  rlimcnp  20260  rlimcnp2  20261  chpchtsum  20458  dchreq  20497  lgsneg  20558  lgsdilem  20561  lgsquadlem2  20594  minvecolem7  21462  shle0  22021  mdsl2bi  22903  dmdbr5ati  23002  cdj3lem1  23014  subfacp1lem3  23713  eupath2lem2  23902  dfres3  24116  hfext  24813  cmp2morp  25958  cover2  26358  heiborlem10  26544  mrefg3  26783  islinds3  27304  acsfn1p  27507  funressnfv  27991  dfdfat2  27994  isusgra0  28106  frgra3vlem2  28179  ople0  29377  atlle0  29495  cdlemg10c  30828  cdlemg33c  30897  hdmap14lem13  32073
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