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  707  3biant1d  1480  elrab3t  3642  reuxfr1d  3705  n0moeu  4308  eldifvsn  4750  xpco  6244  funcnv3  6559  fnssresb  6611  dff1o5  6780  fneqeql2  6989  dffo3  7044  dffo3f  7048  fmptco  7071  fconst4  7157  riota2df  7335  eloprabga  7464  fnwelem  8070  frxp2  8083  xpord2pred  8084  xpord3pred  8091  mptsuppd  8126  mptelixpg  8869  boxcutc  8875  inficl  9320  cantnfle  9572  cantnflem1  9590  ttrclselem2  9627  bnd2  9797  iscard2  9880  alephinit  9997  kmlem2  10054  cfss  10167  fpwwe2lem8  10540  axgroth2  10727  elnnnn0  12435  znnsub  12528  znn0sub  12529  negelrp  12931  xsubge0  13167  divelunit  13401  elfz5  13423  preduz  13557  injresinj  13698  adddivflid  13729  divfl0  13735  hashf1lem1  14369  swrdspsleq  14580  repswsymball  14693  repswsymballbi  14694  2shfti  14994  cnpart  15154  sqrtneglem  15180  rexuz3  15263  rlim  15409  rlim2  15410  clim2c  15419  cvgcmp  15730  bitsmod  16354  bitscmp  16356  pc2dvds  16798  prmreclem4  16838  1arith  16846  imasleval  17453  xpsfrnel  17474  xpsfrnel2  17476  dfiso2  17687  pospropd  18239  latleeqm1  18381  latnlemlt  18386  latnle  18387  ipole  18448  gsumval2a  18601  ismhm0  18706  ghmeqker  19163  gastacos  19230  isslw  19528  slwpss  19532  pgpssslw  19534  fislw  19545  sylow3lem6  19552  dprd2d2  19966  isrnghmmul  20369  isdomn3  20639  lsslss  20903  lsmspsn  21027  zndvds  21495  znleval2  21501  elfilspd  21749  islinds2  21759  islindf2  21760  ismhp3  22076  coe1mul2lem1  22200  eltg3  22897  leordtvallem1  23145  leordtvallem2  23146  lmbrf  23195  cnrest2  23221  xkoccn  23554  hauseqlcld  23581  qtopcn  23649  ordthmeolem  23736  isfbas  23764  fbunfip  23804  fixufil  23857  alexsubALTlem4  23985  ismet2  24268  xblpnfps  24330  xblpnf  24331  blval2  24497  metuel2  24500  dscopn  24508  cnbl0  24708  cnblcld  24709  xrtgioo  24742  mulc1cncf  24845  isclmp  25044  isncvsngp  25096  lmmbrf  25209  iscauf  25227  caucfil  25230  lmclim  25250  evthicc2  25408  volsup  25504  ioombl1lem4  25509  ismbf  25576  ismbfcn  25577  mbfmulc2lem  25595  mbfmax  25597  mbfposr  25600  ismbf3d  25602  mbfimaopnlem  25603  mbfsup  25612  i1fpos  25654  mbfi1fseqlem4  25666  xrge0f  25679  itg2seq  25690  itg2monolem1  25698  itg2gt0  25708  itg2cnlem1  25709  itg2cnlem2  25710  i1fibl  25756  ditgneg  25805  lhop1  25966  r1pid2  26114  fta1  26263  ulm2  26341  pilem1  26408  sineq0  26480  ellogrn  26515  rlimcnp  26922  wilthlem1  27025  sqff1o  27139  logfaclbnd  27180  bposlem1  27242  lgsdilem  27282  lgsabs1  27294  lgsdchrval  27312  lgsquadlem1  27338  lgsquadlem2  27339  ssltsnb  27752  zn0subs  28347  iscgrgd  28511  trgcgrg  28513  ltgov  28595  ishlg  28600  lnhl  28613  israg  28695  islnopp  28737  iscgra  28807  isinag  28836  iseqlg  28865  nbupgrel  29344  isuvtx  29394  iscplgredg  29416  rusgrnumwwlkl1  29970  clwlkclwwlk2  30004  isclwwlknx  30037  clwwlkn1  30042  nmoo0  30792  ubthlem1  30871  ch0pss  31446  pjnorm2  31728  adjval  31891  leop  32124  atcv0eq  32380  xppreima  32649  fmptcof2  32661  xrdifh  32788  hashgt1  32816  isinftm  33191  isunit3  33251  isdrng4  33305  fracerl  33316  dvdsruassoi  33393  dvdsruasso  33394  dvdsrspss  33396  lsmsnorb  33400  ply1degltel  33603  r1pid2OLD  33618  psrbasfsupp  33621  smatrcl  33881  rhmpreimacnlem  33969  ismntop  34111  brfae  34333  eulerpartlemr  34459  eulerpartlemn  34466  reprinrn  34703  reprinfz1  34707  reprdifc  34712  bnj1173  35086  subfacp1lem5  35300  rexxfr3dALT  35755  filnetlem4  36497  bj-clel3gALT  37165  bj-imdirco  37307  taupilem3  37436  topdifinffinlem  37464  finxpsuclem  37514  matunitlindf  37731  poimirlem22  37755  poimirlem26  37759  poimirlem27  37760  heicant  37768  mbfposadd  37780  itg2addnclem  37784  itg2addnclem2  37785  iblabsnclem  37796  ftc1anclem1  37806  ftc1anclem5  37810  areacirclem5  37825  areacirc  37826  lmclim2  37871  caures  37873  rrnheibor  37950  isdmn3  38187  opelvvdif  38369  brxrn  38480  lrelat  39186  lcvbr  39193  lsatcv0eq  39219  ellkr2  39263  lkr0f  39266  lkreqN  39342  opltn0  39362  op1le  39364  leatb  39464  atlltn0  39478  hlrelat5N  39573  hlrelat  39574  cvrval5  39587  cvrexchlem  39591  atcvr0eq  39598  athgt  39628  1cvrco  39644  islpln5  39707  islvol5  39751  elpadd2at2  39979  cdleme0ex2N  40396  cdleme3  40409  cdleme7  40421  cdlemg33e  40882  dochfln0  41649  lcfl1  41664  lcfls1N  41707  lspindp5  41942  isnacs2  42863  rabrenfdioph  42971  rmxycomplete  43074  expdioph  43180  pwfi2f1o  43253  islnr3  43272  sqrtcvallem1  43788  ntrneixb  44252  clim2cf  45810  funressnfv  47205  focofob  47242  oddm1evenALTV  47837  oddp1evenALTV  47838  divgcdoddALTV  47844  lco0  48589  lindslinindsimp2lem5  48624  snlindsntor  48633  elbigo2  48714  affinecomb1  48864  itscnhlinecirc02p  48947  reuxfr1dd  48968  iscnrm3lem1  49095