Theorem biantrurd 535

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm5.3  575  mpbirand  705  3biant1d  1474  elrab3t  3681  reuxfr1d  3743  n0moeu  4318  eldifvsn  4732  xpco  6142  funcnv3  6426  fnssresb  6471  dff1o5  6626  fneqeql2  6819  dffo3  6870  fmptco  6893  fconst4  6979  riota2df  7139  eloprabga  7263  fnwelem  7827  mptsuppd  7855  mptelixpg  8501  boxcutc  8507  inficl  8891  cantnfle  9136  cantnflem1  9154  bnd2  9324  iscard2  9407  alephinit  9523  kmlem2  9579  cfss  9689  fpwwe2lem9  10062  axgroth2  10249  elnnnn0  11943  znnsub  12031  znn0sub  12032  negelrp  12425  xsubge0  12657  divelunit  12883  elfz5  12903  preduz  13032  injresinj  13161  adddivflid  13191  divfl0  13197  hashf1lem1  13816  swrdspsleq  14029  repswsymball  14143  repswsymballbi  14144  2shfti  14441  cnpart  14601  sqrtneglem  14628  rexuz3  14710  rlim  14854  rlim2  14855  clim2c  14864  cvgcmp  15173  bitsmod  15787  bitscmp  15789  pc2dvds  16217  prmreclem4  16257  1arith  16265  imasleval  16816  xpsfrnel  16837  xpsfrnel2  16839  dfiso2  17044  latleeqm1  17691  latnlemlt  17696  latnle  17697  pospropd  17746  ipole  17770  gsumval2a  17897  ghmeqker  18387  gastacos  18442  isslw  18735  slwpss  18739  pgpssslw  18741  fislw  18752  sylow3lem6  18759  dprd2d2  19168  lsslss  19735  lsmspsn  19858  mhpinvcl  20341  coe1mul2lem1  20437  zndvds  20698  znleval2  20704  elfilspd  20949  islinds2  20959  islindf2  20960  eltg3  21572  leordtvallem1  21820  leordtvallem2  21821  lmbrf  21870  cnrest2  21896  xkoccn  22229  hauseqlcld  22256  qtopcn  22324  ordthmeolem  22411  isfbas  22439  fbunfip  22479  fixufil  22532  alexsubALTlem4  22660  ismet2  22945  xblpnfps  23007  xblpnf  23008  blval2  23174  metuel2  23177  dscopn  23185  cnbl0  23384  cnblcld  23385  xrtgioo  23416  mulc1cncf  23515  isclmp  23703  isncvsngp  23755  lmmbrf  23867  iscauf  23885  caucfil  23888  lmclim  23908  evthicc2  24063  volsup  24159  ioombl1lem4  24164  ismbf  24231  ismbfcn  24232  mbfmulc2lem  24250  mbfmax  24252  mbfposr  24255  ismbf3d  24257  mbfimaopnlem  24258  mbfsup  24267  i1fpos  24309  mbfi1fseqlem4  24321  xrge0f  24334  itg2seq  24345  itg2monolem1  24353  itg2gt0  24363  itg2cnlem1  24364  itg2cnlem2  24365  i1fibl  24410  ditgneg  24457  lhop1  24613  fta1  24899  ulm2  24975  pilem1  25041  sineq0  25111  ellogrn  25145  rlimcnp  25545  wilthlem1  25647  sqff1o  25761  logfaclbnd  25800  bposlem1  25862  lgsdilem  25902  lgsabs1  25914  lgsdchrval  25932  lgsquadlem1  25958  lgsquadlem2  25959  iscgrgd  26301  trgcgrg  26303  ltgov  26385  ishlg  26390  lnhl  26403  israg  26485  islnopp  26527  iscgra  26597  isinag  26626  iseqlg  26655  nbupgrel  27129  isuvtx  27179  iscplgredg  27201  rusgrnumwwlkl1  27749  clwlkclwwlk2  27783  isclwwlknx  27816  clwwlkn1  27821  nmoo0  28570  ubthlem1  28649  ch0pss  29224  pjnorm2  29506  adjval  29669  leop  29902  atcv0eq  30158  xppreima  30396  fmptcof2  30404  xrdifh  30505  hashgt1  30532  isinftm  30812  lsmsnorb  30947  smatrcl  31063  ismntop  31269  brfae  31509  eulerpartlemr  31634  eulerpartlemn  31641  reprinrn  31891  reprinfz1  31895  reprdifc  31900  bnj1173  32276  subfacp1lem5  32433  etasslt  33276  filnetlem4  33731  taupilem3  34602  topdifinffinlem  34630  finxpsuclem  34680  matunitlindf  34892  poimirlem22  34916  poimirlem26  34920  poimirlem27  34921  heicant  34929  mbfposadd  34941  itg2addnclem  34945  itg2addnclem2  34946  iblabsnclem  34957  ftc1anclem1  34969  ftc1anclem5  34973  areacirclem5  34988  areacirc  34989  lmclim2  35035  caures  35037  rrnheibor  35117  isdmn3  35354  opelvvdif  35522  brxrn  35628  lrelat  36152  lcvbr  36159  lsatcv0eq  36185  ellkr2  36229  lkr0f  36232  lkreqN  36308  opltn0  36328  op1le  36330  leatb  36430  atlltn0  36444  hlrelat5N  36539  hlrelat  36540  cvrval5  36553  cvrexchlem  36557  atcvr0eq  36564  athgt  36594  1cvrco  36610  islpln5  36673  islvol5  36717  elpadd2at2  36945  cdleme0ex2N  37362  cdleme3  37375  cdleme7  37387  cdlemg33e  37848  dochfln0  38615  lcfl1  38630  lcfls1N  38673  lspindp5  38908  isnacs2  39310  rabrenfdioph  39418  rmxycomplete  39521  expdioph  39627  pwfi2f1o  39703  islnr3  39722  isdomn3  39811  ntrneixb  40452  dffo3f  41445  clim2cf  41938  funressnfv  43285  oddm1evenALTV  43847  oddp1evenALTV  43848  divgcdoddALTV  43854  ismhm0  44079  isrnghmmul  44171  lco0  44489  lindslinindsimp2lem5  44524  snlindsntor  44533  elbigo2  44619  affinecomb1  44696  itscnhlinecirc02p  44779