Theorem biantrurd 532

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

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 ⊢ (𝜑 → 𝜓)
2		ibar 528	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 396

This theorem is referenced by:  pm5.3  572  mpbirand  706  3biant1d  1475  elrab3t  3679  reuxfr1d  3743  n0moeu  4352  eldifvsn  4796  xpco  6287  funcnv3  6617  fnssresb  6671  dff1o5  6842  fneqeql2  7050  dffo3  7106  dffo3f  7110  fmptco  7132  fconst4  7220  riota2df  7394  eloprabga  7521  eloprabgaOLD  7522  fnwelem  8128  frxp2  8141  xpord2pred  8142  xpord3pred  8149  mptsuppd  8183  mptelixpg  8943  boxcutc  8949  inficl  9434  cantnfle  9680  cantnflem1  9698  ttrclselem2  9735  bnd2  9902  iscard2  9985  alephinit  10104  kmlem2  10160  cfss  10274  fpwwe2lem8  10647  axgroth2  10834  elnnnn0  12531  znnsub  12624  znn0sub  12625  negelrp  13025  xsubge0  13258  divelunit  13489  elfz5  13511  preduz  13641  injresinj  13771  adddivflid  13801  divfl0  13807  hashf1lem1  14433  hashf1lem1OLD  14434  swrdspsleq  14633  repswsymball  14747  repswsymballbi  14748  2shfti  15045  cnpart  15205  sqrtneglem  15231  rexuz3  15313  rlim  15457  rlim2  15458  clim2c  15467  cvgcmp  15780  bitsmod  16396  bitscmp  16398  pc2dvds  16833  prmreclem4  16873  1arith  16881  imasleval  17508  xpsfrnel  17529  xpsfrnel2  17531  dfiso2  17740  pospropd  18304  latleeqm1  18444  latnlemlt  18449  latnle  18450  ipole  18511  gsumval2a  18630  ismhm0  18732  ghmeqker  19181  gastacos  19245  isslw  19547  slwpss  19551  pgpssslw  19553  fislw  19564  sylow3lem6  19571  dprd2d2  19985  isrnghmmul  20363  lsslss  20827  lsmspsn  20951  zndvds  21463  znleval2  21469  elfilspd  21717  islinds2  21727  islindf2  21728  ismhp3  22045  coe1mul2lem1  22160  eltg3  22839  leordtvallem1  23088  leordtvallem2  23089  lmbrf  23138  cnrest2  23164  xkoccn  23497  hauseqlcld  23524  qtopcn  23592  ordthmeolem  23679  isfbas  23707  fbunfip  23747  fixufil  23800  alexsubALTlem4  23928  ismet2  24213  xblpnfps  24275  xblpnf  24276  blval2  24445  metuel2  24448  dscopn  24456  cnbl0  24664  cnblcld  24665  xrtgioo  24696  mulc1cncf  24799  isclmp  24998  isncvsngp  25051  lmmbrf  25164  iscauf  25182  caucfil  25185  lmclim  25205  evthicc2  25363  volsup  25459  ioombl1lem4  25464  ismbf  25531  ismbfcn  25532  mbfmulc2lem  25550  mbfmax  25552  mbfposr  25555  ismbf3d  25557  mbfimaopnlem  25558  mbfsup  25567  i1fpos  25610  mbfi1fseqlem4  25622  xrge0f  25635  itg2seq  25646  itg2monolem1  25654  itg2gt0  25664  itg2cnlem1  25665  itg2cnlem2  25666  i1fibl  25711  ditgneg  25760  lhop1  25921  fta1  26217  ulm2  26295  pilem1  26362  sineq0  26432  ellogrn  26467  rlimcnp  26871  wilthlem1  26974  sqff1o  27088  logfaclbnd  27129  bposlem1  27191  lgsdilem  27231  lgsabs1  27243  lgsdchrval  27261  lgsquadlem1  27287  lgsquadlem2  27288  iscgrgd  28291  trgcgrg  28293  ltgov  28375  ishlg  28380  lnhl  28393  israg  28475  islnopp  28517  iscgra  28587  isinag  28616  iseqlg  28645  nbupgrel  29132  isuvtx  29182  iscplgredg  29204  rusgrnumwwlkl1  29753  clwlkclwwlk2  29787  isclwwlknx  29820  clwwlkn1  29825  nmoo0  30575  ubthlem1  30654  ch0pss  31229  pjnorm2  31511  adjval  31674  leop  31907  atcv0eq  32163  xppreima  32402  fmptcof2  32413  xrdifh  32519  hashgt1  32548  isinftm  32854  isdrng4  32919  dvdsruassoi  33015  dvdsruasso  33016  dvdsrspss  33017  lsmsnorb  33027  ply1degltel  33184  r1pid2  33198  smatrcl  33320  rhmpreimacnlem  33408  ismntop  33550  brfae  33790  eulerpartlemr  33917  eulerpartlemn  33924  reprinrn  34173  reprinfz1  34177  reprdifc  34182  bnj1173  34556  subfacp1lem5  34717  filnetlem4  35788  bj-clel3gALT  36450  bj-imdirco  36592  taupilem3  36721  topdifinffinlem  36749  finxpsuclem  36799  matunitlindf  37013  poimirlem22  37037  poimirlem26  37041  poimirlem27  37042  heicant  37050  mbfposadd  37062  itg2addnclem  37066  itg2addnclem2  37067  iblabsnclem  37078  ftc1anclem1  37088  ftc1anclem5  37092  areacirclem5  37107  areacirc  37108  lmclim2  37153  caures  37155  rrnheibor  37232  isdmn3  37469  opelvvdif  37653  brxrn  37770  lrelat  38410  lcvbr  38417  lsatcv0eq  38443  ellkr2  38487  lkr0f  38490  lkreqN  38566  opltn0  38586  op1le  38588  leatb  38688  atlltn0  38702  hlrelat5N  38798  hlrelat  38799  cvrval5  38812  cvrexchlem  38816  atcvr0eq  38823  athgt  38853  1cvrco  38869  islpln5  38932  islvol5  38976  elpadd2at2  39204  cdleme0ex2N  39621  cdleme3  39634  cdleme7  39646  cdlemg33e  40107  dochfln0  40874  lcfl1  40889  lcfls1N  40932  lspindp5  41167  isnacs2  42038  rabrenfdioph  42146  rmxycomplete  42250  expdioph  42356  pwfi2f1o  42432  islnr3  42451  isdomn3  42539  sqrtcvallem1  42974  ntrneixb  43438  clim2cf  44951  funressnfv  46338  focofob  46373  oddm1evenALTV  46928  oddp1evenALTV  46929  divgcdoddALTV  46935  lco0  47408  lindslinindsimp2lem5  47443  snlindsntor  47452  elbigo2  47538  affinecomb1  47688  itscnhlinecirc02p  47771  iscnrm3lem1  47865