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  1477  elrab3t  3693  reuxfr1d  3758  n0moeu  4364  eldifvsn  4801  xpco  6310  funcnv3  6637  fnssresb  6690  dff1o5  6857  fneqeql2  7066  dffo3  7121  dffo3f  7125  fmptco  7148  fconst4  7233  riota2df  7410  eloprabga  7540  eloprabgaOLD  7541  fnwelem  8154  frxp2  8167  xpord2pred  8168  xpord3pred  8175  mptsuppd  8210  mptelixpg  8973  boxcutc  8979  inficl  9462  cantnfle  9708  cantnflem1  9726  ttrclselem2  9763  bnd2  9930  iscard2  10013  alephinit  10132  kmlem2  10189  cfss  10302  fpwwe2lem8  10675  axgroth2  10862  elnnnn0  12566  znnsub  12660  znn0sub  12661  negelrp  13065  xsubge0  13299  divelunit  13530  elfz5  13552  preduz  13686  injresinj  13823  adddivflid  13854  divfl0  13860  hashf1lem1  14490  swrdspsleq  14699  repswsymball  14813  repswsymballbi  14814  2shfti  15115  cnpart  15275  sqrtneglem  15301  rexuz3  15383  rlim  15527  rlim2  15528  clim2c  15537  cvgcmp  15848  bitsmod  16469  bitscmp  16471  pc2dvds  16912  prmreclem4  16952  1arith  16960  imasleval  17587  xpsfrnel  17608  xpsfrnel2  17610  dfiso2  17819  pospropd  18384  latleeqm1  18524  latnlemlt  18529  latnle  18530  ipole  18591  gsumval2a  18710  ismhm0  18815  ghmeqker  19273  gastacos  19340  isslw  19640  slwpss  19644  pgpssslw  19646  fislw  19657  sylow3lem6  19664  dprd2d2  20078  isrnghmmul  20458  isdomn3  20731  lsslss  20976  lsmspsn  21100  zndvds  21585  znleval2  21591  elfilspd  21840  islinds2  21850  islindf2  21851  ismhp3  22163  coe1mul2lem1  22285  eltg3  22984  leordtvallem1  23233  leordtvallem2  23234  lmbrf  23283  cnrest2  23309  xkoccn  23642  hauseqlcld  23669  qtopcn  23737  ordthmeolem  23824  isfbas  23852  fbunfip  23892  fixufil  23945  alexsubALTlem4  24073  ismet2  24358  xblpnfps  24420  xblpnf  24421  blval2  24590  metuel2  24593  dscopn  24601  cnbl0  24809  cnblcld  24810  xrtgioo  24841  mulc1cncf  24944  isclmp  25143  isncvsngp  25196  lmmbrf  25309  iscauf  25327  caucfil  25330  lmclim  25350  evthicc2  25508  volsup  25604  ioombl1lem4  25609  ismbf  25676  ismbfcn  25677  mbfmulc2lem  25695  mbfmax  25697  mbfposr  25700  ismbf3d  25702  mbfimaopnlem  25703  mbfsup  25712  i1fpos  25755  mbfi1fseqlem4  25767  xrge0f  25780  itg2seq  25791  itg2monolem1  25799  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  i1fibl  25857  ditgneg  25906  lhop1  26067  r1pid2  26215  fta1  26364  ulm2  26442  pilem1  26509  sineq0  26580  ellogrn  26615  rlimcnp  27022  wilthlem1  27125  sqff1o  27239  logfaclbnd  27280  bposlem1  27342  lgsdilem  27382  lgsabs1  27394  lgsdchrval  27412  lgsquadlem1  27438  lgsquadlem2  27439  zn0subs  28403  iscgrgd  28535  trgcgrg  28537  ltgov  28619  ishlg  28624  lnhl  28637  israg  28719  islnopp  28761  iscgra  28831  isinag  28860  iseqlg  28889  nbupgrel  29376  isuvtx  29426  iscplgredg  29448  rusgrnumwwlkl1  29997  clwlkclwwlk2  30031  isclwwlknx  30064  clwwlkn1  30069  nmoo0  30819  ubthlem1  30898  ch0pss  31473  pjnorm2  31755  adjval  31918  leop  32151  atcv0eq  32407  xppreima  32661  fmptcof2  32673  xrdifh  32788  hashgt1  32817  isinftm  33170  isunit3  33230  isdrng4  33278  fracerl  33287  dvdsruassoi  33391  dvdsruasso  33392  dvdsrspss  33394  lsmsnorb  33398  ply1degltel  33594  r1pid2OLD  33608  smatrcl  33756  rhmpreimacnlem  33844  ismntop  33988  brfae  34228  eulerpartlemr  34355  eulerpartlemn  34362  reprinrn  34611  reprinfz1  34615  reprdifc  34620  bnj1173  34994  subfacp1lem5  35168  rexxfr3dALT  35623  filnetlem4  36363  bj-clel3gALT  37030  bj-imdirco  37172  taupilem3  37301  topdifinffinlem  37329  finxpsuclem  37379  matunitlindf  37604  poimirlem22  37628  poimirlem26  37632  poimirlem27  37633  heicant  37641  mbfposadd  37653  itg2addnclem  37657  itg2addnclem2  37658  iblabsnclem  37669  ftc1anclem1  37679  ftc1anclem5  37683  areacirclem5  37698  areacirc  37699  lmclim2  37744  caures  37746  rrnheibor  37823  isdmn3  38060  opelvvdif  38240  brxrn  38355  lrelat  38995  lcvbr  39002  lsatcv0eq  39028  ellkr2  39072  lkr0f  39075  lkreqN  39151  opltn0  39171  op1le  39173  leatb  39273  atlltn0  39287  hlrelat5N  39383  hlrelat  39384  cvrval5  39397  cvrexchlem  39401  atcvr0eq  39408  athgt  39438  1cvrco  39454  islpln5  39517  islvol5  39561  elpadd2at2  39789  cdleme0ex2N  40206  cdleme3  40219  cdleme7  40231  cdlemg33e  40692  dochfln0  41459  lcfl1  41474  lcfls1N  41517  lspindp5  41752  isnacs2  42693  rabrenfdioph  42801  rmxycomplete  42905  expdioph  43011  pwfi2f1o  43084  islnr3  43103  sqrtcvallem1  43620  ntrneixb  44084  clim2cf  45605  funressnfv  46992  focofob  47029  oddm1evenALTV  47599  oddp1evenALTV  47600  divgcdoddALTV  47606  lco0  48272  lindslinindsimp2lem5  48307  snlindsntor  48316  elbigo2  48401  affinecomb1  48551  itscnhlinecirc02p  48634  reuxfr1dd  48654  iscnrm3lem1  48729