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

Theorem biantrurd 534
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 (𝜑𝜓)
Assertion
Ref Expression
biantrurd (𝜑 → (𝜒 ↔ (𝜓𝜒)))

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2 (𝜑𝜓)
2 ibar 530 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  pm5.3  574  mpbirand  706  3biant1d  1479  elrab3t  3645  reuxfr1d  3709  n0moeu  4317  eldifvsn  4758  xpco  6242  funcnv3  6572  fnssresb  6624  dff1o5  6794  fneqeql2  6998  dffo3  7053  fmptco  7076  fconst4  7165  riota2df  7338  eloprabga  7465  eloprabgaOLD  7466  fnwelem  8064  frxp2  8077  xpord2pred  8078  xpord3pred  8085  mptsuppd  8119  mptelixpg  8874  boxcutc  8880  inficl  9362  cantnfle  9608  cantnflem1  9626  ttrclselem2  9663  bnd2  9830  iscard2  9913  alephinit  10032  kmlem2  10088  cfss  10202  fpwwe2lem8  10575  axgroth2  10762  elnnnn0  12457  znnsub  12550  znn0sub  12551  negelrp  12949  xsubge0  13181  divelunit  13412  elfz5  13434  preduz  13564  injresinj  13694  adddivflid  13724  divfl0  13730  hashf1lem1  14354  hashf1lem1OLD  14355  swrdspsleq  14554  repswsymball  14668  repswsymballbi  14669  2shfti  14966  cnpart  15126  sqrtneglem  15152  rexuz3  15234  rlim  15378  rlim2  15379  clim2c  15388  cvgcmp  15702  bitsmod  16317  bitscmp  16319  pc2dvds  16752  prmreclem4  16792  1arith  16800  imasleval  17424  xpsfrnel  17445  xpsfrnel2  17447  dfiso2  17656  pospropd  18217  latleeqm1  18357  latnlemlt  18362  latnle  18363  ipole  18424  gsumval2a  18541  ghmeqker  19036  gastacos  19091  isslw  19391  slwpss  19395  pgpssslw  19397  fislw  19408  sylow3lem6  19415  dprd2d2  19824  lsslss  20425  lsmspsn  20548  zndvds  20959  znleval2  20965  elfilspd  21212  islinds2  21222  islindf2  21223  ismhp3  21536  coe1mul2lem1  21641  eltg3  22315  leordtvallem1  22564  leordtvallem2  22565  lmbrf  22614  cnrest2  22640  xkoccn  22973  hauseqlcld  23000  qtopcn  23068  ordthmeolem  23155  isfbas  23183  fbunfip  23223  fixufil  23276  alexsubALTlem4  23404  ismet2  23689  xblpnfps  23751  xblpnf  23752  blval2  23921  metuel2  23924  dscopn  23932  cnbl0  24140  cnblcld  24141  xrtgioo  24172  mulc1cncf  24271  isclmp  24463  isncvsngp  24516  lmmbrf  24629  iscauf  24647  caucfil  24650  lmclim  24670  evthicc2  24827  volsup  24923  ioombl1lem4  24928  ismbf  24995  ismbfcn  24996  mbfmulc2lem  25014  mbfmax  25016  mbfposr  25019  ismbf3d  25021  mbfimaopnlem  25022  mbfsup  25031  i1fpos  25074  mbfi1fseqlem4  25086  xrge0f  25099  itg2seq  25110  itg2monolem1  25118  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  i1fibl  25175  ditgneg  25224  lhop1  25381  fta1  25671  ulm2  25747  pilem1  25813  sineq0  25883  ellogrn  25918  rlimcnp  26318  wilthlem1  26420  sqff1o  26534  logfaclbnd  26573  bposlem1  26635  lgsdilem  26675  lgsabs1  26687  lgsdchrval  26705  lgsquadlem1  26731  lgsquadlem2  26732  iscgrgd  27458  trgcgrg  27460  ltgov  27542  ishlg  27547  lnhl  27560  israg  27642  islnopp  27684  iscgra  27754  isinag  27783  iseqlg  27812  nbupgrel  28296  isuvtx  28346  iscplgredg  28368  rusgrnumwwlkl1  28916  clwlkclwwlk2  28950  isclwwlknx  28983  clwwlkn1  28988  nmoo0  29736  ubthlem1  29815  ch0pss  30390  pjnorm2  30672  adjval  30835  leop  31068  atcv0eq  31324  xppreima  31565  fmptcof2  31576  xrdifh  31686  hashgt1  31713  isinftm  32020  lsmsnorb  32175  smatrcl  32380  rhmpreimacnlem  32468  ismntop  32610  brfae  32850  eulerpartlemr  32977  eulerpartlemn  32984  reprinrn  33234  reprinfz1  33238  reprdifc  33243  bnj1173  33617  subfacp1lem5  33781  filnetlem4  34856  bj-clel3gALT  35522  bj-imdirco  35664  taupilem3  35793  topdifinffinlem  35821  finxpsuclem  35871  matunitlindf  36079  poimirlem22  36103  poimirlem26  36107  poimirlem27  36108  heicant  36116  mbfposadd  36128  itg2addnclem  36132  itg2addnclem2  36133  iblabsnclem  36144  ftc1anclem1  36154  ftc1anclem5  36158  areacirclem5  36173  areacirc  36174  lmclim2  36220  caures  36222  rrnheibor  36299  isdmn3  36536  opelvvdif  36722  brxrn  36839  lrelat  37479  lcvbr  37486  lsatcv0eq  37512  ellkr2  37556  lkr0f  37559  lkreqN  37635  opltn0  37655  op1le  37657  leatb  37757  atlltn0  37771  hlrelat5N  37867  hlrelat  37868  cvrval5  37881  cvrexchlem  37885  atcvr0eq  37892  athgt  37922  1cvrco  37938  islpln5  38001  islvol5  38045  elpadd2at2  38273  cdleme0ex2N  38690  cdleme3  38703  cdleme7  38715  cdlemg33e  39176  dochfln0  39943  lcfl1  39958  lcfls1N  40001  lspindp5  40236  isnacs2  41032  rabrenfdioph  41140  rmxycomplete  41244  expdioph  41350  pwfi2f1o  41426  islnr3  41445  isdomn3  41534  sqrtcvallem1  41910  ntrneixb  42374  dffo3f  43405  clim2cf  43898  funressnfv  45284  focofob  45319  oddm1evenALTV  45874  oddp1evenALTV  45875  divgcdoddALTV  45881  ismhm0  46106  isrnghmmul  46198  lco0  46515  lindslinindsimp2lem5  46550  snlindsntor  46559  elbigo2  46645  affinecomb1  46795  itscnhlinecirc02p  46878  iscnrm3lem1  46973
  Copyright terms: Public domain W3C validator