Theorem biantrurd 541

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

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

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 401

This theorem is referenced by:  pm5.3  582  mpbirand  719  3biant1d  1506  elrab3t  3658  reuxfr1d  3722  n0moeu  4321  eldifvsn  4766  xpco  6288  funcnv3  6604  fnssresb  6655  dff1o5  6828  fneqeql2  7040  dffo3  7095  dffo3f  7099  fmptco  7123  fconst4  7210  riota2df  7388  eloprabga  7517  fnwelem  8123  frxp2  8136  xpord2pred  8137  xpord3pred  8144  mptsuppd  8179  mptelixpg  8929  boxcutc  8935  inficl  9381  cantnfle  9636  cantnflem1  9654  ttrclselem2  9691  bnd2  9875  iscard2  9958  alephinit  10075  kmlem2  10131  cfss  10245  fpwwe2lem8  10619  axgroth2  10806  elnnnn0  12543  znnsub  12636  znn0sub  12637  negelrp  13047  xsubge0  13283  divelunit  13517  elfz5  13540  preduz  13674  injresinj  13816  adddivflid  13847  divfl0  13853  hashf1lem1  14488  swrdspsleq  14699  repswsymball  14812  repswsymballbi  14813  2shfti  15113  cnpart  15287  sqrtneglem  15313  rexuz3  15396  rlim  15542  rlim2  15543  clim2c  15552  cvgcmp  15864  bitsmod  16490  bitscmp  16492  pc2dvds  16935  prmreclem4  16975  1arith  16983  imasleval  17591  xpsfrnel  17612  xpsfrnel2  17614  dfiso2  17825  pospropd  18377  latleeqm1  18519  latnlemlt  18524  latnle  18525  ipole  18586  gsumval2a  18739  ismhm0  18844  ghmeqker  19309  gastacos  19376  isslw  19674  slwpss  19678  pgpssslw  19680  fislw  19691  sylow3lem6  19698  dprd2d2  20112  isrnghmmul  20520  isdomn3  20795  lsslss  21056  lsmspsn  21179  zndvds  21664  znleval2  21670  elfilspd  21918  islinds2  21928  islindf2  21929  ismhp3  22270  coe1mul2lem1  22393  eltg3  23084  leordtvallem1  23332  leordtvallem2  23333  lmbrf  23382  cnrest2  23408  xkoccn  23741  hauseqlcld  23768  qtopcn  23836  ordthmeolem  23923  isfbas  23951  fbunfip  23991  fixufil  24044  alexsubALTlem4  24172  ismet2  24455  xblpnfps  24517  xblpnf  24518  blval2  24684  metuel2  24687  dscopn  24695  cnbl0  24895  cnblcld  24896  xrtgioo  24929  mulc1cncf  25029  isclmp  25221  isncvsngp  25273  lmmbrf  25386  iscauf  25404  caucfil  25407  lmclim  25427  evthicc2  25584  volsup  25680  ioombl1lem4  25685  ismbf  25752  ismbfcn  25753  mbfmulc2lem  25771  mbfmax  25773  mbfposr  25776  ismbf3d  25778  mbfimaopnlem  25779  mbfsup  25788  i1fpos  25830  mbfi1fseqlem4  25842  xrge0f  25855  itg2seq  25866  itg2monolem1  25874  itg2gt0  25884  itg2cnlem1  25885  itg2cnlem2  25886  i1fibl  25932  ditgneg  25981  lhop1  26138  r1pid2  26284  fta1  26434  ulm2  26510  pilem1  26576  sineq0  26651  ellogrn  26686  rlimcnp  27092  wilthlem1  27194  sqff1o  27308  logfaclbnd  27348  bposlem1  27410  lgsdilem  27450  lgsabs1  27462  lgsdchrval  27480  lgsquadlem1  27506  lgsquadlem2  27507  sltssnb  27924  zn0subs  28558  iscgrgd  28744  trgcgrg  28746  ltgov  28828  ishlg  28833  lnhl  28846  israg  28932  islnopp  28975  elplng  29016  plngcplem  29021  iscgra  29073  isinag  29106  iseqlg  29135  nbupgrel  29632  isuvtx  29682  iscplgredg  29704  rusgrnumwwlkl1  30257  clwlkclwwlk2  30291  isclwwlknx  30324  clwwlkn1  30329  nmoo0  31080  ubthlem1  31159  ch0pss  31734  pjnorm2  32016  adjval  32179  leop  32412  atcv0eq  32668  xppreima  32927  fmptcof2  32939  xrdifh  33062  hashgt1  33090  isinftm  33438  isunit3  33497  rlocisunit  33533  isdrng4  33555  fracerl  33566  dvdsruassoi  33637  dvdsruasso  33638  dvdsrspss  33640  lsmsnorb  33644  ply1degltel  33825  psrbasfsupp  33842  smatrcl  34127  rhmpreimacnlem  34215  ismntop  34357  brfae  34579  eulerpartlemr  34705  eulerpartlemn  34712  reprinrn  34946  reprinfz1  34950  reprdifc  34955  bnj1173  35331  subfacp1lem5  35571  rexxfr3dALT  36026  filnetlem4  36777  mh-infprim1bi  36942  bj-clel3gALT  37568  bj-imdirco  37717  taupilem3  37846  topdifinffinlem  37876  finxpsuclem  37926  matunitlindf  38152  poimirlem22  38176  poimirlem26  38180  poimirlem27  38181  heicant  38189  mbfposadd  38201  itg2addnclem  38205  itg2addnclem2  38206  iblabsnclem  38217  ftc1anclem1  38227  ftc1anclem5  38231  areacirclem5  38246  areacirc  38247  lmclim2  38292  caures  38294  rrnheibor  38371  isdmn3  38608  opelvvdif  38798  ralrnmo  38895  raldmqsmo  38897  brxrn  38917  lrelat  39673  lcvbr  39680  lsatcv0eq  39706  ellkr2  39750  lkr0f  39753  lkreqN  39829  opltn0  39849  op1le  39851  leatb  39951  atlltn0  39965  hlrelat5N  40060  hlrelat  40061  cvrval5  40074  cvrexchlem  40078  atcvr0eq  40085  athgt  40115  1cvrco  40131  islpln5  40194  islvol5  40238  elpadd2at2  40466  cdleme0ex2N  40883  cdleme3  40896  cdleme7  40908  cdlemg33e  41369  dochfln0  42136  lcfl1  42151  lcfls1N  42194  lspindp5  42429  isnacs2  43324  rabrenfdioph  43428  rmxycomplete  43531  expdioph  43637  pwfi2f1o  43710  islnr3  43729  sqrtcvallem1  44244  ntrneixb  44708  clim2cf  46251  funressnfv  47664  focofob  47701  nprmmul1  48160  oddm1evenALTV  48324  oddp1evenALTV  48325  divgcdoddALTV  48331  lco0  49087  lindslinindsimp2lem5  49122  snlindsntor  49131  elbigo2  49212  affinecomb1  49362  itscnhlinecirc02p  49445  reuxfr1dd  49465  iscnrm3lem1  49592