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

Theorem biantrurd 496
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 492 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  3anibar  1126  3biant1d  1293  n0moeu  3641  reusv7OLD  4736  reuxfrd  4749  opbrop  4956  opelresiOLD  5158  opelresi  5159  xpco  5415  funcnv3  5513  fnssresb  5558  dff1o5  5684  fneqeql2  5840  dffo3  5885  fmptco  5902  fconst4  5957  eloprabga  6161  fnwelem  6462  riota2df  6571  mptelixpg  7100  boxcutc  7106  inficl  7431  wemapso2  7522  cantnfle  7627  bnd2  7818  iscard2  7864  alephinit  7977  kmlem2  8032  cfss  8146  fpwwe2lem9  8514  axgroth2  8701  elnnnn0  10264  znnsub  10323  znn0sub  10324  uzin  10519  xsubge0  10841  supxrre1  10910  ixxun  10933  elfz5  11052  uzsplit  11119  injresinj  11201  hashf1lem1  11705  2shfti  11896  cnpart  12046  sqrneglem  12073  rexuz3  12153  rlim  12290  rlim2  12291  clim2c  12300  ello12  12311  elo12  12322  fsumss  12520  fsumcom2  12559  cvgcmp  12596  bitsmod  12949  bitscmp  12951  pc2dvds  13253  prmreclem4  13288  1arith  13296  ramval  13377  imasleval  13767  xpsfrnel  13789  xpsfrnel2  13791  latleeqm1  14509  latnlemlt  14514  latnle  14515  pospropd  14562  ipole  14585  gsumval2a  14783  ghmeqker  15033  gastacos  15088  isslw  15243  slwpss  15247  pgpssslw  15249  fislw  15260  sylow3lem6  15267  dprd2d2  15603  lsslss  16038  lspsnel5  16072  lsmspsn  16157  coe1mul2lem1  16661  zndvds  16831  znleval2  16837  eltg3  17028  leordtvallem1  17275  leordtvallem2  17276  lmbrf  17325  cnrest2  17351  cnprest  17354  cnprest2  17355  cnt0  17411  1stccn  17527  kgencn  17589  xkoccn  17652  qtopcn  17747  ordthmeolem  17834  isfbas  17862  fbunfip  17902  fixufil  17955  fbflim  18009  isflf  18026  cnflf  18035  fclscf  18058  cnfcf  18075  alexsubALTlem4  18082  ismet2  18364  elbl2ps  18420  elbl2  18421  xblpnfps  18426  xblpnf  18427  metcn  18574  txmetcn  18579  blval2  18606  metuel2  18610  dscopn  18622  cnbl0  18809  cnblcld  18810  xrtgioo  18838  mulc1cncf  18936  lmmbrf  19216  iscauf  19234  caucfil  19237  lmclim  19256  lmclimf  19257  evthicc2  19358  ovolfioo  19365  ovolficc  19366  ovoliun  19402  ismbl2  19424  volsup  19451  ioombl1lem4  19456  ismbf  19523  ismbfcn  19524  mbfmulc2lem  19540  mbfmax  19542  mbfposr  19545  ismbf3d  19547  mbfimaopnlem  19548  mbfaddlem  19553  mbfsup  19557  i1fpos  19599  mbfi1fseqlem4  19611  xrge0f  19624  itg2seq  19635  itg2monolem1  19643  itg2gt0  19653  itg2cnlem1  19654  itg2cnlem2  19655  i1fibl  19700  ditgneg  19745  lhop1  19899  fta1  20226  ulm2  20302  pilem1  20368  sineq0  20430  ellogrn  20458  rlimcnp  20805  wilthlem1  20852  sqff1o  20966  logfaclbnd  21007  bposlem1  21069  lgsdilem  21107  lgsabs1  21119  lgsdchrval  21132  lgsquadlem1  21139  lgsquadlem2  21140  cusgra3v  21474  wlkdvspthlem  21608  isgrpo2  21786  nmoo0  22293  ubthlem1  22373  ch0pss  22948  pjnorm2  23230  adjval  23394  leop  23627  atcv0eq  23883  reuxfr4d  23978  xppreima  24060  fmptcof2  24077  xrdifh  24144  isinftm  24252  brfae  24600  subfacp1lem5  24871  divelunit  25186  fprodss  25275  fprodcom2  25309  preduz  25476  nofulllem2  25659  mbfposadd  26255  itg2addnclem  26257  itg2addnclem2  26258  iblabsnclem  26269  ftc1anclem1  26281  ftc1anclem5  26285  areacirclem5  26297  areacirc  26298  filnetlem4  26411  lmclim2  26465  caures  26467  rrnheibor  26547  isdmn3  26685  isnacs2  26761  rabrenfdioph  26876  rmxycomplete  26981  expdioph  27095  elfilspd  27233  pwfi2f1o  27238  islinds2  27261  islindf2  27262  islnr3  27297  isdomn3  27501  el2spthonot0  28339  el2wlksotot  28350  bnj1173  29372  lrelat  29813  lcvbr  29820  lsatcv0eq  29846  ellkr2  29890  lkr0f  29893  lkreqN  29969  opltn0  29989  op1le  29991  leatb  30091  atlltn0  30105  hlrelat5N  30199  hlrelat  30200  cvrval5  30213  cvrexchlem  30217  atcvr0eq  30224  athgt  30254  1cvrco  30270  islpln5  30333  islvol5  30377  elpadd2at2  30605  cdleme0ex2N  31022  cdleme3  31035  cdleme7  31047  cdlemg33e  31508  dochfln0  32276  lcfl1  32291  lcfls1N  32334  lspindp5  32569
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 179  df-an 362
  Copyright terms: Public domain W3C validator