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 206   ∧ 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 207  df-an 396

This theorem is referenced by:  pm5.3  572  mpbirand  708  3biant1d  1481  elrab3t  3647  reuxfr1d  3710  n0moeu  4313  eldifvsn  4755  xpco  6255  funcnv3  6570  fnssresb  6622  dff1o5  6791  fneqeql2  7001  dffo3  7056  dffo3f  7060  fmptco  7084  fconst4  7170  riota2df  7348  eloprabga  7477  fnwelem  8083  frxp2  8096  xpord2pred  8097  xpord3pred  8104  mptsuppd  8139  mptelixpg  8885  boxcutc  8891  inficl  9340  cantnfle  9592  cantnflem1  9610  ttrclselem2  9647  bnd2  9817  iscard2  9900  alephinit  10017  kmlem2  10074  cfss  10187  fpwwe2lem8  10561  axgroth2  10748  elnnnn0  12456  znnsub  12549  znn0sub  12550  negelrp  12952  xsubge0  13188  divelunit  13422  elfz5  13444  preduz  13578  injresinj  13719  adddivflid  13750  divfl0  13756  hashf1lem1  14390  swrdspsleq  14601  repswsymball  14714  repswsymballbi  14715  2shfti  15015  cnpart  15175  sqrtneglem  15201  rexuz3  15284  rlim  15430  rlim2  15431  clim2c  15440  cvgcmp  15751  bitsmod  16375  bitscmp  16377  pc2dvds  16819  prmreclem4  16859  1arith  16867  imasleval  17474  xpsfrnel  17495  xpsfrnel2  17497  dfiso2  17708  pospropd  18260  latleeqm1  18402  latnlemlt  18407  latnle  18408  ipole  18469  gsumval2a  18622  ismhm0  18727  ghmeqker  19184  gastacos  19251  isslw  19549  slwpss  19553  pgpssslw  19555  fislw  19566  sylow3lem6  19573  dprd2d2  19987  isrnghmmul  20390  isdomn3  20660  lsslss  20924  lsmspsn  21048  zndvds  21516  znleval2  21522  elfilspd  21770  islinds2  21780  islindf2  21781  ismhp3  22097  coe1mul2lem1  22221  eltg3  22918  leordtvallem1  23166  leordtvallem2  23167  lmbrf  23216  cnrest2  23242  xkoccn  23575  hauseqlcld  23602  qtopcn  23670  ordthmeolem  23757  isfbas  23785  fbunfip  23825  fixufil  23878  alexsubALTlem4  24006  ismet2  24289  xblpnfps  24351  xblpnf  24352  blval2  24518  metuel2  24521  dscopn  24529  cnbl0  24729  cnblcld  24730  xrtgioo  24763  mulc1cncf  24866  isclmp  25065  isncvsngp  25117  lmmbrf  25230  iscauf  25248  caucfil  25251  lmclim  25271  evthicc2  25429  volsup  25525  ioombl1lem4  25530  ismbf  25597  ismbfcn  25598  mbfmulc2lem  25616  mbfmax  25618  mbfposr  25621  ismbf3d  25623  mbfimaopnlem  25624  mbfsup  25633  i1fpos  25675  mbfi1fseqlem4  25687  xrge0f  25700  itg2seq  25711  itg2monolem1  25719  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  i1fibl  25777  ditgneg  25826  lhop1  25987  r1pid2  26135  fta1  26284  ulm2  26362  pilem1  26429  sineq0  26501  ellogrn  26536  rlimcnp  26943  wilthlem1  27046  sqff1o  27160  logfaclbnd  27201  bposlem1  27263  lgsdilem  27303  lgsabs1  27315  lgsdchrval  27333  lgsquadlem1  27359  lgsquadlem2  27360  sltssnb  27777  zn0subs  28411  iscgrgd  28597  trgcgrg  28599  ltgov  28681  ishlg  28686  lnhl  28699  israg  28781  islnopp  28823  iscgra  28893  isinag  28922  iseqlg  28951  nbupgrel  29430  isuvtx  29480  iscplgredg  29502  rusgrnumwwlkl1  30056  clwlkclwwlk2  30090  isclwwlknx  30123  clwwlkn1  30128  nmoo0  30879  ubthlem1  30958  ch0pss  31533  pjnorm2  31815  adjval  31978  leop  32211  atcv0eq  32467  xppreima  32735  fmptcof2  32747  xrdifh  32871  hashgt1  32899  isinftm  33275  isunit3  33335  isdrng4  33389  fracerl  33400  dvdsruassoi  33477  dvdsruasso  33478  dvdsrspss  33480  lsmsnorb  33484  ply1degltel  33687  r1pid2OLD  33702  psrbasfsupp  33705  smatrcl  33974  rhmpreimacnlem  34062  ismntop  34204  brfae  34426  eulerpartlemr  34552  eulerpartlemn  34559  reprinrn  34796  reprinfz1  34800  reprdifc  34805  bnj1173  35178  subfacp1lem5  35400  rexxfr3dALT  35855  filnetlem4  36597  bj-clel3gALT  37296  bj-imdirco  37445  taupilem3  37574  topdifinffinlem  37602  finxpsuclem  37652  matunitlindf  37869  poimirlem22  37893  poimirlem26  37897  poimirlem27  37898  heicant  37906  mbfposadd  37918  itg2addnclem  37922  itg2addnclem2  37923  iblabsnclem  37934  ftc1anclem1  37944  ftc1anclem5  37948  areacirclem5  37963  areacirc  37964  lmclim2  38009  caures  38011  rrnheibor  38088  isdmn3  38325  opelvvdif  38515  ralrnmo  38612  raldmqsmo  38614  brxrn  38634  lrelat  39390  lcvbr  39397  lsatcv0eq  39423  ellkr2  39467  lkr0f  39470  lkreqN  39546  opltn0  39566  op1le  39568  leatb  39668  atlltn0  39682  hlrelat5N  39777  hlrelat  39778  cvrval5  39791  cvrexchlem  39795  atcvr0eq  39802  athgt  39832  1cvrco  39848  islpln5  39911  islvol5  39955  elpadd2at2  40183  cdleme0ex2N  40600  cdleme3  40613  cdleme7  40625  cdlemg33e  41086  dochfln0  41853  lcfl1  41868  lcfls1N  41911  lspindp5  42146  isnacs2  43063  rabrenfdioph  43171  rmxycomplete  43274  expdioph  43380  pwfi2f1o  43453  islnr3  43472  sqrtcvallem1  43987  ntrneixb  44451  clim2cf  46008  funressnfv  47403  focofob  47440  oddm1evenALTV  48035  oddp1evenALTV  48036  divgcdoddALTV  48042  lco0  48787  lindslinindsimp2lem5  48822  snlindsntor  48831  elbigo2  48912  affinecomb1  49062  itscnhlinecirc02p  49145  reuxfr1dd  49166  iscnrm3lem1  49293