Theorem biantrurd 537

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 533	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm5.3  577  mpbirand  713  3biant1d  1486  elrab3t  3628  reuxfr1d  3691  n0moeu  4287  eldifvsn  4730  xpco  6240  funcnv3  6555  fnssresb  6607  dff1o5  6776  fneqeql2  6988  dffo3  7043  dffo3f  7047  fmptco  7071  fconst4  7158  riota2df  7336  eloprabga  7465  fnwelem  8071  frxp2  8084  xpord2pred  8085  xpord3pred  8092  mptsuppd  8127  mptelixpg  8873  boxcutc  8879  inficl  9328  cantnfle  9583  cantnflem1  9601  ttrclselem2  9638  bnd2  9808  iscard2  9891  alephinit  10008  kmlem2  10065  cfss  10178  fpwwe2lem8  10552  axgroth2  10739  elnnnn0  12471  znnsub  12564  znn0sub  12565  negelrp  12968  xsubge0  13204  divelunit  13438  elfz5  13461  preduz  13595  injresinj  13737  adddivflid  13768  divfl0  13774  hashf1lem1  14408  swrdspsleq  14619  repswsymball  14732  repswsymballbi  14733  2shfti  15033  cnpart  15193  sqrtneglem  15219  rexuz3  15302  rlim  15448  rlim2  15449  clim2c  15458  cvgcmp  15770  bitsmod  16396  bitscmp  16398  pc2dvds  16841  prmreclem4  16881  1arith  16889  imasleval  17496  xpsfrnel  17517  xpsfrnel2  17519  dfiso2  17730  pospropd  18282  latleeqm1  18424  latnlemlt  18429  latnle  18430  ipole  18491  gsumval2a  18644  ismhm0  18749  ghmeqker  19209  gastacos  19276  isslw  19574  slwpss  19578  pgpssslw  19580  fislw  19591  sylow3lem6  19598  dprd2d2  20012  isrnghmmul  20413  isdomn3  20687  lsslss  20951  lsmspsn  21074  zndvds  21524  znleval2  21530  elfilspd  21778  islinds2  21788  islindf2  21789  ismhp3  22130  coe1mul2lem1  22253  eltg3  22945  leordtvallem1  23193  leordtvallem2  23194  lmbrf  23243  cnrest2  23269  xkoccn  23602  hauseqlcld  23629  qtopcn  23697  ordthmeolem  23784  isfbas  23812  fbunfip  23852  fixufil  23905  alexsubALTlem4  24033  ismet2  24316  xblpnfps  24378  xblpnf  24379  blval2  24545  metuel2  24548  dscopn  24556  cnbl0  24756  cnblcld  24757  xrtgioo  24790  mulc1cncf  24890  isclmp  25082  isncvsngp  25134  lmmbrf  25247  iscauf  25265  caucfil  25268  lmclim  25288  evthicc2  25445  volsup  25541  ioombl1lem4  25546  ismbf  25613  ismbfcn  25614  mbfmulc2lem  25632  mbfmax  25634  mbfposr  25637  ismbf3d  25639  mbfimaopnlem  25640  mbfsup  25649  i1fpos  25691  mbfi1fseqlem4  25703  xrge0f  25716  itg2seq  25727  itg2monolem1  25735  itg2gt0  25745  itg2cnlem1  25746  itg2cnlem2  25747  i1fibl  25793  ditgneg  25842  lhop1  25999  r1pid2  26145  fta1  26292  ulm2  26368  pilem1  26434  sineq0  26506  ellogrn  26541  rlimcnp  26947  wilthlem1  27049  sqff1o  27163  logfaclbnd  27203  bposlem1  27265  lgsdilem  27305  lgsabs1  27317  lgsdchrval  27335  lgsquadlem1  27361  lgsquadlem2  27362  sltssnb  27779  zn0subs  28413  iscgrgd  28599  trgcgrg  28601  ltgov  28683  ishlg  28688  lnhl  28701  israg  28783  islnopp  28825  iscgra  28895  isinag  28924  iseqlg  28953  nbupgrel  29432  isuvtx  29482  iscplgredg  29504  rusgrnumwwlkl1  30057  clwlkclwwlk2  30091  isclwwlknx  30124  clwwlkn1  30129  nmoo0  30880  ubthlem1  30959  ch0pss  31534  pjnorm2  31816  adjval  31979  leop  32212  atcv0eq  32468  xppreima  32737  fmptcof2  32749  xrdifh  32872  hashgt1  32900  isinftm  33262  isunit3  33322  isdrng4  33379  fracerl  33390  dvdsruassoi  33467  dvdsruasso  33468  dvdsrspss  33470  lsmsnorb  33474  ply1degltel  33677  r1pid2OLD  33692  psrbasfsupp  33695  smatrcl  33980  rhmpreimacnlem  34068  ismntop  34210  brfae  34432  eulerpartlemr  34558  eulerpartlemn  34565  reprinrn  34802  reprinfz1  34806  reprdifc  34811  bnj1173  35184  subfacp1lem5  35412  rexxfr3dALT  35867  filnetlem4  36609  mh-infprim1bi  36774  bj-clel3gALT  37401  bj-imdirco  37550  taupilem3  37679  topdifinffinlem  37709  finxpsuclem  37759  matunitlindf  37985  poimirlem22  38009  poimirlem26  38013  poimirlem27  38014  heicant  38022  mbfposadd  38034  itg2addnclem  38038  itg2addnclem2  38039  iblabsnclem  38050  ftc1anclem1  38060  ftc1anclem5  38064  areacirclem5  38079  areacirc  38080  lmclim2  38125  caures  38127  rrnheibor  38204  isdmn3  38441  opelvvdif  38631  ralrnmo  38728  raldmqsmo  38730  brxrn  38750  lrelat  39506  lcvbr  39513  lsatcv0eq  39539  ellkr2  39583  lkr0f  39586  lkreqN  39662  opltn0  39682  op1le  39684  leatb  39784  atlltn0  39798  hlrelat5N  39893  hlrelat  39894  cvrval5  39907  cvrexchlem  39911  atcvr0eq  39918  athgt  39948  1cvrco  39964  islpln5  40027  islvol5  40071  elpadd2at2  40299  cdleme0ex2N  40716  cdleme3  40729  cdleme7  40741  cdlemg33e  41202  dochfln0  41969  lcfl1  41984  lcfls1N  42027  lspindp5  42262  isnacs2  43155  rabrenfdioph  43259  rmxycomplete  43362  expdioph  43468  pwfi2f1o  43541  islnr3  43560  sqrtcvallem1  44075  ntrneixb  44539  clim2cf  46093  funressnfv  47506  focofob  47543  nprmmul1  48002  oddm1evenALTV  48166  oddp1evenALTV  48167  divgcdoddALTV  48173  lco0  48918  lindslinindsimp2lem5  48953  snlindsntor  48962  elbigo2  49043  affinecomb1  49193  itscnhlinecirc02p  49276  reuxfr1dd  49297  iscnrm3lem1  49424