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  3655  reuxfr1d  3718  n0moeu  4318  eldifvsn  4757  xpco  6250  funcnv3  6570  fnssresb  6622  dff1o5  6791  fneqeql2  7001  dffo3  7056  dffo3f  7060  fmptco  7083  fconst4  7170  riota2df  7349  eloprabga  7478  fnwelem  8087  frxp2  8100  xpord2pred  8101  xpord3pred  8108  mptsuppd  8143  mptelixpg  8885  boxcutc  8891  inficl  9352  cantnfle  9600  cantnflem1  9618  ttrclselem2  9655  bnd2  9822  iscard2  9905  alephinit  10024  kmlem2  10081  cfss  10194  fpwwe2lem8  10567  axgroth2  10754  elnnnn0  12461  znnsub  12555  znn0sub  12556  negelrp  12962  xsubge0  13197  divelunit  13431  elfz5  13453  preduz  13587  injresinj  13725  adddivflid  13756  divfl0  13762  hashf1lem1  14396  swrdspsleq  14606  repswsymball  14720  repswsymballbi  14721  2shfti  15022  cnpart  15182  sqrtneglem  15208  rexuz3  15291  rlim  15437  rlim2  15438  clim2c  15447  cvgcmp  15758  bitsmod  16382  bitscmp  16384  pc2dvds  16826  prmreclem4  16866  1arith  16874  imasleval  17480  xpsfrnel  17501  xpsfrnel2  17503  dfiso2  17710  pospropd  18262  latleeqm1  18402  latnlemlt  18407  latnle  18408  ipole  18469  gsumval2a  18588  ismhm0  18693  ghmeqker  19151  gastacos  19218  isslw  19514  slwpss  19518  pgpssslw  19520  fislw  19531  sylow3lem6  19538  dprd2d2  19952  isrnghmmul  20327  isdomn3  20600  lsslss  20843  lsmspsn  20967  zndvds  21435  znleval2  21441  elfilspd  21688  islinds2  21698  islindf2  21699  ismhp3  22005  coe1mul2lem1  22129  eltg3  22825  leordtvallem1  23073  leordtvallem2  23074  lmbrf  23123  cnrest2  23149  xkoccn  23482  hauseqlcld  23509  qtopcn  23577  ordthmeolem  23664  isfbas  23692  fbunfip  23732  fixufil  23785  alexsubALTlem4  23913  ismet2  24197  xblpnfps  24259  xblpnf  24260  blval2  24426  metuel2  24429  dscopn  24437  cnbl0  24637  cnblcld  24638  xrtgioo  24671  mulc1cncf  24774  isclmp  24973  isncvsngp  25025  lmmbrf  25138  iscauf  25156  caucfil  25159  lmclim  25179  evthicc2  25337  volsup  25433  ioombl1lem4  25438  ismbf  25505  ismbfcn  25506  mbfmulc2lem  25524  mbfmax  25526  mbfposr  25529  ismbf3d  25531  mbfimaopnlem  25532  mbfsup  25541  i1fpos  25583  mbfi1fseqlem4  25595  xrge0f  25608  itg2seq  25619  itg2monolem1  25627  itg2gt0  25637  itg2cnlem1  25638  itg2cnlem2  25639  i1fibl  25685  ditgneg  25734  lhop1  25895  r1pid2  26043  fta1  26192  ulm2  26270  pilem1  26337  sineq0  26409  ellogrn  26444  rlimcnp  26851  wilthlem1  26954  sqff1o  27068  logfaclbnd  27109  bposlem1  27171  lgsdilem  27211  lgsabs1  27223  lgsdchrval  27241  lgsquadlem1  27267  lgsquadlem2  27268  zn0subs  28267  iscgrgd  28416  trgcgrg  28418  ltgov  28500  ishlg  28505  lnhl  28518  israg  28600  islnopp  28642  iscgra  28712  isinag  28741  iseqlg  28770  nbupgrel  29248  isuvtx  29298  iscplgredg  29320  rusgrnumwwlkl1  29871  clwlkclwwlk2  29905  isclwwlknx  29938  clwwlkn1  29943  nmoo0  30693  ubthlem1  30772  ch0pss  31347  pjnorm2  31629  adjval  31792  leop  32025  atcv0eq  32281  xppreima  32542  fmptcof2  32554  xrdifh  32676  hashgt1  32706  isinftm  33108  isunit3  33165  isdrng4  33218  fracerl  33229  dvdsruassoi  33328  dvdsruasso  33329  dvdsrspss  33331  lsmsnorb  33335  ply1degltel  33533  r1pid2OLD  33547  smatrcl  33759  rhmpreimacnlem  33847  ismntop  33989  brfae  34211  eulerpartlemr  34338  eulerpartlemn  34345  reprinrn  34582  reprinfz1  34586  reprdifc  34591  bnj1173  34965  subfacp1lem5  35144  rexxfr3dALT  35599  filnetlem4  36342  bj-clel3gALT  37009  bj-imdirco  37151  taupilem3  37280  topdifinffinlem  37308  finxpsuclem  37358  matunitlindf  37585  poimirlem22  37609  poimirlem26  37613  poimirlem27  37614  heicant  37622  mbfposadd  37634  itg2addnclem  37638  itg2addnclem2  37639  iblabsnclem  37650  ftc1anclem1  37660  ftc1anclem5  37664  areacirclem5  37679  areacirc  37680  lmclim2  37725  caures  37727  rrnheibor  37804  isdmn3  38041  opelvvdif  38221  brxrn  38329  lrelat  38980  lcvbr  38987  lsatcv0eq  39013  ellkr2  39057  lkr0f  39060  lkreqN  39136  opltn0  39156  op1le  39158  leatb  39258  atlltn0  39272  hlrelat5N  39368  hlrelat  39369  cvrval5  39382  cvrexchlem  39386  atcvr0eq  39393  athgt  39423  1cvrco  39439  islpln5  39502  islvol5  39546  elpadd2at2  39774  cdleme0ex2N  40191  cdleme3  40204  cdleme7  40216  cdlemg33e  40677  dochfln0  41444  lcfl1  41459  lcfls1N  41502  lspindp5  41737  isnacs2  42667  rabrenfdioph  42775  rmxycomplete  42879  expdioph  42985  pwfi2f1o  43058  islnr3  43077  sqrtcvallem1  43593  ntrneixb  44057  clim2cf  45621  funressnfv  47017  focofob  47054  oddm1evenALTV  47649  oddp1evenALTV  47650  divgcdoddALTV  47656  lco0  48389  lindslinindsimp2lem5  48424  snlindsntor  48433  elbigo2  48514  affinecomb1  48664  itscnhlinecirc02p  48747  reuxfr1dd  48768  iscnrm3lem1  48895