Theorem biantrurd 535

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

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

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 399

This theorem is referenced by:  pm5.3  575  mpbirand  705  3biant1d  1474  elrab3t  3679  reuxfr1d  3741  n0moeu  4316  eldifvsn  4730  xpco  6140  funcnv3  6424  fnssresb  6469  dff1o5  6624  fneqeql2  6817  dffo3  6868  fmptco  6891  fconst4  6977  riota2df  7137  eloprabga  7261  fnwelem  7825  mptsuppd  7853  mptelixpg  8499  boxcutc  8505  inficl  8889  cantnfle  9134  cantnflem1  9152  bnd2  9322  iscard2  9405  alephinit  9521  kmlem2  9577  cfss  9687  fpwwe2lem9  10060  axgroth2  10247  elnnnn0  11941  znnsub  12029  znn0sub  12030  negelrp  12423  xsubge0  12655  divelunit  12881  elfz5  12901  preduz  13030  injresinj  13159  adddivflid  13189  divfl0  13195  hashf1lem1  13814  swrdspsleq  14027  repswsymball  14141  repswsymballbi  14142  2shfti  14439  cnpart  14599  sqrtneglem  14626  rexuz3  14708  rlim  14852  rlim2  14853  clim2c  14862  cvgcmp  15171  bitsmod  15785  bitscmp  15787  pc2dvds  16215  prmreclem4  16255  1arith  16263  imasleval  16814  xpsfrnel  16835  xpsfrnel2  16837  dfiso2  17042  latleeqm1  17689  latnlemlt  17694  latnle  17695  pospropd  17744  ipole  17768  gsumval2a  17895  ghmeqker  18385  gastacos  18440  isslw  18733  slwpss  18737  pgpssslw  18739  fislw  18750  sylow3lem6  18757  dprd2d2  19166  lsslss  19733  lsmspsn  19856  mhpinvcl  20339  coe1mul2lem1  20435  zndvds  20696  znleval2  20702  elfilspd  20947  islinds2  20957  islindf2  20958  eltg3  21570  leordtvallem1  21818  leordtvallem2  21819  lmbrf  21868  cnrest2  21894  xkoccn  22227  hauseqlcld  22254  qtopcn  22322  ordthmeolem  22409  isfbas  22437  fbunfip  22477  fixufil  22530  alexsubALTlem4  22658  ismet2  22943  xblpnfps  23005  xblpnf  23006  blval2  23172  metuel2  23175  dscopn  23183  cnbl0  23382  cnblcld  23383  xrtgioo  23414  mulc1cncf  23513  isclmp  23701  isncvsngp  23753  lmmbrf  23865  iscauf  23883  caucfil  23886  lmclim  23906  evthicc2  24061  volsup  24157  ioombl1lem4  24162  ismbf  24229  ismbfcn  24230  mbfmulc2lem  24248  mbfmax  24250  mbfposr  24253  ismbf3d  24255  mbfimaopnlem  24256  mbfsup  24265  i1fpos  24307  mbfi1fseqlem4  24319  xrge0f  24332  itg2seq  24343  itg2monolem1  24351  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  i1fibl  24408  ditgneg  24455  lhop1  24611  fta1  24897  ulm2  24973  pilem1  25039  sineq0  25109  ellogrn  25143  rlimcnp  25543  wilthlem1  25645  sqff1o  25759  logfaclbnd  25798  bposlem1  25860  lgsdilem  25900  lgsabs1  25912  lgsdchrval  25930  lgsquadlem1  25956  lgsquadlem2  25957  iscgrgd  26299  trgcgrg  26301  ltgov  26383  ishlg  26388  lnhl  26401  israg  26483  islnopp  26525  iscgra  26595  isinag  26624  iseqlg  26653  nbupgrel  27127  isuvtx  27177  iscplgredg  27199  rusgrnumwwlkl1  27747  clwlkclwwlk2  27781  isclwwlknx  27814  clwwlkn1  27819  nmoo0  28568  ubthlem1  28647  ch0pss  29222  pjnorm2  29504  adjval  29667  leop  29900  atcv0eq  30156  xppreima  30394  fmptcof2  30402  xrdifh  30503  hashgt1  30530  isinftm  30810  lsmsnorb  30945  smatrcl  31061  ismntop  31267  brfae  31507  eulerpartlemr  31632  eulerpartlemn  31639  reprinrn  31889  reprinfz1  31893  reprdifc  31898  bnj1173  32274  subfacp1lem5  32431  etasslt  33274  filnetlem4  33729  taupilem3  34603  topdifinffinlem  34631  finxpsuclem  34681  matunitlindf  34905  poimirlem22  34929  poimirlem26  34933  poimirlem27  34934  heicant  34942  mbfposadd  34954  itg2addnclem  34958  itg2addnclem2  34959  iblabsnclem  34970  ftc1anclem1  34982  ftc1anclem5  34986  areacirclem5  35001  areacirc  35002  lmclim2  35048  caures  35050  rrnheibor  35130  isdmn3  35367  opelvvdif  35535  brxrn  35641  lrelat  36165  lcvbr  36172  lsatcv0eq  36198  ellkr2  36242  lkr0f  36245  lkreqN  36321  opltn0  36341  op1le  36343  leatb  36443  atlltn0  36457  hlrelat5N  36552  hlrelat  36553  cvrval5  36566  cvrexchlem  36570  atcvr0eq  36577  athgt  36607  1cvrco  36623  islpln5  36686  islvol5  36730  elpadd2at2  36958  cdleme0ex2N  37375  cdleme3  37388  cdleme7  37400  cdlemg33e  37861  dochfln0  38628  lcfl1  38643  lcfls1N  38686  lspindp5  38921  isnacs2  39352  rabrenfdioph  39460  rmxycomplete  39563  expdioph  39669  pwfi2f1o  39745  islnr3  39764  isdomn3  39853  ntrneixb  40494  dffo3f  41487  clim2cf  41980  funressnfv  43327  oddm1evenALTV  43889  oddp1evenALTV  43890  divgcdoddALTV  43896  ismhm0  44121  isrnghmmul  44213  lco0  44531  lindslinindsimp2lem5  44566  snlindsntor  44575  elbigo2  44661  affinecomb1  44738  itscnhlinecirc02p  44821