Theorem biantrurd 528

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpbirand  529  3biant1d  1433  elrab3t  3330  n0moeu  3893  eldifvsn  4267  reuxfrd  4819  xpco  5592  funcnv3  5873  fnssresb  5917  dff1o5  6059  fneqeql2  6234  dffo3  6282  fmptco  6303  fconst4  6383  riota2df  6531  eloprabga  6645  fnwelem  7179  mptsuppd  7205  mptelixpg  7831  boxcutc  7837  inficl  8214  wemapso2lem  8340  cantnfle  8451  cantnflem1  8469  bnd2  8639  iscard2  8685  alephinit  8801  kmlem2  8856  cfss  8970  fpwwe2lem9  9339  axgroth2  9526  elnnnn0  11213  znnsub  11300  znn0sub  11301  uzin  11596  negelrp  11740  xsubge0  11963  supxrre1  12032  ixxun  12062  divelunit  12185  elfz5  12205  uzsplit  12281  preduz  12330  injresinj  12451  adddivflid  12481  divfl0  12487  hashf1lem1  13096  swrdspsleq  13301  repswsymball  13377  repswsymballbi  13378  2shfti  13668  cnpart  13828  sqrtneglem  13855  rexuz3  13936  rlim  14074  rlim2  14075  clim2c  14084  ello12  14095  elo12  14106  fsumss  14303  fsumcom2OLD  14348  cvgcmp  14389  fprodss  14517  fprodcom2OLD  14554  bitsmod  14996  bitscmp  14998  pc2dvds  15421  prmreclem4  15461  1arith  15469  ramval  15550  imasleval  16024  xpsfrnel  16046  xpsfrnel2  16048  dfiso2  16255  latleeqm1  16902  latnlemlt  16907  latnle  16908  pospropd  16957  ipole  16981  gsumval2a  17102  ghmeqker  17510  gastacos  17566  isslw  17846  slwpss  17850  pgpssslw  17852  fislw  17863  sylow3lem6  17870  dprd2d2  18266  lsslss  18782  lspsnel5  18816  lsmspsn  18905  coe1mul2lem1  19458  zndvds  19717  znleval2  19723  elfilspd  19961  islinds2  19971  islindf2  19972  eltg3  20577  leordtvallem1  20824  leordtvallem2  20825  lmbrf  20874  cnrest2  20900  cnprest  20903  cnprest2  20904  cnt0  20960  1stccn  21076  kgencn  21169  xkoccn  21232  qtopcn  21327  ordthmeolem  21414  isfbas  21443  fbunfip  21483  fixufil  21536  fbflim  21590  isflf  21607  cnflf  21616  fclscf  21639  cnfcf  21656  alexsubALTlem4  21664  ismet2  21948  elbl2ps  22004  elbl2  22005  xblpnfps  22010  xblpnf  22011  metcn  22158  txmetcn  22163  blval2  22177  metuel2  22180  dscopn  22188  cnbl0  22387  cnblcld  22388  xrtgioo  22417  mulc1cncf  22516  isclmp  22705  isncvsngp  22757  lmmbrf  22868  iscauf  22886  caucfil  22889  lmclim  22909  lmclimf  22910  evthicc2  23036  ovolfioo  23043  ovolficc  23044  ovoliun  23080  ismbl2  23102  volsup  23131  ioombl1lem4  23136  ismbf  23203  ismbfcn  23204  mbfmulc2lem  23220  mbfmax  23222  mbfposr  23225  ismbf3d  23227  mbfimaopnlem  23228  mbfaddlem  23233  mbfsup  23237  i1fpos  23279  mbfi1fseqlem4  23291  xrge0f  23304  itg2seq  23315  itg2monolem1  23323  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  i1fibl  23380  ditgneg  23427  lhop1  23581  fta1  23867  ulm2  23943  pilem1  24009  sineq0  24077  ellogrn  24110  rlimcnp  24492  wilthlem1  24594  sqff1o  24708  logfaclbnd  24747  bposlem1  24809  lgsdilem  24849  lgsabs1  24861  lgsdchrval  24879  lgsquadlem1  24905  lgsquadlem2  24906  iscgrgd  25208  trgcgrg  25210  tgellng  25248  ltgov  25292  ishlg  25297  lnhl  25310  israg  25392  islnopp  25431  iscgra  25501  isinag  25529  isleag  25533  iseqlg  25547  ttgelitv  25563  cusgra3v  25993  wlkdvspthlem  26137  clwlkisclwwlk2  26318  el2spthonot0  26398  el2wlksotot  26409  rusgranumwlkl1  26474  numclwlk1lem2f1  26621  nmoo0  27030  ubthlem1  27110  ch0pss  27688  pjnorm2  27970  adjval  28133  leop  28366  atcv0eq  28622  reuxfr4d  28714  xppreima  28829  fmptcof2  28839  xrdifh  28932  isinftm  29066  smatrcl  29190  ismntoplly  29397  ismntop  29398  brfae  29638  eulerpartlemr  29763  eulerpartlemn  29770  bnj1173  30324  subfacp1lem5  30420  nofulllem2  31102  filnetlem4  31546  taupilem3  32342  topdifinffinlem  32371  finxpsuclem  32410  matunitlindf  32577  poimirlem22  32601  poimirlem26  32605  poimirlem27  32606  heicant  32614  mbfposadd  32627  itg2addnclem  32631  itg2addnclem2  32632  iblabsnclem  32643  ftc1anclem1  32655  ftc1anclem5  32659  areacirclem5  32674  areacirc  32675  lmclim2  32724  caures  32726  rrnheibor  32806  isdmn3  33043  lrelat  33319  lcvbr  33326  lsatcv0eq  33352  ellkr2  33396  lkr0f  33399  lkreqN  33475  opltn0  33495  op1le  33497  leatb  33597  atlltn0  33611  hlrelat5N  33705  hlrelat  33706  cvrval5  33719  cvrexchlem  33723  atcvr0eq  33730  athgt  33760  1cvrco  33776  islpln5  33839  islvol5  33883  elpadd2at2  34111  cdleme0ex2N  34529  cdleme3  34542  cdleme7  34554  cdlemg33e  35016  dochfln0  35784  lcfl1  35799  lcfls1N  35842  lspindp5  36077  isnacs2  36287  rabrenfdioph  36396  rmxycomplete  36500  expdioph  36608  pwfi2f1o  36684  islnr3  36704  isdomn3  36801  ntrneixb  37413  dffo3f  38359  clim2cf  38717  oddm1evenALTV  40124  oddp1evenALTV  40125  divgcdoddALTV  40131  pfxsuffeqwrdeq  40269  nbupgrel  40567  isuvtxa  40621  iscplgredg  40639  rusgrnumwwlkl1  41172  isclwwlksnx  41197  clwlkclwwlk2  41212  av-numclwlk1lem2f1  41524  ismhm0  41595  isrnghmmul  41683  lco0  42010  lindslinindsimp2lem5  42045  snlindsntor  42054  elbigo2  42144