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  3641  reuxfr1d  3704  n0moeu  4304  eldifvsn  4744  xpco  6231  funcnv3  6546  fnssresb  6598  dff1o5  6767  fneqeql2  6975  dffo3  7030  dffo3f  7034  fmptco  7057  fconst4  7143  riota2df  7321  eloprabga  7450  fnwelem  8056  frxp2  8069  xpord2pred  8070  xpord3pred  8077  mptsuppd  8112  mptelixpg  8854  boxcutc  8860  inficl  9304  cantnfle  9556  cantnflem1  9574  ttrclselem2  9611  bnd2  9781  iscard2  9864  alephinit  9981  kmlem2  10038  cfss  10151  fpwwe2lem8  10524  axgroth2  10711  elnnnn0  12419  znnsub  12513  znn0sub  12514  negelrp  12920  xsubge0  13155  divelunit  13389  elfz5  13411  preduz  13545  injresinj  13686  adddivflid  13717  divfl0  13723  hashf1lem1  14357  swrdspsleq  14568  repswsymball  14681  repswsymballbi  14682  2shfti  14982  cnpart  15142  sqrtneglem  15168  rexuz3  15251  rlim  15397  rlim2  15398  clim2c  15407  cvgcmp  15718  bitsmod  16342  bitscmp  16344  pc2dvds  16786  prmreclem4  16826  1arith  16834  imasleval  17440  xpsfrnel  17461  xpsfrnel2  17463  dfiso2  17674  pospropd  18226  latleeqm1  18368  latnlemlt  18373  latnle  18374  ipole  18435  gsumval2a  18588  ismhm0  18693  ghmeqker  19150  gastacos  19217  isslw  19515  slwpss  19519  pgpssslw  19521  fislw  19532  sylow3lem6  19539  dprd2d2  19953  isrnghmmul  20355  isdomn3  20625  lsslss  20889  lsmspsn  21013  zndvds  21481  znleval2  21487  elfilspd  21735  islinds2  21745  islindf2  21746  ismhp3  22052  coe1mul2lem1  22176  eltg3  22872  leordtvallem1  23120  leordtvallem2  23121  lmbrf  23170  cnrest2  23196  xkoccn  23529  hauseqlcld  23556  qtopcn  23624  ordthmeolem  23711  isfbas  23739  fbunfip  23779  fixufil  23832  alexsubALTlem4  23960  ismet2  24243  xblpnfps  24305  xblpnf  24306  blval2  24472  metuel2  24475  dscopn  24483  cnbl0  24683  cnblcld  24684  xrtgioo  24717  mulc1cncf  24820  isclmp  25019  isncvsngp  25071  lmmbrf  25184  iscauf  25202  caucfil  25205  lmclim  25225  evthicc2  25383  volsup  25479  ioombl1lem4  25484  ismbf  25551  ismbfcn  25552  mbfmulc2lem  25570  mbfmax  25572  mbfposr  25575  ismbf3d  25577  mbfimaopnlem  25578  mbfsup  25587  i1fpos  25629  mbfi1fseqlem4  25641  xrge0f  25654  itg2seq  25665  itg2monolem1  25673  itg2gt0  25683  itg2cnlem1  25684  itg2cnlem2  25685  i1fibl  25731  ditgneg  25780  lhop1  25941  r1pid2  26089  fta1  26238  ulm2  26316  pilem1  26383  sineq0  26455  ellogrn  26490  rlimcnp  26897  wilthlem1  27000  sqff1o  27114  logfaclbnd  27155  bposlem1  27217  lgsdilem  27257  lgsabs1  27269  lgsdchrval  27287  lgsquadlem1  27313  lgsquadlem2  27314  ssltsnb  27727  zn0subs  28322  iscgrgd  28486  trgcgrg  28488  ltgov  28570  ishlg  28575  lnhl  28588  israg  28670  islnopp  28712  iscgra  28782  isinag  28811  iseqlg  28840  nbupgrel  29318  isuvtx  29368  iscplgredg  29390  rusgrnumwwlkl1  29941  clwlkclwwlk2  29975  isclwwlknx  30008  clwwlkn1  30013  nmoo0  30763  ubthlem1  30842  ch0pss  31417  pjnorm2  31699  adjval  31862  leop  32095  atcv0eq  32351  xppreima  32619  fmptcof2  32631  xrdifh  32755  hashgt1  32782  isinftm  33142  isunit3  33200  isdrng4  33253  fracerl  33264  dvdsruassoi  33341  dvdsruasso  33342  dvdsrspss  33344  lsmsnorb  33348  ply1degltel  33547  r1pid2OLD  33561  psrbasfsupp  33564  smatrcl  33801  rhmpreimacnlem  33889  ismntop  34031  brfae  34253  eulerpartlemr  34379  eulerpartlemn  34386  reprinrn  34623  reprinfz1  34627  reprdifc  34632  bnj1173  35006  subfacp1lem5  35220  rexxfr3dALT  35675  filnetlem4  36415  bj-clel3gALT  37082  bj-imdirco  37224  taupilem3  37353  topdifinffinlem  37381  finxpsuclem  37431  matunitlindf  37658  poimirlem22  37682  poimirlem26  37686  poimirlem27  37687  heicant  37695  mbfposadd  37707  itg2addnclem  37711  itg2addnclem2  37712  iblabsnclem  37723  ftc1anclem1  37733  ftc1anclem5  37737  areacirclem5  37752  areacirc  37753  lmclim2  37798  caures  37800  rrnheibor  37877  isdmn3  38114  opelvvdif  38294  brxrn  38402  lrelat  39053  lcvbr  39060  lsatcv0eq  39086  ellkr2  39130  lkr0f  39133  lkreqN  39209  opltn0  39229  op1le  39231  leatb  39331  atlltn0  39345  hlrelat5N  39440  hlrelat  39441  cvrval5  39454  cvrexchlem  39458  atcvr0eq  39465  athgt  39495  1cvrco  39511  islpln5  39574  islvol5  39618  elpadd2at2  39846  cdleme0ex2N  40263  cdleme3  40276  cdleme7  40288  cdlemg33e  40749  dochfln0  41516  lcfl1  41531  lcfls1N  41574  lspindp5  41809  isnacs2  42739  rabrenfdioph  42847  rmxycomplete  42950  expdioph  43056  pwfi2f1o  43129  islnr3  43148  sqrtcvallem1  43664  ntrneixb  44128  clim2cf  45688  funressnfv  47074  focofob  47111  oddm1evenALTV  47706  oddp1evenALTV  47707  divgcdoddALTV  47713  lco0  48459  lindslinindsimp2lem5  48494  snlindsntor  48503  elbigo2  48584  affinecomb1  48734  itscnhlinecirc02p  48817  reuxfr1dd  48838  iscnrm3lem1  48965