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

Theorem biantrurd 495
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 491 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  3anibar  1125  3biant1d  1292  n0moeu  3600  reusv7OLD  4694  reuxfrd  4707  opbrop  4914  opelresiOLD  5116  opelresi  5117  xpco  5373  funcnv3  5471  fnssresb  5516  dff1o5  5642  fneqeql2  5798  dffo3  5843  fmptco  5860  fconst4  5915  eloprabga  6119  fnwelem  6420  riota2df  6529  mptelixpg  7058  boxcutc  7064  inficl  7388  wemapso2  7477  cantnfle  7582  bnd2  7773  iscard2  7819  alephinit  7932  kmlem2  7987  cfss  8101  fpwwe2lem9  8469  axgroth2  8656  elnnnn0  10219  znnsub  10278  znn0sub  10279  uzin  10474  xsubge0  10796  supxrre1  10865  ixxun  10888  elfz5  11007  uzsplit  11073  injresinj  11155  hashf1lem1  11659  2shfti  11850  cnpart  12000  sqrneglem  12027  rexuz3  12107  rlim  12244  rlim2  12245  clim2c  12254  ello12  12265  elo12  12276  fsumss  12474  fsumcom2  12513  cvgcmp  12550  bitsmod  12903  bitscmp  12905  pc2dvds  13207  prmreclem4  13242  1arith  13250  ramval  13331  imasleval  13721  xpsfrnel  13743  xpsfrnel2  13745  latleeqm1  14463  latnlemlt  14468  latnle  14469  pospropd  14516  ipole  14539  gsumval2a  14737  ghmeqker  14987  gastacos  15042  isslw  15197  slwpss  15201  pgpssslw  15203  fislw  15214  sylow3lem6  15221  dprd2d2  15557  lsslss  15992  lspsnel5  16026  lsmspsn  16111  coe1mul2lem1  16615  zndvds  16785  znleval2  16791  eltg3  16982  leordtvallem1  17228  leordtvallem2  17229  lmbrf  17278  cnrest2  17304  cnprest  17307  cnprest2  17308  cnt0  17364  1stccn  17479  kgencn  17541  xkoccn  17604  qtopcn  17699  ordthmeolem  17786  isfbas  17814  fbunfip  17854  fixufil  17907  fbflim  17961  isflf  17978  cnflf  17987  fclscf  18010  cnfcf  18027  alexsubALTlem4  18034  ismet2  18316  elbl2ps  18372  elbl2  18373  xblpnfps  18378  xblpnf  18379  metcn  18526  txmetcn  18531  blval2  18558  metuel2  18562  dscopn  18574  cnbl0  18761  cnblcld  18762  xrtgioo  18790  mulc1cncf  18888  lmmbrf  19168  iscauf  19186  caucfil  19189  lmclim  19208  lmclimf  19209  evthicc2  19310  ovolfioo  19317  ovolficc  19318  ovoliun  19354  ismbl2  19376  volsup  19403  ioombl1lem4  19408  ismbf  19475  ismbfcn  19476  mbfmulc2lem  19492  mbfmax  19494  mbfposr  19497  ismbf3d  19499  mbfimaopnlem  19500  mbfaddlem  19505  mbfsup  19509  i1fpos  19551  mbfi1fseqlem4  19563  xrge0f  19576  itg2seq  19587  itg2monolem1  19595  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  i1fibl  19652  ditgneg  19697  lhop1  19851  fta1  20178  ulm2  20254  pilem1  20320  sineq0  20382  ellogrn  20410  rlimcnp  20757  wilthlem1  20804  sqff1o  20918  logfaclbnd  20959  bposlem1  21021  lgsdilem  21059  lgsabs1  21071  lgsdchrval  21084  lgsquadlem1  21091  lgsquadlem2  21092  cusgra3v  21426  wlkdvspthlem  21560  isgrpo2  21738  nmoo0  22245  ubthlem1  22325  ch0pss  22900  pjnorm2  23182  adjval  23346  leop  23579  atcv0eq  23835  reuxfr4d  23930  xppreima  24012  fmptcof2  24029  xrdifh  24096  isinftm  24204  brfae  24552  subfacp1lem5  24823  divelunit  25138  fprodss  25227  fprodcom2  25261  preduz  25414  nofulllem2  25571  mbfposadd  26153  itg2addnclem  26155  itg2addnclem2  26156  iblabsnclem  26167  areacirclem6  26186  areacirc  26187  filnetlem4  26300  lmclim2  26354  caures  26356  rrnheibor  26436  isdmn3  26574  isnacs2  26650  rabrenfdioph  26765  rmxycomplete  26870  expdioph  26984  elfilspd  27123  pwfi2f1o  27128  islinds2  27151  islindf2  27152  islnr3  27187  isdomn3  27391  el2spthonot0  28068  el2wlksotot  28079  bnj1173  29077  lrelat  29497  lcvbr  29504  lsatcv0eq  29530  ellkr2  29574  lkr0f  29577  lkreqN  29653  opltn0  29673  op1le  29675  leatb  29775  atlltn0  29789  hlrelat5N  29883  hlrelat  29884  cvrval5  29897  cvrexchlem  29901  atcvr0eq  29908  athgt  29938  1cvrco  29954  islpln5  30017  islvol5  30061  elpadd2at2  30289  cdleme0ex2N  30706  cdleme3  30719  cdleme7  30731  cdlemg33e  31192  dochfln0  31960  lcfl1  31975  lcfls1N  32018  lspindp5  32253
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 178  df-an 361
  Copyright terms: Public domain W3C validator