Theorem biantrud 533

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)

Hypothesis

Ref	Expression
biantrud.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
biantrud	⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

Proof of Theorem biantrud

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 ⊢ (𝜑 → 𝜓)
2		iba 529	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ifptru  1075  cad1  1619  raldifeq  4494  rexreusng  4684  posn  5762  elrnmpt1  5958  dfres3  5987  opelres  5988  ffrnbd  6734  fliftf  7312  eroveu  8806  ixpfi2  9350  elfi2  9409  dffi3  9426  cfss  10260  wunex2  10733  nnle1eq1  12242  nn0le0eq0  12500  ixxun  13340  ioopos  13401  injresinj  13753  hashle00  14360  prprrab  14434  xpcogend  14921  cnpart  15187  fz1f1o  15656  nndivdvds  16206  dvdsmultr2  16241  bitsmod  16377  sadadd  16408  sadass  16412  smuval2  16423  smumul  16434  pcmpt  16825  pcmpt2  16826  prmreclem2  16850  prmreclem5  16853  ramcl  16962  mrcidb2  17562  acsfn  17603  fncnvimaeqv  18071  latleeqj1  18404  resmndismnd  18689  pgpssslw  19482  subgdmdprd  19904  resrhm2b  20349  acsfn1p  20415  lssle0  20560  islpir2  20889  islinds3  21389  iscld4  22569  cncnpi  22782  cnprest2  22794  lmss  22802  isconn2  22918  dfconn2  22923  subislly  22985  lly1stc  23000  elptr  23077  txcn  23130  xkoinjcn  23191  tsmsres  23648  isxmet2d  23833  xmetgt0  23864  prdsxmetlem  23874  imasdsf1olem  23879  xblss2  23908  stdbdbl  24026  prdsxmslem2  24038  xrtgioo  24322  xrsxmet  24325  cnmpopc  24444  elpi1i  24562  minveclem7  24952  elovolmr  24993  ismbf  25145  mbfmax  25166  itg1val2  25201  mbfi1fseqlem4  25236  itgresr  25296  iblrelem  25308  iblpos  25310  rlimcnp  26470  rlimcnp2  26471  chpchtsum  26722  lgsneg  26824  lgsdilem  26827  2lgslem1a  26894  eqscut2  27307  lmiinv  28043  isspthonpth  29006  s3wwlks2on  29210  clwlkclwwlk  29255  clwwlknonel  29348  clwwlknun  29365  eupth2lem2  29472  frgr3vlem2  29527  numclwwlk2lem1  29629  nrt2irr  29726  minvecolem7  30136  shle0  30695  mdsl2bi  31576  dmdbr5ati  31675  cdj3lem1  31687  qsfld  32612  eulerpartlemr  33373  subfacp1lem3  34173  satefvfmla1  34416  hfext  35155  bj-issetwt  35754  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  mblfinlem3  36527  mblfinlem4  36528  mbfresfi  36534  itg2addnclem  36539  itg2addnc  36542  heiborlem10  36688  relssinxpdmrn  37218  dffunsALTV2  37554  dffunsALTV3  37555  dffunsALTV4  37556  elfunsALTV2  37563  elfunsALTV3  37564  elfunsALTV4  37565  elfunsALTV5  37566  dfdisjs2  37579  dfdisjs5  37582  eldisjs2  37593  ople0  38057  atlle0  38175  cdlemg10c  39510  cdlemg33c  39579  hdmap14lem13  40751  mrefg3  41446  onsupneqmaxlim0  41973  onsupnmax  41977  radcnvrat  43073  2ffzoeq  46036