Theorem biantrurd 533

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

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

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 397

This theorem is referenced by:  pm5.3  573  mpbirand  704  3biant1d  1477  elrab3t  3624  reuxfr1d  3686  n0moeu  4291  eldifvsn  4731  xpco  6196  funcnv3  6511  fnssresb  6563  dff1o5  6734  fneqeql2  6933  dffo3  6987  fmptco  7010  fconst4  7099  riota2df  7265  eloprabga  7391  eloprabgaOLD  7392  fnwelem  7981  mptsuppd  8012  mptelixpg  8732  boxcutc  8738  inficl  9193  cantnfle  9438  cantnflem1  9456  ttrclselem2  9493  bnd2  9660  iscard2  9743  alephinit  9860  kmlem2  9916  cfss  10030  fpwwe2lem8  10403  axgroth2  10590  elnnnn0  12285  znnsub  12375  znn0sub  12376  negelrp  12772  xsubge0  13004  divelunit  13235  elfz5  13257  preduz  13387  injresinj  13517  adddivflid  13547  divfl0  13553  hashf1lem1  14177  hashf1lem1OLD  14178  swrdspsleq  14387  repswsymball  14501  repswsymballbi  14502  2shfti  14800  cnpart  14960  sqrtneglem  14987  rexuz3  15069  rlim  15213  rlim2  15214  clim2c  15223  cvgcmp  15537  bitsmod  16152  bitscmp  16154  pc2dvds  16589  prmreclem4  16629  1arith  16637  imasleval  17261  xpsfrnel  17282  xpsfrnel2  17284  dfiso2  17493  pospropd  18054  latleeqm1  18194  latnlemlt  18199  latnle  18200  ipole  18261  gsumval2a  18378  ghmeqker  18870  gastacos  18925  isslw  19222  slwpss  19226  pgpssslw  19228  fislw  19239  sylow3lem6  19246  dprd2d2  19656  lsslss  20232  lsmspsn  20355  zndvds  20766  znleval2  20772  elfilspd  21019  islinds2  21029  islindf2  21030  ismhp3  21342  coe1mul2lem1  21447  eltg3  22121  leordtvallem1  22370  leordtvallem2  22371  lmbrf  22420  cnrest2  22446  xkoccn  22779  hauseqlcld  22806  qtopcn  22874  ordthmeolem  22961  isfbas  22989  fbunfip  23029  fixufil  23082  alexsubALTlem4  23210  ismet2  23495  xblpnfps  23557  xblpnf  23558  blval2  23727  metuel2  23730  dscopn  23738  cnbl0  23946  cnblcld  23947  xrtgioo  23978  mulc1cncf  24077  isclmp  24269  isncvsngp  24322  lmmbrf  24435  iscauf  24453  caucfil  24456  lmclim  24476  evthicc2  24633  volsup  24729  ioombl1lem4  24734  ismbf  24801  ismbfcn  24802  mbfmulc2lem  24820  mbfmax  24822  mbfposr  24825  ismbf3d  24827  mbfimaopnlem  24828  mbfsup  24837  i1fpos  24880  mbfi1fseqlem4  24892  xrge0f  24905  itg2seq  24916  itg2monolem1  24924  itg2gt0  24934  itg2cnlem1  24935  itg2cnlem2  24936  i1fibl  24981  ditgneg  25030  lhop1  25187  fta1  25477  ulm2  25553  pilem1  25619  sineq0  25689  ellogrn  25724  rlimcnp  26124  wilthlem1  26226  sqff1o  26340  logfaclbnd  26379  bposlem1  26441  lgsdilem  26481  lgsabs1  26493  lgsdchrval  26511  lgsquadlem1  26537  lgsquadlem2  26538  iscgrgd  26883  trgcgrg  26885  ltgov  26967  ishlg  26972  lnhl  26985  israg  27067  islnopp  27109  iscgra  27179  isinag  27208  iseqlg  27237  nbupgrel  27721  isuvtx  27771  iscplgredg  27793  rusgrnumwwlkl1  28342  clwlkclwwlk2  28376  isclwwlknx  28409  clwwlkn1  28414  nmoo0  29162  ubthlem1  29241  ch0pss  29816  pjnorm2  30098  adjval  30261  leop  30494  atcv0eq  30750  xppreima  30992  fmptcof2  31003  xrdifh  31110  hashgt1  31137  isinftm  31444  lsmsnorb  31588  smatrcl  31755  rhmpreimacnlem  31843  ismntop  31985  brfae  32225  eulerpartlemr  32350  eulerpartlemn  32357  reprinrn  32607  reprinfz1  32611  reprdifc  32616  bnj1173  32991  subfacp1lem5  33155  frxp2  33800  xpord2pred  33801  xpord3pred  33807  filnetlem4  34579  bj-clel3gALT  35230  bj-imdirco  35370  taupilem3  35499  topdifinffinlem  35527  finxpsuclem  35577  matunitlindf  35784  poimirlem22  35808  poimirlem26  35812  poimirlem27  35813  heicant  35821  mbfposadd  35833  itg2addnclem  35837  itg2addnclem2  35838  iblabsnclem  35849  ftc1anclem1  35859  ftc1anclem5  35863  areacirclem5  35878  areacirc  35879  lmclim2  35925  caures  35927  rrnheibor  36004  isdmn3  36241  opelvvdif  36406  brxrn  36511  lrelat  37035  lcvbr  37042  lsatcv0eq  37068  ellkr2  37112  lkr0f  37115  lkreqN  37191  opltn0  37211  op1le  37213  leatb  37313  atlltn0  37327  hlrelat5N  37422  hlrelat  37423  cvrval5  37436  cvrexchlem  37440  atcvr0eq  37447  athgt  37477  1cvrco  37493  islpln5  37556  islvol5  37600  elpadd2at2  37828  cdleme0ex2N  38245  cdleme3  38258  cdleme7  38270  cdlemg33e  38731  dochfln0  39498  lcfl1  39513  lcfls1N  39556  lspindp5  39791  isnacs2  40535  rabrenfdioph  40643  rmxycomplete  40746  expdioph  40852  pwfi2f1o  40928  islnr3  40947  isdomn3  41036  sqrtcvallem1  41246  ntrneixb  41712  dffo3f  42724  clim2cf  43198  funressnfv  44548  focofob  44583  oddm1evenALTV  45138  oddp1evenALTV  45139  divgcdoddALTV  45145  ismhm0  45370  isrnghmmul  45462  lco0  45779  lindslinindsimp2lem5  45814  snlindsntor  45823  elbigo2  45909  affinecomb1  46059  itscnhlinecirc02p  46142  iscnrm3lem1  46238