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  3658  reuxfr1d  3721  n0moeu  4322  eldifvsn  4761  xpco  6262  funcnv3  6586  fnssresb  6640  dff1o5  6809  fneqeql2  7019  dffo3  7074  dffo3f  7078  fmptco  7101  fconst4  7188  riota2df  7367  eloprabga  7498  fnwelem  8110  frxp2  8123  xpord2pred  8124  xpord3pred  8131  mptsuppd  8166  mptelixpg  8908  boxcutc  8914  inficl  9376  cantnfle  9624  cantnflem1  9642  ttrclselem2  9679  bnd2  9846  iscard2  9929  alephinit  10048  kmlem2  10105  cfss  10218  fpwwe2lem8  10591  axgroth2  10778  elnnnn0  12485  znnsub  12579  znn0sub  12580  negelrp  12986  xsubge0  13221  divelunit  13455  elfz5  13477  preduz  13611  injresinj  13749  adddivflid  13780  divfl0  13786  hashf1lem1  14420  swrdspsleq  14630  repswsymball  14744  repswsymballbi  14745  2shfti  15046  cnpart  15206  sqrtneglem  15232  rexuz3  15315  rlim  15461  rlim2  15462  clim2c  15471  cvgcmp  15782  bitsmod  16406  bitscmp  16408  pc2dvds  16850  prmreclem4  16890  1arith  16898  imasleval  17504  xpsfrnel  17525  xpsfrnel2  17527  dfiso2  17734  pospropd  18286  latleeqm1  18426  latnlemlt  18431  latnle  18432  ipole  18493  gsumval2a  18612  ismhm0  18717  ghmeqker  19175  gastacos  19242  isslw  19538  slwpss  19542  pgpssslw  19544  fislw  19555  sylow3lem6  19562  dprd2d2  19976  isrnghmmul  20351  isdomn3  20624  lsslss  20867  lsmspsn  20991  zndvds  21459  znleval2  21465  elfilspd  21712  islinds2  21722  islindf2  21723  ismhp3  22029  coe1mul2lem1  22153  eltg3  22849  leordtvallem1  23097  leordtvallem2  23098  lmbrf  23147  cnrest2  23173  xkoccn  23506  hauseqlcld  23533  qtopcn  23601  ordthmeolem  23688  isfbas  23716  fbunfip  23756  fixufil  23809  alexsubALTlem4  23937  ismet2  24221  xblpnfps  24283  xblpnf  24284  blval2  24450  metuel2  24453  dscopn  24461  cnbl0  24661  cnblcld  24662  xrtgioo  24695  mulc1cncf  24798  isclmp  24997  isncvsngp  25049  lmmbrf  25162  iscauf  25180  caucfil  25183  lmclim  25203  evthicc2  25361  volsup  25457  ioombl1lem4  25462  ismbf  25529  ismbfcn  25530  mbfmulc2lem  25548  mbfmax  25550  mbfposr  25553  ismbf3d  25555  mbfimaopnlem  25556  mbfsup  25565  i1fpos  25607  mbfi1fseqlem4  25619  xrge0f  25632  itg2seq  25643  itg2monolem1  25651  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  i1fibl  25709  ditgneg  25758  lhop1  25919  r1pid2  26067  fta1  26216  ulm2  26294  pilem1  26361  sineq0  26433  ellogrn  26468  rlimcnp  26875  wilthlem1  26978  sqff1o  27092  logfaclbnd  27133  bposlem1  27195  lgsdilem  27235  lgsabs1  27247  lgsdchrval  27265  lgsquadlem1  27291  lgsquadlem2  27292  zn0subs  28291  iscgrgd  28440  trgcgrg  28442  ltgov  28524  ishlg  28529  lnhl  28542  israg  28624  islnopp  28666  iscgra  28736  isinag  28765  iseqlg  28794  nbupgrel  29272  isuvtx  29322  iscplgredg  29344  rusgrnumwwlkl1  29898  clwlkclwwlk2  29932  isclwwlknx  29965  clwwlkn1  29970  nmoo0  30720  ubthlem1  30799  ch0pss  31374  pjnorm2  31656  adjval  31819  leop  32052  atcv0eq  32308  xppreima  32569  fmptcof2  32581  xrdifh  32703  hashgt1  32733  isinftm  33135  isunit3  33192  isdrng4  33245  fracerl  33256  dvdsruassoi  33355  dvdsruasso  33356  dvdsrspss  33358  lsmsnorb  33362  ply1degltel  33560  r1pid2OLD  33574  smatrcl  33786  rhmpreimacnlem  33874  ismntop  34016  brfae  34238  eulerpartlemr  34365  eulerpartlemn  34372  reprinrn  34609  reprinfz1  34613  reprdifc  34618  bnj1173  34992  subfacp1lem5  35171  rexxfr3dALT  35626  filnetlem4  36369  bj-clel3gALT  37036  bj-imdirco  37178  taupilem3  37307  topdifinffinlem  37335  finxpsuclem  37385  matunitlindf  37612  poimirlem22  37636  poimirlem26  37640  poimirlem27  37641  heicant  37649  mbfposadd  37661  itg2addnclem  37665  itg2addnclem2  37666  iblabsnclem  37677  ftc1anclem1  37687  ftc1anclem5  37691  areacirclem5  37706  areacirc  37707  lmclim2  37752  caures  37754  rrnheibor  37831  isdmn3  38068  opelvvdif  38248  brxrn  38356  lrelat  39007  lcvbr  39014  lsatcv0eq  39040  ellkr2  39084  lkr0f  39087  lkreqN  39163  opltn0  39183  op1le  39185  leatb  39285  atlltn0  39299  hlrelat5N  39395  hlrelat  39396  cvrval5  39409  cvrexchlem  39413  atcvr0eq  39420  athgt  39450  1cvrco  39466  islpln5  39529  islvol5  39573  elpadd2at2  39801  cdleme0ex2N  40218  cdleme3  40231  cdleme7  40243  cdlemg33e  40704  dochfln0  41471  lcfl1  41486  lcfls1N  41529  lspindp5  41764  isnacs2  42694  rabrenfdioph  42802  rmxycomplete  42906  expdioph  43012  pwfi2f1o  43085  islnr3  43104  sqrtcvallem1  43620  ntrneixb  44084  clim2cf  45648  funressnfv  47044  focofob  47081  oddm1evenALTV  47676  oddp1evenALTV  47677  divgcdoddALTV  47683  lco0  48416  lindslinindsimp2lem5  48451  snlindsntor  48460  elbigo2  48541  affinecomb1  48691  itscnhlinecirc02p  48774  reuxfr1dd  48795  iscnrm3lem1  48922