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  3691  reuxfr1d  3756  n0moeu  4359  eldifvsn  4797  xpco  6309  funcnv3  6636  fnssresb  6690  dff1o5  6857  fneqeql2  7067  dffo3  7122  dffo3f  7126  fmptco  7149  fconst4  7234  riota2df  7411  eloprabga  7542  fnwelem  8156  frxp2  8169  xpord2pred  8170  xpord3pred  8177  mptsuppd  8212  mptelixpg  8975  boxcutc  8981  inficl  9465  cantnfle  9711  cantnflem1  9729  ttrclselem2  9766  bnd2  9933  iscard2  10016  alephinit  10135  kmlem2  10192  cfss  10305  fpwwe2lem8  10678  axgroth2  10865  elnnnn0  12569  znnsub  12663  znn0sub  12664  negelrp  13068  xsubge0  13303  divelunit  13534  elfz5  13556  preduz  13690  injresinj  13827  adddivflid  13858  divfl0  13864  hashf1lem1  14494  swrdspsleq  14703  repswsymball  14817  repswsymballbi  14818  2shfti  15119  cnpart  15279  sqrtneglem  15305  rexuz3  15387  rlim  15531  rlim2  15532  clim2c  15541  cvgcmp  15852  bitsmod  16473  bitscmp  16475  pc2dvds  16917  prmreclem4  16957  1arith  16965  imasleval  17586  xpsfrnel  17607  xpsfrnel2  17609  dfiso2  17816  pospropd  18372  latleeqm1  18512  latnlemlt  18517  latnle  18518  ipole  18579  gsumval2a  18698  ismhm0  18803  ghmeqker  19261  gastacos  19328  isslw  19626  slwpss  19630  pgpssslw  19632  fislw  19643  sylow3lem6  19650  dprd2d2  20064  isrnghmmul  20442  isdomn3  20715  lsslss  20959  lsmspsn  21083  zndvds  21568  znleval2  21574  elfilspd  21823  islinds2  21833  islindf2  21834  ismhp3  22146  coe1mul2lem1  22270  eltg3  22969  leordtvallem1  23218  leordtvallem2  23219  lmbrf  23268  cnrest2  23294  xkoccn  23627  hauseqlcld  23654  qtopcn  23722  ordthmeolem  23809  isfbas  23837  fbunfip  23877  fixufil  23930  alexsubALTlem4  24058  ismet2  24343  xblpnfps  24405  xblpnf  24406  blval2  24575  metuel2  24578  dscopn  24586  cnbl0  24794  cnblcld  24795  xrtgioo  24828  mulc1cncf  24931  isclmp  25130  isncvsngp  25183  lmmbrf  25296  iscauf  25314  caucfil  25317  lmclim  25337  evthicc2  25495  volsup  25591  ioombl1lem4  25596  ismbf  25663  ismbfcn  25664  mbfmulc2lem  25682  mbfmax  25684  mbfposr  25687  ismbf3d  25689  mbfimaopnlem  25690  mbfsup  25699  i1fpos  25741  mbfi1fseqlem4  25753  xrge0f  25766  itg2seq  25777  itg2monolem1  25785  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  i1fibl  25843  ditgneg  25892  lhop1  26053  r1pid2  26201  fta1  26350  ulm2  26428  pilem1  26495  sineq0  26566  ellogrn  26601  rlimcnp  27008  wilthlem1  27111  sqff1o  27225  logfaclbnd  27266  bposlem1  27328  lgsdilem  27368  lgsabs1  27380  lgsdchrval  27398  lgsquadlem1  27424  lgsquadlem2  27425  zn0subs  28389  iscgrgd  28521  trgcgrg  28523  ltgov  28605  ishlg  28610  lnhl  28623  israg  28705  islnopp  28747  iscgra  28817  isinag  28846  iseqlg  28875  nbupgrel  29362  isuvtx  29412  iscplgredg  29434  rusgrnumwwlkl1  29988  clwlkclwwlk2  30022  isclwwlknx  30055  clwwlkn1  30060  nmoo0  30810  ubthlem1  30889  ch0pss  31464  pjnorm2  31746  adjval  31909  leop  32142  atcv0eq  32398  xppreima  32655  fmptcof2  32667  xrdifh  32782  hashgt1  32812  isinftm  33188  isunit3  33245  isdrng4  33298  fracerl  33308  dvdsruassoi  33412  dvdsruasso  33413  dvdsrspss  33415  lsmsnorb  33419  ply1degltel  33615  r1pid2OLD  33629  smatrcl  33795  rhmpreimacnlem  33883  ismntop  34027  brfae  34249  eulerpartlemr  34376  eulerpartlemn  34383  reprinrn  34633  reprinfz1  34637  reprdifc  34642  bnj1173  35016  subfacp1lem5  35189  rexxfr3dALT  35644  filnetlem4  36382  bj-clel3gALT  37049  bj-imdirco  37191  taupilem3  37320  topdifinffinlem  37348  finxpsuclem  37398  matunitlindf  37625  poimirlem22  37649  poimirlem26  37653  poimirlem27  37654  heicant  37662  mbfposadd  37674  itg2addnclem  37678  itg2addnclem2  37679  iblabsnclem  37690  ftc1anclem1  37700  ftc1anclem5  37704  areacirclem5  37719  areacirc  37720  lmclim2  37765  caures  37767  rrnheibor  37844  isdmn3  38081  opelvvdif  38260  brxrn  38375  lrelat  39015  lcvbr  39022  lsatcv0eq  39048  ellkr2  39092  lkr0f  39095  lkreqN  39171  opltn0  39191  op1le  39193  leatb  39293  atlltn0  39307  hlrelat5N  39403  hlrelat  39404  cvrval5  39417  cvrexchlem  39421  atcvr0eq  39428  athgt  39458  1cvrco  39474  islpln5  39537  islvol5  39581  elpadd2at2  39809  cdleme0ex2N  40226  cdleme3  40239  cdleme7  40251  cdlemg33e  40712  dochfln0  41479  lcfl1  41494  lcfls1N  41537  lspindp5  41772  isnacs2  42717  rabrenfdioph  42825  rmxycomplete  42929  expdioph  43035  pwfi2f1o  43108  islnr3  43127  sqrtcvallem1  43644  ntrneixb  44108  clim2cf  45665  funressnfv  47055  focofob  47092  oddm1evenALTV  47662  oddp1evenALTV  47663  divgcdoddALTV  47669  lco0  48344  lindslinindsimp2lem5  48379  snlindsntor  48388  elbigo2  48473  affinecomb1  48623  itscnhlinecirc02p  48706  reuxfr1dd  48726  iscnrm3lem1  48831