Theorem biantrurd 534

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

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

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 398

This theorem is referenced by:  pm5.3  574  mpbirand  706  3biant1d  1479  elrab3t  3682  reuxfr1d  3746  n0moeu  4356  eldifvsn  4800  xpco  6286  funcnv3  6616  fnssresb  6670  dff1o5  6840  fneqeql2  7046  dffo3  7101  fmptco  7124  fconst4  7213  riota2df  7386  eloprabga  7513  eloprabgaOLD  7514  fnwelem  8114  frxp2  8127  xpord2pred  8128  xpord3pred  8135  mptsuppd  8169  mptelixpg  8926  boxcutc  8932  inficl  9417  cantnfle  9663  cantnflem1  9681  ttrclselem2  9718  bnd2  9885  iscard2  9968  alephinit  10087  kmlem2  10143  cfss  10257  fpwwe2lem8  10630  axgroth2  10817  elnnnn0  12512  znnsub  12605  znn0sub  12606  negelrp  13004  xsubge0  13237  divelunit  13468  elfz5  13490  preduz  13620  injresinj  13750  adddivflid  13780  divfl0  13786  hashf1lem1  14412  hashf1lem1OLD  14413  swrdspsleq  14612  repswsymball  14726  repswsymballbi  14727  2shfti  15024  cnpart  15184  sqrtneglem  15210  rexuz3  15292  rlim  15436  rlim2  15437  clim2c  15446  cvgcmp  15759  bitsmod  16374  bitscmp  16376  pc2dvds  16809  prmreclem4  16849  1arith  16857  imasleval  17484  xpsfrnel  17505  xpsfrnel2  17507  dfiso2  17716  pospropd  18277  latleeqm1  18417  latnlemlt  18422  latnle  18423  ipole  18484  gsumval2a  18601  ghmeqker  19114  gastacos  19169  isslw  19471  slwpss  19475  pgpssslw  19477  fislw  19488  sylow3lem6  19495  dprd2d2  19909  lsslss  20565  lsmspsn  20688  zndvds  21097  znleval2  21103  elfilspd  21350  islinds2  21360  islindf2  21361  ismhp3  21678  coe1mul2lem1  21781  eltg3  22457  leordtvallem1  22706  leordtvallem2  22707  lmbrf  22756  cnrest2  22782  xkoccn  23115  hauseqlcld  23142  qtopcn  23210  ordthmeolem  23297  isfbas  23325  fbunfip  23365  fixufil  23418  alexsubALTlem4  23546  ismet2  23831  xblpnfps  23893  xblpnf  23894  blval2  24063  metuel2  24066  dscopn  24074  cnbl0  24282  cnblcld  24283  xrtgioo  24314  mulc1cncf  24413  isclmp  24605  isncvsngp  24658  lmmbrf  24771  iscauf  24789  caucfil  24792  lmclim  24812  evthicc2  24969  volsup  25065  ioombl1lem4  25070  ismbf  25137  ismbfcn  25138  mbfmulc2lem  25156  mbfmax  25158  mbfposr  25161  ismbf3d  25163  mbfimaopnlem  25164  mbfsup  25173  i1fpos  25216  mbfi1fseqlem4  25228  xrge0f  25241  itg2seq  25252  itg2monolem1  25260  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  i1fibl  25317  ditgneg  25366  lhop1  25523  fta1  25813  ulm2  25889  pilem1  25955  sineq0  26025  ellogrn  26060  rlimcnp  26460  wilthlem1  26562  sqff1o  26676  logfaclbnd  26715  bposlem1  26777  lgsdilem  26817  lgsabs1  26829  lgsdchrval  26847  lgsquadlem1  26873  lgsquadlem2  26874  iscgrgd  27754  trgcgrg  27756  ltgov  27838  ishlg  27843  lnhl  27856  israg  27938  islnopp  27980  iscgra  28050  isinag  28079  iseqlg  28108  nbupgrel  28592  isuvtx  28642  iscplgredg  28664  rusgrnumwwlkl1  29212  clwlkclwwlk2  29246  isclwwlknx  29279  clwwlkn1  29284  nmoo0  30032  ubthlem1  30111  ch0pss  30686  pjnorm2  30968  adjval  31131  leop  31364  atcv0eq  31620  xppreima  31859  fmptcof2  31870  xrdifh  31979  hashgt1  32008  isinftm  32315  isdrng4  32384  dvdsruassoi  32478  dvdsruasso  32479  dvdsrspss  32480  lsmsnorb  32490  ply1degltel  32655  smatrcl  32765  rhmpreimacnlem  32853  ismntop  32995  brfae  33235  eulerpartlemr  33362  eulerpartlemn  33369  reprinrn  33619  reprinfz1  33623  reprdifc  33628  bnj1173  34002  subfacp1lem5  34164  filnetlem4  35255  bj-clel3gALT  35918  bj-imdirco  36060  taupilem3  36189  topdifinffinlem  36217  finxpsuclem  36267  matunitlindf  36475  poimirlem22  36499  poimirlem26  36503  poimirlem27  36504  heicant  36512  mbfposadd  36524  itg2addnclem  36528  itg2addnclem2  36529  iblabsnclem  36540  ftc1anclem1  36550  ftc1anclem5  36554  areacirclem5  36569  areacirc  36570  lmclim2  36615  caures  36617  rrnheibor  36694  isdmn3  36931  opelvvdif  37116  brxrn  37233  lrelat  37873  lcvbr  37880  lsatcv0eq  37906  ellkr2  37950  lkr0f  37953  lkreqN  38029  opltn0  38049  op1le  38051  leatb  38151  atlltn0  38165  hlrelat5N  38261  hlrelat  38262  cvrval5  38275  cvrexchlem  38279  atcvr0eq  38286  athgt  38316  1cvrco  38332  islpln5  38395  islvol5  38439  elpadd2at2  38667  cdleme0ex2N  39084  cdleme3  39097  cdleme7  39109  cdlemg33e  39570  dochfln0  40337  lcfl1  40352  lcfls1N  40395  lspindp5  40630  isnacs2  41430  rabrenfdioph  41538  rmxycomplete  41642  expdioph  41748  pwfi2f1o  41824  islnr3  41843  isdomn3  41932  sqrtcvallem1  42368  ntrneixb  42832  dffo3f  43863  clim2cf  44353  funressnfv  45740  focofob  45775  oddm1evenALTV  46330  oddp1evenALTV  46331  divgcdoddALTV  46337  ismhm0  46562  isrnghmmul  46677  lco0  47062  lindslinindsimp2lem5  47097  snlindsntor  47106  elbigo2  47192  affinecomb1  47342  itscnhlinecirc02p  47425  iscnrm3lem1  47520