Theorem biantrurd 534

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 530	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  pm5.3  574  mpbirand  706  3biant1d  1479  elrab3t  3683  reuxfr1d  3747  n0moeu  4357  eldifvsn  4801  xpco  6289  funcnv3  6619  fnssresb  6673  dff1o5  6843  fneqeql2  7049  dffo3  7104  fmptco  7127  fconst4  7216  riota2df  7389  eloprabga  7516  eloprabgaOLD  7517  fnwelem  8117  frxp2  8130  xpord2pred  8131  xpord3pred  8138  mptsuppd  8172  mptelixpg  8929  boxcutc  8935  inficl  9420  cantnfle  9666  cantnflem1  9684  ttrclselem2  9721  bnd2  9888  iscard2  9971  alephinit  10090  kmlem2  10146  cfss  10260  fpwwe2lem8  10633  axgroth2  10820  elnnnn0  12515  znnsub  12608  znn0sub  12609  negelrp  13007  xsubge0  13240  divelunit  13471  elfz5  13493  preduz  13623  injresinj  13753  adddivflid  13783  divfl0  13789  hashf1lem1  14415  hashf1lem1OLD  14416  swrdspsleq  14615  repswsymball  14729  repswsymballbi  14730  2shfti  15027  cnpart  15187  sqrtneglem  15213  rexuz3  15295  rlim  15439  rlim2  15440  clim2c  15449  cvgcmp  15762  bitsmod  16377  bitscmp  16379  pc2dvds  16812  prmreclem4  16852  1arith  16860  imasleval  17487  xpsfrnel  17508  xpsfrnel2  17510  dfiso2  17719  pospropd  18280  latleeqm1  18420  latnlemlt  18425  latnle  18426  ipole  18487  gsumval2a  18604  ghmeqker  19119  gastacos  19174  isslw  19476  slwpss  19480  pgpssslw  19482  fislw  19493  sylow3lem6  19500  dprd2d2  19914  lsslss  20572  lsmspsn  20695  zndvds  21105  znleval2  21111  elfilspd  21358  islinds2  21368  islindf2  21369  ismhp3  21686  coe1mul2lem1  21789  eltg3  22465  leordtvallem1  22714  leordtvallem2  22715  lmbrf  22764  cnrest2  22790  xkoccn  23123  hauseqlcld  23150  qtopcn  23218  ordthmeolem  23305  isfbas  23333  fbunfip  23373  fixufil  23426  alexsubALTlem4  23554  ismet2  23839  xblpnfps  23901  xblpnf  23902  blval2  24071  metuel2  24074  dscopn  24082  cnbl0  24290  cnblcld  24291  xrtgioo  24322  mulc1cncf  24421  isclmp  24613  isncvsngp  24666  lmmbrf  24779  iscauf  24797  caucfil  24800  lmclim  24820  evthicc2  24977  volsup  25073  ioombl1lem4  25078  ismbf  25145  ismbfcn  25146  mbfmulc2lem  25164  mbfmax  25166  mbfposr  25169  ismbf3d  25171  mbfimaopnlem  25172  mbfsup  25181  i1fpos  25224  mbfi1fseqlem4  25236  xrge0f  25249  itg2seq  25260  itg2monolem1  25268  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  i1fibl  25325  ditgneg  25374  lhop1  25531  fta1  25821  ulm2  25897  pilem1  25963  sineq0  26033  ellogrn  26068  rlimcnp  26470  wilthlem1  26572  sqff1o  26686  logfaclbnd  26725  bposlem1  26787  lgsdilem  26827  lgsabs1  26839  lgsdchrval  26857  lgsquadlem1  26883  lgsquadlem2  26884  iscgrgd  27764  trgcgrg  27766  ltgov  27848  ishlg  27853  lnhl  27866  israg  27948  islnopp  27990  iscgra  28060  isinag  28089  iseqlg  28118  nbupgrel  28602  isuvtx  28652  iscplgredg  28674  rusgrnumwwlkl1  29222  clwlkclwwlk2  29256  isclwwlknx  29289  clwwlkn1  29294  nmoo0  30044  ubthlem1  30123  ch0pss  30698  pjnorm2  30980  adjval  31143  leop  31376  atcv0eq  31632  xppreima  31871  fmptcof2  31882  xrdifh  31991  hashgt1  32020  isinftm  32327  isdrng4  32395  dvdsruassoi  32489  dvdsruasso  32490  dvdsrspss  32491  lsmsnorb  32501  ply1degltel  32666  smatrcl  32776  rhmpreimacnlem  32864  ismntop  33006  brfae  33246  eulerpartlemr  33373  eulerpartlemn  33380  reprinrn  33630  reprinfz1  33634  reprdifc  33639  bnj1173  34013  subfacp1lem5  34175  filnetlem4  35266  bj-clel3gALT  35929  bj-imdirco  36071  taupilem3  36200  topdifinffinlem  36228  finxpsuclem  36278  matunitlindf  36486  poimirlem22  36510  poimirlem26  36514  poimirlem27  36515  heicant  36523  mbfposadd  36535  itg2addnclem  36539  itg2addnclem2  36540  iblabsnclem  36551  ftc1anclem1  36561  ftc1anclem5  36565  areacirclem5  36580  areacirc  36581  lmclim2  36626  caures  36628  rrnheibor  36705  isdmn3  36942  opelvvdif  37127  brxrn  37244  lrelat  37884  lcvbr  37891  lsatcv0eq  37917  ellkr2  37961  lkr0f  37964  lkreqN  38040  opltn0  38060  op1le  38062  leatb  38162  atlltn0  38176  hlrelat5N  38272  hlrelat  38273  cvrval5  38286  cvrexchlem  38290  atcvr0eq  38297  athgt  38327  1cvrco  38343  islpln5  38406  islvol5  38450  elpadd2at2  38678  cdleme0ex2N  39095  cdleme3  39108  cdleme7  39120  cdlemg33e  39581  dochfln0  40348  lcfl1  40363  lcfls1N  40406  lspindp5  40641  isnacs2  41444  rabrenfdioph  41552  rmxycomplete  41656  expdioph  41762  pwfi2f1o  41838  islnr3  41857  isdomn3  41946  sqrtcvallem1  42382  ntrneixb  42846  dffo3f  43877  clim2cf  44366  funressnfv  45753  focofob  45788  oddm1evenALTV  46343  oddp1evenALTV  46344  divgcdoddALTV  46350  ismhm0  46575  isrnghmmul  46691  lco0  47108  lindslinindsimp2lem5  47143  snlindsntor  47152  elbigo2  47238  affinecomb1  47388  itscnhlinecirc02p  47471  iscnrm3lem1  47566