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  3661  reuxfr1d  3724  n0moeu  4325  eldifvsn  4764  xpco  6265  funcnv3  6589  fnssresb  6643  dff1o5  6812  fneqeql2  7022  dffo3  7077  dffo3f  7081  fmptco  7104  fconst4  7191  riota2df  7370  eloprabga  7501  fnwelem  8113  frxp2  8126  xpord2pred  8127  xpord3pred  8134  mptsuppd  8169  mptelixpg  8911  boxcutc  8917  inficl  9383  cantnfle  9631  cantnflem1  9649  ttrclselem2  9686  bnd2  9853  iscard2  9936  alephinit  10055  kmlem2  10112  cfss  10225  fpwwe2lem8  10598  axgroth2  10785  elnnnn0  12492  znnsub  12586  znn0sub  12587  negelrp  12993  xsubge0  13228  divelunit  13462  elfz5  13484  preduz  13618  injresinj  13756  adddivflid  13787  divfl0  13793  hashf1lem1  14427  swrdspsleq  14637  repswsymball  14751  repswsymballbi  14752  2shfti  15053  cnpart  15213  sqrtneglem  15239  rexuz3  15322  rlim  15468  rlim2  15469  clim2c  15478  cvgcmp  15789  bitsmod  16413  bitscmp  16415  pc2dvds  16857  prmreclem4  16897  1arith  16905  imasleval  17511  xpsfrnel  17532  xpsfrnel2  17534  dfiso2  17741  pospropd  18293  latleeqm1  18433  latnlemlt  18438  latnle  18439  ipole  18500  gsumval2a  18619  ismhm0  18724  ghmeqker  19182  gastacos  19249  isslw  19545  slwpss  19549  pgpssslw  19551  fislw  19562  sylow3lem6  19569  dprd2d2  19983  isrnghmmul  20358  isdomn3  20631  lsslss  20874  lsmspsn  20998  zndvds  21466  znleval2  21472  elfilspd  21719  islinds2  21729  islindf2  21730  ismhp3  22036  coe1mul2lem1  22160  eltg3  22856  leordtvallem1  23104  leordtvallem2  23105  lmbrf  23154  cnrest2  23180  xkoccn  23513  hauseqlcld  23540  qtopcn  23608  ordthmeolem  23695  isfbas  23723  fbunfip  23763  fixufil  23816  alexsubALTlem4  23944  ismet2  24228  xblpnfps  24290  xblpnf  24291  blval2  24457  metuel2  24460  dscopn  24468  cnbl0  24668  cnblcld  24669  xrtgioo  24702  mulc1cncf  24805  isclmp  25004  isncvsngp  25056  lmmbrf  25169  iscauf  25187  caucfil  25190  lmclim  25210  evthicc2  25368  volsup  25464  ioombl1lem4  25469  ismbf  25536  ismbfcn  25537  mbfmulc2lem  25555  mbfmax  25557  mbfposr  25560  ismbf3d  25562  mbfimaopnlem  25563  mbfsup  25572  i1fpos  25614  mbfi1fseqlem4  25626  xrge0f  25639  itg2seq  25650  itg2monolem1  25658  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  i1fibl  25716  ditgneg  25765  lhop1  25926  r1pid2  26074  fta1  26223  ulm2  26301  pilem1  26368  sineq0  26440  ellogrn  26475  rlimcnp  26882  wilthlem1  26985  sqff1o  27099  logfaclbnd  27140  bposlem1  27202  lgsdilem  27242  lgsabs1  27254  lgsdchrval  27272  lgsquadlem1  27298  lgsquadlem2  27299  zn0subs  28298  iscgrgd  28447  trgcgrg  28449  ltgov  28531  ishlg  28536  lnhl  28549  israg  28631  islnopp  28673  iscgra  28743  isinag  28772  iseqlg  28801  nbupgrel  29279  isuvtx  29329  iscplgredg  29351  rusgrnumwwlkl1  29905  clwlkclwwlk2  29939  isclwwlknx  29972  clwwlkn1  29977  nmoo0  30727  ubthlem1  30806  ch0pss  31381  pjnorm2  31663  adjval  31826  leop  32059  atcv0eq  32315  xppreima  32576  fmptcof2  32588  xrdifh  32710  hashgt1  32740  isinftm  33142  isunit3  33199  isdrng4  33252  fracerl  33263  dvdsruassoi  33362  dvdsruasso  33363  dvdsrspss  33365  lsmsnorb  33369  ply1degltel  33567  r1pid2OLD  33581  smatrcl  33793  rhmpreimacnlem  33881  ismntop  34023  brfae  34245  eulerpartlemr  34372  eulerpartlemn  34379  reprinrn  34616  reprinfz1  34620  reprdifc  34625  bnj1173  34999  subfacp1lem5  35178  rexxfr3dALT  35633  filnetlem4  36376  bj-clel3gALT  37043  bj-imdirco  37185  taupilem3  37314  topdifinffinlem  37342  finxpsuclem  37392  matunitlindf  37619  poimirlem22  37643  poimirlem26  37647  poimirlem27  37648  heicant  37656  mbfposadd  37668  itg2addnclem  37672  itg2addnclem2  37673  iblabsnclem  37684  ftc1anclem1  37694  ftc1anclem5  37698  areacirclem5  37713  areacirc  37714  lmclim2  37759  caures  37761  rrnheibor  37838  isdmn3  38075  opelvvdif  38255  brxrn  38363  lrelat  39014  lcvbr  39021  lsatcv0eq  39047  ellkr2  39091  lkr0f  39094  lkreqN  39170  opltn0  39190  op1le  39192  leatb  39292  atlltn0  39306  hlrelat5N  39402  hlrelat  39403  cvrval5  39416  cvrexchlem  39420  atcvr0eq  39427  athgt  39457  1cvrco  39473  islpln5  39536  islvol5  39580  elpadd2at2  39808  cdleme0ex2N  40225  cdleme3  40238  cdleme7  40250  cdlemg33e  40711  dochfln0  41478  lcfl1  41493  lcfls1N  41536  lspindp5  41771  isnacs2  42701  rabrenfdioph  42809  rmxycomplete  42913  expdioph  43019  pwfi2f1o  43092  islnr3  43111  sqrtcvallem1  43627  ntrneixb  44091  clim2cf  45655  funressnfv  47048  focofob  47085  oddm1evenALTV  47680  oddp1evenALTV  47681  divgcdoddALTV  47687  lco0  48420  lindslinindsimp2lem5  48455  snlindsntor  48464  elbigo2  48545  affinecomb1  48695  itscnhlinecirc02p  48778  reuxfr1dd  48799  iscnrm3lem1  48926