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  1124  3biant1d  1291  n0moeu  3555  reusv7OLD  4649  reuxfrd  4662  opbrop  4870  opelresiOLD  5069  opelresi  5070  funcnv3  5416  fnssresb  5461  dff1o5  5587  fneqeql2  5741  dffo3  5786  fmptco  5802  fconst4  5856  eloprabga  6060  fnwelem  6358  riota2df  6467  mptelixpg  6996  boxcutc  7002  inficl  7325  wemapso2  7414  cantnfle  7519  bnd2  7710  iscard2  7756  alephinit  7869  kmlem2  7924  cfss  8038  fpwwe2lem9  8407  axgroth2  8594  elnnnn0  10156  znnsub  10215  znn0sub  10216  uzin  10411  xsubge0  10733  supxrre1  10802  ixxun  10825  elfz5  10943  uzsplit  11008  injresinj  11087  hashf1lem1  11591  2shfti  11782  cnpart  11932  sqrneglem  11959  rexuz3  12039  rlim  12176  rlim2  12177  clim2c  12186  ello12  12197  elo12  12208  fsumss  12406  fsumcom2  12445  cvgcmp  12482  bitsmod  12835  bitscmp  12837  pc2dvds  13139  prmreclem4  13174  1arith  13182  ramval  13263  imasleval  13653  xpsfrnel  13675  xpsfrnel2  13677  latleeqm1  14395  latnlemlt  14400  latnle  14401  pospropd  14448  ipole  14471  gsumval2a  14669  ghmeqker  14919  gastacos  14974  isslw  15129  slwpss  15133  pgpssslw  15135  fislw  15146  sylow3lem6  15153  dprd2d2  15489  lsslss  15928  lspsnel5  15962  lsmspsn  16047  coe1mul2lem1  16554  zndvds  16720  znleval2  16726  eltg3  16917  leordtvallem1  17157  leordtvallem2  17158  lmbrf  17207  cnrest2  17231  cnprest  17234  cnprest2  17235  cnt0  17291  1stccn  17406  kgencn  17468  xkoccn  17530  qtopcn  17622  ordthmeolem  17709  isfbas  17737  fbunfip  17777  fixufil  17830  fbflim  17884  isflf  17901  cnflf  17910  fclscf  17933  cnfcf  17950  alexsubALTlem4  17957  ismet2  18111  elbl2  18163  xblpnf  18166  metcn  18302  txmetcn  18307  dscopn  18309  cnbl0  18496  cnblcld  18497  xrtgioo  18525  mulc1cncf  18623  lmmbrf  18903  iscauf  18921  caucfil  18924  lmclim  18943  lmclimf  18944  evthicc2  19035  ovolfioo  19042  ovolficc  19043  ovoliun  19079  ismbl2  19101  volsup  19128  ioombl1lem4  19133  ismbf  19200  ismbfcn  19201  mbfmulc2lem  19217  mbfmax  19219  mbfposr  19222  ismbf3d  19224  mbfimaopnlem  19225  mbfaddlem  19230  mbfsup  19234  i1fpos  19276  mbfi1fseqlem4  19288  xrge0f  19301  itg2seq  19312  itg2monolem1  19320  itg2gt0  19330  itg2cnlem1  19331  itg2cnlem2  19332  i1fibl  19377  ditgneg  19422  lhop1  19576  itgsubst  19611  fta1  19903  ulm2  19979  pilem1  20045  sineq0  20107  ellogrn  20135  rlimcnp  20482  wilthlem1  20529  sqff1o  20643  logfaclbnd  20684  bposlem1  20746  lgsdilem  20784  lgsabs1  20796  lgsdchrval  20809  lgsquadlem1  20816  lgsquadlem2  20817  cusgra3v  21143  isgrpo2  21296  nmoo0  21803  ubthlem1  21883  ch0pss  22458  pjnorm2  22740  adjval  22904  leop  23137  atcv0eq  23393  reuxfr4d  23492  fmptcof2  23600  xrdifh  23665  xpco  23845  blval2  23928  brfae  24183  subfacp1lem5  24439  divelunit  24754  fprodss  24843  preduz  25026  nofulllem2  25183  itg2addnclem  25760  itg2addnclem2  25761  itgaddnclem2  25767  iblabsnclem  25771  areacirclem6  25790  areacirc  25791  filnetlem4  25922  lmclim2  26066  caures  26068  rrnheibor  26152  isdmn3  26290  isnacs2  26372  rabrenfdioph  26488  rmxycomplete  26593  expdioph  26707  elfilspd  26846  pwfi2f1o  26851  islinds2  26874  islindf2  26875  islnr3  26910  isdomn3  27114  wlkdvspthlem  27754  bnj1173  28784  lrelat  29263  lcvbr  29270  lsatcv0eq  29296  ellkr2  29340  lkr0f  29343  lkreqN  29419  opltn0  29439  op1le  29441  leatb  29541  atlltn0  29555  hlrelat5N  29649  hlrelat  29650  cvrval5  29663  cvrexchlem  29667  atcvr0eq  29674  athgt  29704  1cvrco  29720  islpln5  29783  islvol5  29827  elpadd2at2  30055  cdleme0ex2N  30472  cdleme3  30485  cdleme7  30497  cdlemg33e  30958  dochfln0  31726  lcfl1  31741  lcfls1N  31784  lspindp5  32019
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