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  708  3biant1d  1481  elrab3t  3634  reuxfr1d  3697  n0moeu  4300  eldifvsn  4741  xpco  6247  funcnv3  6562  fnssresb  6614  dff1o5  6783  fneqeql2  6993  dffo3  7048  dffo3f  7052  fmptco  7076  fconst4  7162  riota2df  7340  eloprabga  7469  fnwelem  8074  frxp2  8087  xpord2pred  8088  xpord3pred  8095  mptsuppd  8130  mptelixpg  8876  boxcutc  8882  inficl  9331  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  20683  lsslss  20947  lsmspsn  21071  zndvds  21539  znleval2  21545  elfilspd  21793  islinds2  21803  islindf2  21804  ismhp3  22118  coe1mul2lem1  22242  eltg3  22937  leordtvallem1  23185  leordtvallem2  23186  lmbrf  23235  cnrest2  23261  xkoccn  23594  hauseqlcld  23621  qtopcn  23689  ordthmeolem  23776  isfbas  23804  fbunfip  23844  fixufil  23897  alexsubALTlem4  24025  ismet2  24308  xblpnfps  24370  xblpnf  24371  blval2  24537  metuel2  24540  dscopn  24548  cnbl0  24748  cnblcld  24749  xrtgioo  24782  mulc1cncf  24882  isclmp  25074  isncvsngp  25126  lmmbrf  25239  iscauf  25257  caucfil  25260  lmclim  25280  evthicc2  25437  volsup  25533  ioombl1lem4  25538  ismbf  25605  ismbfcn  25606  mbfmulc2lem  25624  mbfmax  25626  mbfposr  25629  ismbf3d  25631  mbfimaopnlem  25632  mbfsup  25641  i1fpos  25683  mbfi1fseqlem4  25695  xrge0f  25708  itg2seq  25719  itg2monolem1  25727  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  i1fibl  25785  ditgneg  25834  lhop1  25991  r1pid2  26137  fta1  26285  ulm2  26363  pilem1  26429  sineq0  26501  ellogrn  26536  rlimcnp  26942  wilthlem1  27045  sqff1o  27159  logfaclbnd  27199  bposlem1  27261  lgsdilem  27301  lgsabs1  27313  lgsdchrval  27331  lgsquadlem1  27357  lgsquadlem2  27358  sltssnb  27775  zn0subs  28409  iscgrgd  28595  trgcgrg  28597  ltgov  28679  ishlg  28684  lnhl  28697  israg  28779  islnopp  28821  iscgra  28891  isinag  28920  iseqlg  28949  nbupgrel  29428  isuvtx  29478  iscplgredg  29500  rusgrnumwwlkl1  30054  clwlkclwwlk2  30088  isclwwlknx  30121  clwwlkn1  30126  nmoo0  30877  ubthlem1  30956  ch0pss  31531  pjnorm2  31813  adjval  31976  leop  32209  atcv0eq  32465  xppreima  32733  fmptcof2  32745  xrdifh  32868  hashgt1  32896  isinftm  33257  isunit3  33317  isdrng4  33371  fracerl  33382  dvdsruassoi  33459  dvdsruasso  33460  dvdsrspss  33462  lsmsnorb  33466  ply1degltel  33669  r1pid2OLD  33684  psrbasfsupp  33687  smatrcl  33956  rhmpreimacnlem  34044  ismntop  34186  brfae  34408  eulerpartlemr  34534  eulerpartlemn  34541  reprinrn  34778  reprinfz1  34782  reprdifc  34787  bnj1173  35160  subfacp1lem5  35382  rexxfr3dALT  35837  filnetlem4  36579  mh-infprim1bi  36744  bj-clel3gALT  37371  bj-imdirco  37520  taupilem3  37649  topdifinffinlem  37677  finxpsuclem  37727  matunitlindf  37953  poimirlem22  37977  poimirlem26  37981  poimirlem27  37982  heicant  37990  mbfposadd  38002  itg2addnclem  38006  itg2addnclem2  38007  iblabsnclem  38018  ftc1anclem1  38028  ftc1anclem5  38032  areacirclem5  38047  areacirc  38048  lmclim2  38093  caures  38095  rrnheibor  38172  isdmn3  38409  opelvvdif  38599  ralrnmo  38696  raldmqsmo  38698  brxrn  38718  lrelat  39474  lcvbr  39481  lsatcv0eq  39507  ellkr2  39551  lkr0f  39554  lkreqN  39630  opltn0  39650  op1le  39652  leatb  39752  atlltn0  39766  hlrelat5N  39861  hlrelat  39862  cvrval5  39875  cvrexchlem  39879  atcvr0eq  39886  athgt  39916  1cvrco  39932  islpln5  39995  islvol5  40039  elpadd2at2  40267  cdleme0ex2N  40684  cdleme3  40697  cdleme7  40709  cdlemg33e  41170  dochfln0  41937  lcfl1  41952  lcfls1N  41995  lspindp5  42230  isnacs2  43152  rabrenfdioph  43260  rmxycomplete  43363  expdioph  43469  pwfi2f1o  43542  islnr3  43561  sqrtcvallem1  44076  ntrneixb  44540  clim2cf  46096  funressnfv  47503  focofob  47540  nprmmul1  47999  oddm1evenALTV  48163  oddp1evenALTV  48164  divgcdoddALTV  48170  lco0  48915  lindslinindsimp2lem5  48950  snlindsntor  48959  elbigo2  49040  affinecomb1  49190  itscnhlinecirc02p  49273  reuxfr1dd  49294  iscnrm3lem1  49421