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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm5.3  572  mpbirand  703  3biant1d  1476  elrab3t  3616  reuxfr1d  3680  n0moeu  4287  eldifvsn  4727  xpco  6181  funcnv3  6488  fnssresb  6538  dff1o5  6709  fneqeql2  6906  dffo3  6960  fmptco  6983  fconst4  7072  riota2df  7236  eloprabga  7360  eloprabgaOLD  7361  fnwelem  7943  mptsuppd  7974  mptelixpg  8681  boxcutc  8687  inficl  9114  cantnfle  9359  cantnflem1  9377  bnd2  9582  iscard2  9665  alephinit  9782  kmlem2  9838  cfss  9952  fpwwe2lem8  10325  axgroth2  10512  elnnnn0  12206  znnsub  12296  znn0sub  12297  negelrp  12692  xsubge0  12924  divelunit  13155  elfz5  13177  preduz  13307  injresinj  13436  adddivflid  13466  divfl0  13472  hashf1lem1  14096  hashf1lem1OLD  14097  swrdspsleq  14306  repswsymball  14420  repswsymballbi  14421  2shfti  14719  cnpart  14879  sqrtneglem  14906  rexuz3  14988  rlim  15132  rlim2  15133  clim2c  15142  cvgcmp  15456  bitsmod  16071  bitscmp  16073  pc2dvds  16508  prmreclem4  16548  1arith  16556  imasleval  17169  xpsfrnel  17190  xpsfrnel2  17192  dfiso2  17401  pospropd  17960  latleeqm1  18100  latnlemlt  18105  latnle  18106  ipole  18167  gsumval2a  18284  ghmeqker  18776  gastacos  18831  isslw  19128  slwpss  19132  pgpssslw  19134  fislw  19145  sylow3lem6  19152  dprd2d2  19562  lsslss  20138  lsmspsn  20261  zndvds  20669  znleval2  20675  elfilspd  20920  islinds2  20930  islindf2  20931  ismhp3  21243  coe1mul2lem1  21348  eltg3  22020  leordtvallem1  22269  leordtvallem2  22270  lmbrf  22319  cnrest2  22345  xkoccn  22678  hauseqlcld  22705  qtopcn  22773  ordthmeolem  22860  isfbas  22888  fbunfip  22928  fixufil  22981  alexsubALTlem4  23109  ismet2  23394  xblpnfps  23456  xblpnf  23457  blval2  23624  metuel2  23627  dscopn  23635  cnbl0  23843  cnblcld  23844  xrtgioo  23875  mulc1cncf  23974  isclmp  24166  isncvsngp  24218  lmmbrf  24331  iscauf  24349  caucfil  24352  lmclim  24372  evthicc2  24529  volsup  24625  ioombl1lem4  24630  ismbf  24697  ismbfcn  24698  mbfmulc2lem  24716  mbfmax  24718  mbfposr  24721  ismbf3d  24723  mbfimaopnlem  24724  mbfsup  24733  i1fpos  24776  mbfi1fseqlem4  24788  xrge0f  24801  itg2seq  24812  itg2monolem1  24820  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  i1fibl  24877  ditgneg  24926  lhop1  25083  fta1  25373  ulm2  25449  pilem1  25515  sineq0  25585  ellogrn  25620  rlimcnp  26020  wilthlem1  26122  sqff1o  26236  logfaclbnd  26275  bposlem1  26337  lgsdilem  26377  lgsabs1  26389  lgsdchrval  26407  lgsquadlem1  26433  lgsquadlem2  26434  iscgrgd  26778  trgcgrg  26780  ltgov  26862  ishlg  26867  lnhl  26880  israg  26962  islnopp  27004  iscgra  27074  isinag  27103  iseqlg  27132  nbupgrel  27615  isuvtx  27665  iscplgredg  27687  rusgrnumwwlkl1  28234  clwlkclwwlk2  28268  isclwwlknx  28301  clwwlkn1  28306  nmoo0  29054  ubthlem1  29133  ch0pss  29708  pjnorm2  29990  adjval  30153  leop  30386  atcv0eq  30642  xppreima  30884  fmptcof2  30896  xrdifh  31003  hashgt1  31030  isinftm  31337  lsmsnorb  31481  smatrcl  31648  rhmpreimacnlem  31736  ismntop  31876  brfae  32116  eulerpartlemr  32241  eulerpartlemn  32248  reprinrn  32498  reprinfz1  32502  reprdifc  32507  bnj1173  32882  subfacp1lem5  33046  ttrclselem2  33712  frxp2  33718  xpord2pred  33719  xpord3pred  33725  filnetlem4  34497  bj-clel3gALT  35148  bj-imdirco  35288  taupilem3  35417  topdifinffinlem  35445  finxpsuclem  35495  matunitlindf  35702  poimirlem22  35726  poimirlem26  35730  poimirlem27  35731  heicant  35739  mbfposadd  35751  itg2addnclem  35755  itg2addnclem2  35756  iblabsnclem  35767  ftc1anclem1  35777  ftc1anclem5  35781  areacirclem5  35796  areacirc  35797  lmclim2  35843  caures  35845  rrnheibor  35922  isdmn3  36159  opelvvdif  36325  brxrn  36431  lrelat  36955  lcvbr  36962  lsatcv0eq  36988  ellkr2  37032  lkr0f  37035  lkreqN  37111  opltn0  37131  op1le  37133  leatb  37233  atlltn0  37247  hlrelat5N  37342  hlrelat  37343  cvrval5  37356  cvrexchlem  37360  atcvr0eq  37367  athgt  37397  1cvrco  37413  islpln5  37476  islvol5  37520  elpadd2at2  37748  cdleme0ex2N  38165  cdleme3  38178  cdleme7  38190  cdlemg33e  38651  dochfln0  39418  lcfl1  39433  lcfls1N  39476  lspindp5  39711  isnacs2  40444  rabrenfdioph  40552  rmxycomplete  40655  expdioph  40761  pwfi2f1o  40837  islnr3  40856  isdomn3  40945  sqrtcvallem1  41128  ntrneixb  41594  dffo3f  42606  clim2cf  43081  funressnfv  44424  focofob  44459  oddm1evenALTV  45015  oddp1evenALTV  45016  divgcdoddALTV  45022  ismhm0  45247  isrnghmmul  45339  lco0  45656  lindslinindsimp2lem5  45691  snlindsntor  45700  elbigo2  45786  affinecomb1  45936  itscnhlinecirc02p  46019  iscnrm3lem1  46115