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  706  3biant1d  1478  elrab3t  3707  reuxfr1d  3772  n0moeu  4382  eldifvsn  4822  xpco  6320  funcnv3  6648  fnssresb  6702  dff1o5  6871  fneqeql2  7080  dffo3  7136  dffo3f  7140  fmptco  7163  fconst4  7251  riota2df  7428  eloprabga  7558  eloprabgaOLD  7559  fnwelem  8172  frxp2  8185  xpord2pred  8186  xpord3pred  8193  mptsuppd  8228  mptelixpg  8993  boxcutc  8999  inficl  9494  cantnfle  9740  cantnflem1  9758  ttrclselem2  9795  bnd2  9962  iscard2  10045  alephinit  10164  kmlem2  10221  cfss  10334  fpwwe2lem8  10707  axgroth2  10894  elnnnn0  12596  znnsub  12689  znn0sub  12690  negelrp  13090  xsubge0  13323  divelunit  13554  elfz5  13576  preduz  13707  injresinj  13838  adddivflid  13869  divfl0  13875  hashf1lem1  14504  swrdspsleq  14713  repswsymball  14827  repswsymballbi  14828  2shfti  15129  cnpart  15289  sqrtneglem  15315  rexuz3  15397  rlim  15541  rlim2  15542  clim2c  15551  cvgcmp  15864  bitsmod  16482  bitscmp  16484  pc2dvds  16926  prmreclem4  16966  1arith  16974  imasleval  17601  xpsfrnel  17622  xpsfrnel2  17624  dfiso2  17833  pospropd  18397  latleeqm1  18537  latnlemlt  18542  latnle  18543  ipole  18604  gsumval2a  18723  ismhm0  18825  ghmeqker  19283  gastacos  19350  isslw  19650  slwpss  19654  pgpssslw  19656  fislw  19667  sylow3lem6  19674  dprd2d2  20088  isrnghmmul  20468  isdomn3  20737  lsslss  20982  lsmspsn  21106  zndvds  21591  znleval2  21597  elfilspd  21846  islinds2  21856  islindf2  21857  ismhp3  22169  coe1mul2lem1  22291  eltg3  22990  leordtvallem1  23239  leordtvallem2  23240  lmbrf  23289  cnrest2  23315  xkoccn  23648  hauseqlcld  23675  qtopcn  23743  ordthmeolem  23830  isfbas  23858  fbunfip  23898  fixufil  23951  alexsubALTlem4  24079  ismet2  24364  xblpnfps  24426  xblpnf  24427  blval2  24596  metuel2  24599  dscopn  24607  cnbl0  24815  cnblcld  24816  xrtgioo  24847  mulc1cncf  24950  isclmp  25149  isncvsngp  25202  lmmbrf  25315  iscauf  25333  caucfil  25336  lmclim  25356  evthicc2  25514  volsup  25610  ioombl1lem4  25615  ismbf  25682  ismbfcn  25683  mbfmulc2lem  25701  mbfmax  25703  mbfposr  25706  ismbf3d  25708  mbfimaopnlem  25709  mbfsup  25718  i1fpos  25761  mbfi1fseqlem4  25773  xrge0f  25786  itg2seq  25797  itg2monolem1  25805  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  i1fibl  25863  ditgneg  25912  lhop1  26073  r1pid2  26221  fta1  26368  ulm2  26446  pilem1  26513  sineq0  26584  ellogrn  26619  rlimcnp  27026  wilthlem1  27129  sqff1o  27243  logfaclbnd  27284  bposlem1  27346  lgsdilem  27386  lgsabs1  27398  lgsdchrval  27416  lgsquadlem1  27442  lgsquadlem2  27443  zn0subs  28407  iscgrgd  28539  trgcgrg  28541  ltgov  28623  ishlg  28628  lnhl  28641  israg  28723  islnopp  28765  iscgra  28835  isinag  28864  iseqlg  28893  nbupgrel  29380  isuvtx  29430  iscplgredg  29452  rusgrnumwwlkl1  30001  clwlkclwwlk2  30035  isclwwlknx  30068  clwwlkn1  30073  nmoo0  30823  ubthlem1  30902  ch0pss  31477  pjnorm2  31759  adjval  31922  leop  32155  atcv0eq  32411  xppreima  32664  fmptcof2  32675  xrdifh  32785  hashgt1  32815  isinftm  33161  isunit3  33221  isdrng4  33264  fracerl  33273  dvdsruassoi  33377  dvdsruasso  33378  dvdsrspss  33380  lsmsnorb  33384  ply1degltel  33580  r1pid2OLD  33594  smatrcl  33742  rhmpreimacnlem  33830  ismntop  33972  brfae  34212  eulerpartlemr  34339  eulerpartlemn  34346  reprinrn  34595  reprinfz1  34599  reprdifc  34604  bnj1173  34978  subfacp1lem5  35152  rexxfr3dALT  35607  filnetlem4  36347  bj-clel3gALT  37014  bj-imdirco  37156  taupilem3  37285  topdifinffinlem  37313  finxpsuclem  37363  matunitlindf  37578  poimirlem22  37602  poimirlem26  37606  poimirlem27  37607  heicant  37615  mbfposadd  37627  itg2addnclem  37631  itg2addnclem2  37632  iblabsnclem  37643  ftc1anclem1  37653  ftc1anclem5  37657  areacirclem5  37672  areacirc  37673  lmclim2  37718  caures  37720  rrnheibor  37797  isdmn3  38034  opelvvdif  38215  brxrn  38330  lrelat  38970  lcvbr  38977  lsatcv0eq  39003  ellkr2  39047  lkr0f  39050  lkreqN  39126  opltn0  39146  op1le  39148  leatb  39248  atlltn0  39262  hlrelat5N  39358  hlrelat  39359  cvrval5  39372  cvrexchlem  39376  atcvr0eq  39383  athgt  39413  1cvrco  39429  islpln5  39492  islvol5  39536  elpadd2at2  39764  cdleme0ex2N  40181  cdleme3  40194  cdleme7  40206  cdlemg33e  40667  dochfln0  41434  lcfl1  41449  lcfls1N  41492  lspindp5  41727  isnacs2  42662  rabrenfdioph  42770  rmxycomplete  42874  expdioph  42980  pwfi2f1o  43053  islnr3  43072  sqrtcvallem1  43593  ntrneixb  44057  clim2cf  45571  funressnfv  46958  focofob  46995  oddm1evenALTV  47549  oddp1evenALTV  47550  divgcdoddALTV  47556  lco0  48156  lindslinindsimp2lem5  48191  snlindsntor  48200  elbigo2  48286  affinecomb1  48436  itscnhlinecirc02p  48519  iscnrm3lem1  48613