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  3645  reuxfr1d  3708  n0moeu  4311  eldifvsn  4753  xpco  6247  funcnv3  6562  fnssresb  6614  dff1o5  6783  fneqeql2  6992  dffo3  7047  dffo3f  7051  fmptco  7074  fconst4  7160  riota2df  7338  eloprabga  7467  fnwelem  8073  frxp2  8086  xpord2pred  8087  xpord3pred  8094  mptsuppd  8129  mptelixpg  8873  boxcutc  8879  inficl  9328  cantnfle  9580  cantnflem1  9598  ttrclselem2  9635  bnd2  9805  iscard2  9888  alephinit  10005  kmlem2  10062  cfss  10175  fpwwe2lem8  10549  axgroth2  10736  elnnnn0  12444  znnsub  12537  znn0sub  12538  negelrp  12940  xsubge0  13176  divelunit  13410  elfz5  13432  preduz  13566  injresinj  13707  adddivflid  13738  divfl0  13744  hashf1lem1  14378  swrdspsleq  14589  repswsymball  14702  repswsymballbi  14703  2shfti  15003  cnpart  15163  sqrtneglem  15189  rexuz3  15272  rlim  15418  rlim2  15419  clim2c  15428  cvgcmp  15739  bitsmod  16363  bitscmp  16365  pc2dvds  16807  prmreclem4  16847  1arith  16855  imasleval  17462  xpsfrnel  17483  xpsfrnel2  17485  dfiso2  17696  pospropd  18248  latleeqm1  18390  latnlemlt  18395  latnle  18396  ipole  18457  gsumval2a  18610  ismhm0  18715  ghmeqker  19172  gastacos  19239  isslw  19537  slwpss  19541  pgpssslw  19543  fislw  19554  sylow3lem6  19561  dprd2d2  19975  isrnghmmul  20378  isdomn3  20648  lsslss  20912  lsmspsn  21036  zndvds  21504  znleval2  21510  elfilspd  21758  islinds2  21768  islindf2  21769  ismhp3  22085  coe1mul2lem1  22209  eltg3  22906  leordtvallem1  23154  leordtvallem2  23155  lmbrf  23204  cnrest2  23230  xkoccn  23563  hauseqlcld  23590  qtopcn  23658  ordthmeolem  23745  isfbas  23773  fbunfip  23813  fixufil  23866  alexsubALTlem4  23994  ismet2  24277  xblpnfps  24339  xblpnf  24340  blval2  24506  metuel2  24509  dscopn  24517  cnbl0  24717  cnblcld  24718  xrtgioo  24751  mulc1cncf  24854  isclmp  25053  isncvsngp  25105  lmmbrf  25218  iscauf  25236  caucfil  25239  lmclim  25259  evthicc2  25417  volsup  25513  ioombl1lem4  25518  ismbf  25585  ismbfcn  25586  mbfmulc2lem  25604  mbfmax  25606  mbfposr  25609  ismbf3d  25611  mbfimaopnlem  25612  mbfsup  25621  i1fpos  25663  mbfi1fseqlem4  25675  xrge0f  25688  itg2seq  25699  itg2monolem1  25707  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  i1fibl  25765  ditgneg  25814  lhop1  25975  r1pid2  26123  fta1  26272  ulm2  26350  pilem1  26417  sineq0  26489  ellogrn  26524  rlimcnp  26931  wilthlem1  27034  sqff1o  27148  logfaclbnd  27189  bposlem1  27251  lgsdilem  27291  lgsabs1  27303  lgsdchrval  27321  lgsquadlem1  27347  lgsquadlem2  27348  sltssnb  27765  zn0subs  28399  iscgrgd  28585  trgcgrg  28587  ltgov  28669  ishlg  28674  lnhl  28687  israg  28769  islnopp  28811  iscgra  28881  isinag  28910  iseqlg  28939  nbupgrel  29418  isuvtx  29468  iscplgredg  29490  rusgrnumwwlkl1  30044  clwlkclwwlk2  30078  isclwwlknx  30111  clwwlkn1  30116  nmoo0  30866  ubthlem1  30945  ch0pss  31520  pjnorm2  31802  adjval  31965  leop  32198  atcv0eq  32454  xppreima  32723  fmptcof2  32735  xrdifh  32860  hashgt1  32888  isinftm  33263  isunit3  33323  isdrng4  33377  fracerl  33388  dvdsruassoi  33465  dvdsruasso  33466  dvdsrspss  33468  lsmsnorb  33472  ply1degltel  33675  r1pid2OLD  33690  psrbasfsupp  33693  smatrcl  33953  rhmpreimacnlem  34041  ismntop  34183  brfae  34405  eulerpartlemr  34531  eulerpartlemn  34538  reprinrn  34775  reprinfz1  34779  reprdifc  34784  bnj1173  35158  subfacp1lem5  35378  rexxfr3dALT  35833  filnetlem4  36575  bj-clel3gALT  37249  bj-imdirco  37395  taupilem3  37524  topdifinffinlem  37552  finxpsuclem  37602  matunitlindf  37819  poimirlem22  37843  poimirlem26  37847  poimirlem27  37848  heicant  37856  mbfposadd  37868  itg2addnclem  37872  itg2addnclem2  37873  iblabsnclem  37884  ftc1anclem1  37894  ftc1anclem5  37898  areacirclem5  37913  areacirc  37914  lmclim2  37959  caures  37961  rrnheibor  38038  isdmn3  38275  opelvvdif  38457  brxrn  38568  lrelat  39274  lcvbr  39281  lsatcv0eq  39307  ellkr2  39351  lkr0f  39354  lkreqN  39430  opltn0  39450  op1le  39452  leatb  39552  atlltn0  39566  hlrelat5N  39661  hlrelat  39662  cvrval5  39675  cvrexchlem  39679  atcvr0eq  39686  athgt  39716  1cvrco  39732  islpln5  39795  islvol5  39839  elpadd2at2  40067  cdleme0ex2N  40484  cdleme3  40497  cdleme7  40509  cdlemg33e  40970  dochfln0  41737  lcfl1  41752  lcfls1N  41795  lspindp5  42030  isnacs2  42948  rabrenfdioph  43056  rmxycomplete  43159  expdioph  43265  pwfi2f1o  43338  islnr3  43357  sqrtcvallem1  43872  ntrneixb  44336  clim2cf  45894  funressnfv  47289  focofob  47326  oddm1evenALTV  47921  oddp1evenALTV  47922  divgcdoddALTV  47928  lco0  48673  lindslinindsimp2lem5  48708  snlindsntor  48717  elbigo2  48798  affinecomb1  48948  itscnhlinecirc02p  49031  reuxfr1dd  49052  iscnrm3lem1  49179