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  3633  reuxfr1d  3696  n0moeu  4299  eldifvsn  4742  xpco  6253  funcnv3  6568  fnssresb  6620  dff1o5  6789  fneqeql2  6999  dffo3  7054  dffo3f  7058  fmptco  7082  fconst4  7169  riota2df  7347  eloprabga  7476  fnwelem  8081  frxp2  8094  xpord2pred  8095  xpord3pred  8102  mptsuppd  8137  mptelixpg  8883  boxcutc  8889  inficl  9338  cantnfle  9592  cantnflem1  9610  ttrclselem2  9647  bnd2  9817  iscard2  9900  alephinit  10017  kmlem2  10074  cfss  10187  fpwwe2lem8  10561  axgroth2  10748  elnnnn0  12480  znnsub  12573  znn0sub  12574  negelrp  12977  xsubge0  13213  divelunit  13447  elfz5  13470  preduz  13604  injresinj  13746  adddivflid  13777  divfl0  13783  hashf1lem1  14417  swrdspsleq  14628  repswsymball  14741  repswsymballbi  14742  2shfti  15042  cnpart  15202  sqrtneglem  15228  rexuz3  15311  rlim  15457  rlim2  15458  clim2c  15467  cvgcmp  15779  bitsmod  16405  bitscmp  16407  pc2dvds  16850  prmreclem4  16890  1arith  16898  imasleval  17505  xpsfrnel  17526  xpsfrnel2  17528  dfiso2  17739  pospropd  18291  latleeqm1  18433  latnlemlt  18438  latnle  18439  ipole  18500  gsumval2a  18653  ismhm0  18758  ghmeqker  19218  gastacos  19285  isslw  19583  slwpss  19587  pgpssslw  19589  fislw  19600  sylow3lem6  19607  dprd2d2  20021  isrnghmmul  20422  isdomn3  20692  lsslss  20956  lsmspsn  21079  zndvds  21529  znleval2  21535  elfilspd  21783  islinds2  21793  islindf2  21794  ismhp3  22108  coe1mul2lem1  22232  eltg3  22927  leordtvallem1  23175  leordtvallem2  23176  lmbrf  23225  cnrest2  23251  xkoccn  23584  hauseqlcld  23611  qtopcn  23679  ordthmeolem  23766  isfbas  23794  fbunfip  23834  fixufil  23887  alexsubALTlem4  24015  ismet2  24298  xblpnfps  24360  xblpnf  24361  blval2  24527  metuel2  24530  dscopn  24538  cnbl0  24738  cnblcld  24739  xrtgioo  24772  mulc1cncf  24872  isclmp  25064  isncvsngp  25116  lmmbrf  25229  iscauf  25247  caucfil  25250  lmclim  25270  evthicc2  25427  volsup  25523  ioombl1lem4  25528  ismbf  25595  ismbfcn  25596  mbfmulc2lem  25614  mbfmax  25616  mbfposr  25619  ismbf3d  25621  mbfimaopnlem  25622  mbfsup  25631  i1fpos  25673  mbfi1fseqlem4  25685  xrge0f  25698  itg2seq  25709  itg2monolem1  25717  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  i1fibl  25775  ditgneg  25824  lhop1  25981  r1pid2  26127  fta1  26274  ulm2  26350  pilem1  26416  sineq0  26488  ellogrn  26523  rlimcnp  26929  wilthlem1  27031  sqff1o  27145  logfaclbnd  27185  bposlem1  27247  lgsdilem  27287  lgsabs1  27299  lgsdchrval  27317  lgsquadlem1  27343  lgsquadlem2  27344  sltssnb  27761  zn0subs  28395  iscgrgd  28581  trgcgrg  28583  ltgov  28665  ishlg  28670  lnhl  28683  israg  28765  islnopp  28807  iscgra  28877  isinag  28906  iseqlg  28935  nbupgrel  29414  isuvtx  29464  iscplgredg  29486  rusgrnumwwlkl1  30039  clwlkclwwlk2  30073  isclwwlknx  30106  clwwlkn1  30111  nmoo0  30862  ubthlem1  30941  ch0pss  31516  pjnorm2  31798  adjval  31961  leop  32194  atcv0eq  32450  xppreima  32718  fmptcof2  32730  xrdifh  32853  hashgt1  32881  isinftm  33242  isunit3  33302  isdrng4  33356  fracerl  33367  dvdsruassoi  33444  dvdsruasso  33445  dvdsrspss  33447  lsmsnorb  33451  ply1degltel  33654  r1pid2OLD  33669  psrbasfsupp  33672  smatrcl  33940  rhmpreimacnlem  34028  ismntop  34170  brfae  34392  eulerpartlemr  34518  eulerpartlemn  34525  reprinrn  34762  reprinfz1  34766  reprdifc  34771  bnj1173  35144  subfacp1lem5  35366  rexxfr3dALT  35821  filnetlem4  36563  mh-infprim1bi  36728  bj-clel3gALT  37355  bj-imdirco  37504  taupilem3  37633  topdifinffinlem  37663  finxpsuclem  37713  matunitlindf  37939  poimirlem22  37963  poimirlem26  37967  poimirlem27  37968  heicant  37976  mbfposadd  37988  itg2addnclem  37992  itg2addnclem2  37993  iblabsnclem  38004  ftc1anclem1  38014  ftc1anclem5  38018  areacirclem5  38033  areacirc  38034  lmclim2  38079  caures  38081  rrnheibor  38158  isdmn3  38395  opelvvdif  38585  ralrnmo  38682  raldmqsmo  38684  brxrn  38704  lrelat  39460  lcvbr  39467  lsatcv0eq  39493  ellkr2  39537  lkr0f  39540  lkreqN  39616  opltn0  39636  op1le  39638  leatb  39738  atlltn0  39752  hlrelat5N  39847  hlrelat  39848  cvrval5  39861  cvrexchlem  39865  atcvr0eq  39872  athgt  39902  1cvrco  39918  islpln5  39981  islvol5  40025  elpadd2at2  40253  cdleme0ex2N  40670  cdleme3  40683  cdleme7  40695  cdlemg33e  41156  dochfln0  41923  lcfl1  41938  lcfls1N  41981  lspindp5  42216  isnacs2  43138  rabrenfdioph  43242  rmxycomplete  43345  expdioph  43451  pwfi2f1o  43524  islnr3  43543  sqrtcvallem1  44058  ntrneixb  44522  clim2cf  46078  funressnfv  47491  focofob  47528  nprmmul1  47987  oddm1evenALTV  48151  oddp1evenALTV  48152  divgcdoddALTV  48158  lco0  48903  lindslinindsimp2lem5  48938  snlindsntor  48947  elbigo2  49028  affinecomb1  49178  itscnhlinecirc02p  49261  reuxfr1dd  49282  iscnrm3lem1  49409