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

Theorem biantrurd 494
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
biantrud.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
biantrurd  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2  |-  ( ph  ->  ps )
2 ibar 490 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
31, 2syl 15 1  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  3anibar  1123  n0moeu  3467  reusv7OLD  4546  reuxfrd  4559  opbrop  4767  opelresiOLD  4966  opelresi  4967  funcnv3  5311  fnssresb  5356  dff1o5  5481  fneqeql2  5634  dffo3  5675  fmptco  5691  fconst4  5736  eloprabga  5934  fnwelem  6230  riota2df  6325  mptelixpg  6853  boxcutc  6859  inficl  7178  wemapso2  7267  cantnfle  7372  bnd2  7563  iscard2  7609  alephinit  7722  kmlem2  7777  cfss  7891  fpwwe2lem9  8260  axgroth2  8447  elnnnn0  10007  znnsub  10064  znn0sub  10065  uzin  10260  xsubge0  10581  supxrre1  10649  ixxun  10672  elfz5  10790  uzsplit  10855  hashf1lem1  11393  2shfti  11575  cnpart  11725  sqrneglem  11752  rexuz3  11832  rlim  11969  rlim2  11970  clim2c  11979  ello12  11990  elo12  12001  fsumss  12198  fsumcom2  12237  cvgcmp  12274  bitsmod  12627  bitscmp  12629  pc2dvds  12931  prmreclem4  12966  1arith  12974  ramval  13055  imasleval  13443  xpsfrnel  13465  xpsfrnel2  13467  latleeqm1  14185  latnlemlt  14190  latnle  14191  pospropd  14238  ipole  14261  gsumval2a  14459  ghmeqker  14709  gastacos  14764  isslw  14919  slwpss  14923  pgpssslw  14925  fislw  14936  sylow3lem6  14943  dprd2d2  15279  lsslss  15718  lspsnel5  15752  lsmspsn  15837  coe1mul2lem1  16344  zndvds  16503  znleval2  16509  eltg3  16700  leordtvallem1  16940  leordtvallem2  16941  lmbrf  16990  cnrest2  17014  cnprest  17017  cnprest2  17018  cnt0  17074  1stccn  17189  kgencn  17251  xkoccn  17313  qtopcn  17405  ordthmeolem  17492  isfbas  17524  fbunfip  17564  fixufil  17617  fbflim  17671  isflf  17688  cnflf  17697  fclscf  17720  cnfcf  17737  alexsubALTlem4  17744  ismet2  17898  elbl2  17950  xblpnf  17953  metcn  18089  txmetcn  18094  dscopn  18096  cnbl0  18283  cnblcld  18284  xrtgioo  18312  mulc1cncf  18409  lmmbrf  18688  iscauf  18706  caucfil  18709  lmclim  18728  lmclimf  18729  evthicc2  18820  ovolfioo  18827  ovolficc  18828  ovoliun  18864  ismbl2  18886  volsup  18913  ioombl1lem4  18918  ismbf  18985  ismbfcn  18986  mbfmulc2lem  19002  mbfmax  19004  mbfposr  19007  ismbf3d  19009  mbfimaopnlem  19010  mbfaddlem  19015  mbfsup  19019  i1fpos  19061  mbfi1fseqlem4  19073  xrge0f  19086  itg2seq  19097  itg2monolem1  19105  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  i1fibl  19162  ditgneg  19207  lhop1  19361  itgsubst  19396  fta1  19688  ulm2  19764  pilem1  19827  sineq0  19889  ellogrn  19917  rlimcnp  20260  wilthlem1  20306  sqff1o  20420  logfaclbnd  20461  bposlem1  20523  lgsdilem  20561  lgsabs1  20573  lgsdchrval  20586  lgsquadlem1  20593  lgsquadlem2  20594  isgrpo2  20864  nmoo0  21369  ubthlem1  21449  ch0pss  22024  pjnorm2  22306  adjval  22470  leop  22703  atcv0eq  22959  reuxfr4d  23139  fmptcof2  23229  xrdifh  23273  subfacp1lem5  23715  divelunit  24080  preduz  24200  nofulllem2  24357  areacirclem6  24930  areacirc  24931  elo  25041  dffprod  25319  conttnf2  25562  filnetlem4  26330  lmclim2  26474  caures  26476  rrnheibor  26561  isdmn3  26699  isnacs2  26781  rabrenfdioph  26897  rmxycomplete  27002  expdioph  27116  elfilspd  27255  pwfi2f1o  27260  islinds2  27283  islindf2  27284  islnr3  27319  isdomn3  27523  bnj1173  29032  lrelat  29204  lcvbr  29211  lsatcv0eq  29237  ellkr2  29281  lkr0f  29284  lkreqN  29360  opltn0  29380  op1le  29382  leatb  29482  atlltn0  29496  hlrelat5N  29590  hlrelat  29591  cvrval5  29604  cvrexchlem  29608  atcvr0eq  29615  athgt  29645  1cvrco  29661  islpln5  29724  islvol5  29768  elpadd2at2  29996  cdleme0ex2N  30413  cdleme3  30426  cdleme7  30438  cdlemg33e  30899  dochfln0  31667  lcfl1  31682  lcfls1N  31725  lspindp5  31960
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