Theorem biantrurd 536

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  pm5.3  576  mpbirand  706  3biant1d  1475  elrab3t  3627  reuxfr1d  3689  n0moeu  4270  eldifvsn  4690  xpco  6108  funcnv3  6394  fnssresb  6441  dff1o5  6599  fneqeql2  6794  dffo3  6845  fmptco  6868  fconst4  6954  riota2df  7116  eloprabga  7240  fnwelem  7808  mptsuppd  7836  mptelixpg  8482  boxcutc  8488  inficl  8873  cantnfle  9118  cantnflem1  9136  bnd2  9306  iscard2  9389  alephinit  9506  kmlem2  9562  cfss  9676  fpwwe2lem9  10049  axgroth2  10236  elnnnn0  11928  znnsub  12016  znn0sub  12017  negelrp  12410  xsubge0  12642  divelunit  12872  elfz5  12894  preduz  13024  injresinj  13153  adddivflid  13183  divfl0  13189  hashf1lem1  13809  swrdspsleq  14018  repswsymball  14132  repswsymballbi  14133  2shfti  14431  cnpart  14591  sqrtneglem  14618  rexuz3  14700  rlim  14844  rlim2  14845  clim2c  14854  cvgcmp  15163  bitsmod  15775  bitscmp  15777  pc2dvds  16205  prmreclem4  16245  1arith  16253  imasleval  16806  xpsfrnel  16827  xpsfrnel2  16829  dfiso2  17034  latleeqm1  17681  latnlemlt  17686  latnle  17687  pospropd  17736  ipole  17760  gsumval2a  17887  ghmeqker  18377  gastacos  18432  isslw  18725  slwpss  18729  pgpssslw  18731  fislw  18742  sylow3lem6  18749  dprd2d2  19159  lsslss  19726  lsmspsn  19849  zndvds  20241  znleval2  20247  elfilspd  20492  islinds2  20502  islindf2  20503  coe1mul2lem1  20896  eltg3  21567  leordtvallem1  21815  leordtvallem2  21816  lmbrf  21865  cnrest2  21891  xkoccn  22224  hauseqlcld  22251  qtopcn  22319  ordthmeolem  22406  isfbas  22434  fbunfip  22474  fixufil  22527  alexsubALTlem4  22655  ismet2  22940  xblpnfps  23002  xblpnf  23003  blval2  23169  metuel2  23172  dscopn  23180  cnbl0  23379  cnblcld  23380  xrtgioo  23411  mulc1cncf  23510  isclmp  23702  isncvsngp  23754  lmmbrf  23866  iscauf  23884  caucfil  23887  lmclim  23907  evthicc2  24064  volsup  24160  ioombl1lem4  24165  ismbf  24232  ismbfcn  24233  mbfmulc2lem  24251  mbfmax  24253  mbfposr  24256  ismbf3d  24258  mbfimaopnlem  24259  mbfsup  24268  i1fpos  24310  mbfi1fseqlem4  24322  xrge0f  24335  itg2seq  24346  itg2monolem1  24354  itg2gt0  24364  itg2cnlem1  24365  itg2cnlem2  24366  i1fibl  24411  ditgneg  24460  lhop1  24617  fta1  24904  ulm2  24980  pilem1  25046  sineq0  25116  ellogrn  25151  rlimcnp  25551  wilthlem1  25653  sqff1o  25767  logfaclbnd  25806  bposlem1  25868  lgsdilem  25908  lgsabs1  25920  lgsdchrval  25938  lgsquadlem1  25964  lgsquadlem2  25965  iscgrgd  26307  trgcgrg  26309  ltgov  26391  ishlg  26396  lnhl  26409  israg  26491  islnopp  26533  iscgra  26603  isinag  26632  iseqlg  26661  nbupgrel  27135  isuvtx  27185  iscplgredg  27207  rusgrnumwwlkl1  27754  clwlkclwwlk2  27788  isclwwlknx  27821  clwwlkn1  27826  nmoo0  28574  ubthlem1  28653  ch0pss  29228  pjnorm2  29510  adjval  29673  leop  29906  atcv0eq  30162  xppreima  30408  fmptcof2  30420  xrdifh  30529  hashgt1  30556  isinftm  30860  lsmsnorb  30999  smatrcl  31149  rhmpreimacnlem  31237  ismntop  31377  brfae  31617  eulerpartlemr  31742  eulerpartlemn  31749  reprinrn  31999  reprinfz1  32003  reprdifc  32008  bnj1173  32384  subfacp1lem5  32544  etasslt  33387  filnetlem4  33842  bj-imdirco  34605  taupilem3  34733  topdifinffinlem  34764  finxpsuclem  34814  matunitlindf  35055  poimirlem22  35079  poimirlem26  35083  poimirlem27  35084  heicant  35092  mbfposadd  35104  itg2addnclem  35108  itg2addnclem2  35109  iblabsnclem  35120  ftc1anclem1  35130  ftc1anclem5  35134  areacirclem5  35149  areacirc  35150  lmclim2  35196  caures  35198  rrnheibor  35275  isdmn3  35512  opelvvdif  35680  brxrn  35786  lrelat  36310  lcvbr  36317  lsatcv0eq  36343  ellkr2  36387  lkr0f  36390  lkreqN  36466  opltn0  36486  op1le  36488  leatb  36588  atlltn0  36602  hlrelat5N  36697  hlrelat  36698  cvrval5  36711  cvrexchlem  36715  atcvr0eq  36722  athgt  36752  1cvrco  36768  islpln5  36831  islvol5  36875  elpadd2at2  37103  cdleme0ex2N  37520  cdleme3  37533  cdleme7  37545  cdlemg33e  38006  dochfln0  38773  lcfl1  38788  lcfls1N  38831  lspindp5  39066  isnacs2  39647  rabrenfdioph  39755  rmxycomplete  39858  expdioph  39964  pwfi2f1o  40040  islnr3  40059  isdomn3  40148  sqrtcvallem1  40331  ntrneixb  40798  dffo3f  41806  clim2cf  42292  funressnfv  43635  oddm1evenALTV  44193  oddp1evenALTV  44194  divgcdoddALTV  44200  ismhm0  44425  isrnghmmul  44517  lco0  44836  lindslinindsimp2lem5  44871  snlindsntor  44880  elbigo2  44966  affinecomb1  45116  itscnhlinecirc02p  45199