Theorem biantrurd 540

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm5.3  580  mpbirand  717  3biant1d  1498  elrab3t  3648  reuxfr1d  3711  n0moeu  4309  eldifvsn  4754  xpco  6271  funcnv3  6586  fnssresb  6638  dff1o5  6811  fneqeql2  7023  dffo3  7078  dffo3f  7082  fmptco  7106  fconst4  7193  riota2df  7371  eloprabga  7500  fnwelem  8105  frxp2  8118  xpord2pred  8119  xpord3pred  8126  mptsuppd  8161  mptelixpg  8911  boxcutc  8917  inficl  9365  cantnfle  9620  cantnflem1  9638  ttrclselem2  9675  bnd2  9845  iscard2  9928  alephinit  10045  kmlem2  10102  cfss  10216  fpwwe2lem8  10590  axgroth2  10777  elnnnn0  12518  znnsub  12611  znn0sub  12612  negelrp  13022  xsubge0  13258  divelunit  13492  elfz5  13515  preduz  13649  injresinj  13791  adddivflid  13822  divfl0  13828  hashf1lem1  14462  swrdspsleq  14673  repswsymball  14786  repswsymballbi  14787  2shfti  15087  cnpart  15258  sqrtneglem  15284  rexuz3  15367  rlim  15513  rlim2  15514  clim2c  15523  cvgcmp  15835  bitsmod  16461  bitscmp  16463  pc2dvds  16906  prmreclem4  16946  1arith  16954  imasleval  17562  xpsfrnel  17583  xpsfrnel2  17585  dfiso2  17796  pospropd  18348  latleeqm1  18490  latnlemlt  18495  latnle  18496  ipole  18557  gsumval2a  18710  ismhm0  18815  ghmeqker  19274  gastacos  19341  isslw  19639  slwpss  19643  pgpssslw  19645  fislw  19656  sylow3lem6  19663  dprd2d2  20077  isrnghmmul  20478  isdomn3  20752  lsslss  21016  lsmspsn  21139  zndvds  21589  znleval2  21595  elfilspd  21843  islinds2  21853  islindf2  21854  ismhp3  22195  coe1mul2lem1  22318  eltg3  23010  leordtvallem1  23258  leordtvallem2  23259  lmbrf  23308  cnrest2  23334  xkoccn  23667  hauseqlcld  23694  qtopcn  23762  ordthmeolem  23849  isfbas  23877  fbunfip  23917  fixufil  23970  alexsubALTlem4  24098  ismet2  24381  xblpnfps  24443  xblpnf  24444  blval2  24610  metuel2  24613  dscopn  24621  cnbl0  24821  cnblcld  24822  xrtgioo  24855  mulc1cncf  24955  isclmp  25147  isncvsngp  25199  lmmbrf  25312  iscauf  25330  caucfil  25333  lmclim  25353  evthicc2  25510  volsup  25606  ioombl1lem4  25611  ismbf  25678  ismbfcn  25679  mbfmulc2lem  25697  mbfmax  25699  mbfposr  25702  ismbf3d  25704  mbfimaopnlem  25705  mbfsup  25714  i1fpos  25756  mbfi1fseqlem4  25768  xrge0f  25781  itg2seq  25792  itg2monolem1  25800  itg2gt0  25810  itg2cnlem1  25811  itg2cnlem2  25812  i1fibl  25858  ditgneg  25907  lhop1  26064  r1pid2  26210  fta1  26360  ulm2  26436  pilem1  26502  sineq0  26577  ellogrn  26612  rlimcnp  27018  wilthlem1  27120  sqff1o  27234  logfaclbnd  27274  bposlem1  27336  lgsdilem  27376  lgsabs1  27388  lgsdchrval  27406  lgsquadlem1  27432  lgsquadlem2  27433  sltssnb  27850  zn0subs  28484  iscgrgd  28670  trgcgrg  28672  ltgov  28754  ishlg  28759  lnhl  28772  israg  28854  islnopp  28896  iscgra  28966  isinag  28995  iseqlg  29024  nbupgrel  29503  isuvtx  29553  iscplgredg  29575  rusgrnumwwlkl1  30128  clwlkclwwlk2  30162  isclwwlknx  30195  clwwlkn1  30200  nmoo0  30951  ubthlem1  31030  ch0pss  31605  pjnorm2  31887  adjval  32050  leop  32283  atcv0eq  32539  xppreima  32808  fmptcof2  32820  xrdifh  32943  hashgt1  32971  isinftm  33322  isunit3  33382  rlocisunit  33418  isdrng4  33443  fracerl  33454  dvdsruassoi  33531  dvdsruasso  33532  dvdsrspss  33534  lsmsnorb  33538  ply1degltel  33751  r1pid2OLD  33766  psrbasfsupp  33769  smatrcl  34054  rhmpreimacnlem  34142  ismntop  34284  brfae  34506  eulerpartlemr  34632  eulerpartlemn  34639  reprinrn  34873  reprinfz1  34877  reprdifc  34882  bnj1173  35258  subfacp1lem5  35495  rexxfr3dALT  35950  filnetlem4  36702  mh-infprim1bi  36867  bj-clel3gALT  37494  bj-imdirco  37643  taupilem3  37772  topdifinffinlem  37802  finxpsuclem  37852  matunitlindf  38078  poimirlem22  38102  poimirlem26  38106  poimirlem27  38107  heicant  38115  mbfposadd  38127  itg2addnclem  38131  itg2addnclem2  38132  iblabsnclem  38143  ftc1anclem1  38153  ftc1anclem5  38157  areacirclem5  38172  areacirc  38173  lmclim2  38218  caures  38220  rrnheibor  38297  isdmn3  38534  opelvvdif  38724  ralrnmo  38821  raldmqsmo  38823  brxrn  38843  lrelat  39599  lcvbr  39606  lsatcv0eq  39632  ellkr2  39676  lkr0f  39679  lkreqN  39755  opltn0  39775  op1le  39777  leatb  39877  atlltn0  39891  hlrelat5N  39986  hlrelat  39987  cvrval5  40000  cvrexchlem  40004  atcvr0eq  40011  athgt  40041  1cvrco  40057  islpln5  40120  islvol5  40164  elpadd2at2  40392  cdleme0ex2N  40809  cdleme3  40822  cdleme7  40834  cdlemg33e  41295  dochfln0  42062  lcfl1  42077  lcfls1N  42120  lspindp5  42355  isnacs2  43248  rabrenfdioph  43352  rmxycomplete  43455  expdioph  43561  pwfi2f1o  43634  islnr3  43653  sqrtcvallem1  44168  ntrneixb  44632  clim2cf  46185  funressnfv  47598  focofob  47635  nprmmul1  48094  oddm1evenALTV  48258  oddp1evenALTV  48259  divgcdoddALTV  48265  lco0  49010  lindslinindsimp2lem5  49045  snlindsntor  49054  elbigo2  49135  affinecomb1  49285  itscnhlinecirc02p  49368  reuxfr1dd  49389  iscnrm3lem1  49516