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

This theorem is referenced by:  pm5.3  572  mpbirand  707  3biant1d  1480  elrab3t  3670  reuxfr1d  3733  n0moeu  4334  eldifvsn  4773  xpco  6278  funcnv3  6605  fnssresb  6659  dff1o5  6826  fneqeql2  7036  dffo3  7091  dffo3f  7095  fmptco  7118  fconst4  7205  riota2df  7383  eloprabga  7514  fnwelem  8128  frxp2  8141  xpord2pred  8142  xpord3pred  8149  mptsuppd  8184  mptelixpg  8947  boxcutc  8953  inficl  9435  cantnfle  9683  cantnflem1  9701  ttrclselem2  9738  bnd2  9905  iscard2  9988  alephinit  10107  kmlem2  10164  cfss  10277  fpwwe2lem8  10650  axgroth2  10837  elnnnn0  12542  znnsub  12636  znn0sub  12637  negelrp  13040  xsubge0  13275  divelunit  13509  elfz5  13531  preduz  13665  injresinj  13802  adddivflid  13833  divfl0  13839  hashf1lem1  14471  swrdspsleq  14681  repswsymball  14795  repswsymballbi  14796  2shfti  15097  cnpart  15257  sqrtneglem  15283  rexuz3  15365  rlim  15509  rlim2  15510  clim2c  15519  cvgcmp  15830  bitsmod  16453  bitscmp  16455  pc2dvds  16897  prmreclem4  16937  1arith  16945  imasleval  17553  xpsfrnel  17574  xpsfrnel2  17576  dfiso2  17783  pospropd  18335  latleeqm1  18475  latnlemlt  18480  latnle  18481  ipole  18542  gsumval2a  18661  ismhm0  18766  ghmeqker  19224  gastacos  19291  isslw  19587  slwpss  19591  pgpssslw  19593  fislw  19604  sylow3lem6  19611  dprd2d2  20025  isrnghmmul  20400  isdomn3  20673  lsslss  20916  lsmspsn  21040  zndvds  21508  znleval2  21514  elfilspd  21761  islinds2  21771  islindf2  21772  ismhp3  22078  coe1mul2lem1  22202  eltg3  22898  leordtvallem1  23146  leordtvallem2  23147  lmbrf  23196  cnrest2  23222  xkoccn  23555  hauseqlcld  23582  qtopcn  23650  ordthmeolem  23737  isfbas  23765  fbunfip  23805  fixufil  23858  alexsubALTlem4  23986  ismet2  24270  xblpnfps  24332  xblpnf  24333  blval2  24499  metuel2  24502  dscopn  24510  cnbl0  24710  cnblcld  24711  xrtgioo  24744  mulc1cncf  24847  isclmp  25046  isncvsngp  25099  lmmbrf  25212  iscauf  25230  caucfil  25233  lmclim  25253  evthicc2  25411  volsup  25507  ioombl1lem4  25512  ismbf  25579  ismbfcn  25580  mbfmulc2lem  25598  mbfmax  25600  mbfposr  25603  ismbf3d  25605  mbfimaopnlem  25606  mbfsup  25615  i1fpos  25657  mbfi1fseqlem4  25669  xrge0f  25682  itg2seq  25693  itg2monolem1  25701  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  i1fibl  25759  ditgneg  25808  lhop1  25969  r1pid2  26117  fta1  26266  ulm2  26344  pilem1  26411  sineq0  26483  ellogrn  26518  rlimcnp  26925  wilthlem1  27028  sqff1o  27142  logfaclbnd  27183  bposlem1  27245  lgsdilem  27285  lgsabs1  27297  lgsdchrval  27315  lgsquadlem1  27341  lgsquadlem2  27342  zn0subs  28306  iscgrgd  28438  trgcgrg  28440  ltgov  28522  ishlg  28527  lnhl  28540  israg  28622  islnopp  28664  iscgra  28734  isinag  28763  iseqlg  28792  nbupgrel  29270  isuvtx  29320  iscplgredg  29342  rusgrnumwwlkl1  29896  clwlkclwwlk2  29930  isclwwlknx  29963  clwwlkn1  29968  nmoo0  30718  ubthlem1  30797  ch0pss  31372  pjnorm2  31654  adjval  31817  leop  32050  atcv0eq  32306  xppreima  32569  fmptcof2  32581  xrdifh  32703  hashgt1  32733  isinftm  33125  isunit3  33182  isdrng4  33235  fracerl  33246  dvdsruassoi  33345  dvdsruasso  33346  dvdsrspss  33348  lsmsnorb  33352  ply1degltel  33550  r1pid2OLD  33564  smatrcl  33773  rhmpreimacnlem  33861  ismntop  34003  brfae  34225  eulerpartlemr  34352  eulerpartlemn  34359  reprinrn  34596  reprinfz1  34600  reprdifc  34605  bnj1173  34979  subfacp1lem5  35152  rexxfr3dALT  35607  filnetlem4  36345  bj-clel3gALT  37012  bj-imdirco  37154  taupilem3  37283  topdifinffinlem  37311  finxpsuclem  37361  matunitlindf  37588  poimirlem22  37612  poimirlem26  37616  poimirlem27  37617  heicant  37625  mbfposadd  37637  itg2addnclem  37641  itg2addnclem2  37642  iblabsnclem  37653  ftc1anclem1  37663  ftc1anclem5  37667  areacirclem5  37682  areacirc  37683  lmclim2  37728  caures  37730  rrnheibor  37807  isdmn3  38044  opelvvdif  38223  brxrn  38338  lrelat  38978  lcvbr  38985  lsatcv0eq  39011  ellkr2  39055  lkr0f  39058  lkreqN  39134  opltn0  39154  op1le  39156  leatb  39256  atlltn0  39270  hlrelat5N  39366  hlrelat  39367  cvrval5  39380  cvrexchlem  39384  atcvr0eq  39391  athgt  39421  1cvrco  39437  islpln5  39500  islvol5  39544  elpadd2at2  39772  cdleme0ex2N  40189  cdleme3  40202  cdleme7  40214  cdlemg33e  40675  dochfln0  41442  lcfl1  41457  lcfls1N  41500  lspindp5  41735  isnacs2  42676  rabrenfdioph  42784  rmxycomplete  42888  expdioph  42994  pwfi2f1o  43067  islnr3  43086  sqrtcvallem1  43602  ntrneixb  44066  clim2cf  45627  funressnfv  47020  focofob  47057  oddm1evenALTV  47637  oddp1evenALTV  47638  divgcdoddALTV  47644  lco0  48351  lindslinindsimp2lem5  48386  snlindsntor  48395  elbigo2  48480  affinecomb1  48630  itscnhlinecirc02p  48713  reuxfr1dd  48733  iscnrm3lem1  48856