MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantrud Structured version   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  |-  ( ph  ->  ps )
Assertion
Ref Expression
biantrud  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )

Proof of Theorem biantrud
StepHypRef Expression
1 biantrud.1 . 2  |-  ( ph  ->  ps )
2 iba 503 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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
This theorem is referenced by:  raldifeq  3763  posn  4902  elrnmpt1  5083  fliftf  6003  eroveu  7187  ixpfi2  7601  funsnfsupp  7636  elfi2  7656  dffi3  7673  cantnfrescl  7876  cfss  8426  wunex2  8897  nn2ge  10339  nnle1eq1  10342  nn0le0eq0  10600  nn0lt10b  10698  ixxun  11308  ioopos  11364  injresinj  11631  cnpart  12721  fz1f1o  13179  nndivdvds  13533  dvdsmultr2  13560  bitsmod  13624  sadadd  13655  sadass  13659  smuval2  13670  smumul  13681  pcmpt  13946  pcmpt2  13947  prmreclem2  13970  prmreclem5  13973  ramcl  14082  mrcidb2  14548  acsfn  14589  latleeqj1  15225  pgpssslw  16104  subgdmdprd  16519  lssle0  17008  islpir2  17310  islinds3  18238  iscld4  18644  discld  18668  cncnpi  18857  cnprest2  18869  lmss  18877  iscon2  18993  dfcon2  18998  subislly  19060  lly1stc  19075  elptr  19121  txcn  19174  hauseqlcld  19194  xkoinjcn  19235  tsmsresOLD  19692  tsmsres  19693  isxmet2d  19877  xmetgt0  19908  prdsxmetlem  19918  imasdsf1olem  19923  xblss2  19952  stdbdbl  20067  prdsxmslem2  20079  xrtgioo  20358  xrsxmet  20361  cncffvrn  20449  cnmpt2pc  20475  elpi1i  20593  minveclem7  20897  elovolmr  20934  ismbf  21083  mbfmax  21102  itg1val2  21137  mbfi1fseqlem4  21171  itgresr  21231  iblrelem  21243  iblpos  21245  itgfsum  21279  rlimcnp  22334  rlimcnp2  22335  chpchtsum  22533  dchreq  22572  lgsneg  22633  lgsdilem  22636  lgsquadlem2  22669  isusgra0  23226  dfconngra1  23508  eupath2lem2  23550  minvecolem7  24235  shle0  24796  mdsl2bi  25678  dmdbr5ati  25777  cdj3lem1  25789  eulerpartlemr  26709  subfacp1lem3  27022  dfres3  27520  hfext  28172  mblfinlem3  28383  mblfinlem4  28384  mbfresfi  28391  itg2addnclem  28396  itg2addnc  28399  cover2  28560  heiborlem10  28672  mrefg3  28997  acsfn1p  29509  funressnfv  29987  dfdfat2  29990  2ffzoeq  30167  frgra3vlem2  30546  numclwwlk2lem1  30648  bj-issetwt  32219  ople0  32672  atlle0  32790  cdlemg10c  34123  cdlemg33c  34192  hdmap14lem13  35368
  Copyright terms: Public domain W3C validator