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

Theorem biantrud 514
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 510 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 17 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ifptru  1446  cad1  1530  raldifeq  3869  posn  4922  elrnmpt1  5102  fliftf  6233  eroveu  7484  ixpfi2  7898  funsnfsupp  7933  elfi2  7954  dffi3  7971  cfss  8721  wunex2  9189  nn2ge  10662  nnle1eq1  10665  nn0le0eq0  10927  nn0lt10bOLD  11028  ixxun  11680  ioopos  11740  injresinj  12057  xpcogend  13087  cnpart  13352  fz1f1o  13825  nndivdvds  14360  dvdsmultr2  14389  bitsmod  14459  sadadd  14490  sadass  14494  smuval2  14505  smumul  14516  pcmpt  14886  pcmpt2  14887  prmreclem2  14910  prmreclem5  14913  ramcl  15036  mrcidb2  15573  acsfn  15614  fncnvimaeqv  16054  latleeqj1  16358  pgpssslw  17315  subgdmdprd  17716  lssle0  18222  islpir2  18524  islinds3  19441  iscld4  20130  discld  20154  cncnpi  20343  cnprest2  20355  lmss  20363  iscon2  20478  dfcon2  20483  subislly  20545  lly1stc  20560  elptr  20637  txcn  20690  hauseqlcld  20710  xkoinjcn  20751  tsmsres  21207  isxmet2d  21391  xmetgt0  21422  prdsxmetlem  21432  imasdsf1olem  21437  xblss2  21466  stdbdbl  21581  prdsxmslem2  21593  xrtgioo  21873  xrsxmet  21876  cncffvrn  21979  cnmpt2pc  22005  elpi1i  22126  minveclem7  22426  minveclem7OLD  22438  elovolmr  22478  ismbf  22635  mbfmax  22654  itg1val2  22691  mbfi1fseqlem4  22725  itgresr  22785  iblrelem  22797  iblpos  22799  itgfsum  22833  rlimcnp  23940  rlimcnp2  23941  chpchtsum  24196  dchreq  24235  lgsneg  24296  lgsdilem  24299  lgsquadlem2  24332  lmiinv  24883  isusgra0  25123  usgraop  25126  dfconngra1  25448  eupath2lem2  25755  frgra3vlem2  25778  numclwwlk2lem1  25879  minvecolem7  26574  minvecolem7OLD  26584  shle0  27144  mdsl2bi  28025  dmdbr5ati  28124  cdj3lem1  28136  eulerpartlemr  29256  subfacp1lem3  29954  dfres3  30448  hfext  30999  bj-issetwt  31513  poimirlem25  32010  poimirlem26  32011  poimirlem27  32012  mblfinlem3  32024  mblfinlem4  32025  mbfresfi  32032  itg2addnclem  32038  itg2addnc  32041  cover2  32085  heiborlem10  32197  ople0  32798  atlle0  32916  cdlemg10c  34251  cdlemg33c  34320  hdmap14lem13  35496  mrefg3  35595  acsfn1p  36110  radcnvrat  36707  funressnfv  38667  dfdfat2  38671  2ffzoeq  39106  prprrab  39114  isspthonpth-av  39781  dfconngr1  39929
  Copyright terms: Public domain W3C validator