Theorem biantrud 541

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ifptru  1091  cad1  1649  nrmod  3838  raldifeq  4448  rexreusng  4636  posn  5736  dmxp  5910  elrnmpt1  5941  dfres3  5974  opelres  5975  ffrnbd  6725  fliftf  7323  eroveu  8836  ixpfi2  9342  elfi2  9409  dffi3  9426  cfss  10346  wunex2  10826  nnle1eq1  12371  nn0le0eq0  12637  ixxun  13495  ioopos  13558  injresinj  13929  hashle00  14547  prprrab  14621  xpcogend  15132  cnpart  15412  fz1f1o  15881  nndivdvds  16436  dvdsmultr2  16473  bitsmod  16611  sadadd  16642  sadass  16646  smuval2  16657  smumul  16668  pcmpt  17075  pcmpt2  17076  prmreclem2  17100  prmreclem5  17103  ramcl  17212  mrcidb2  17797  acsfn  17838  fncnvimaeqv  18299  latleeqj1  18630  resmndismnd  19008  pgpssslw  19833  subgdmdprd  20255  resrhm2b  20859  acsfn1p  21061  lssle0  21230  islpir2  21659  islinds3  22145  iscld4  23388  cncnpi  23601  cnprest2  23613  lmss  23621  isconn2  23737  dfconn2  23742  subislly  23805  lly1stc  23820  elptr  23897  txcn  23950  xkoinjcn  24011  tsmsres  24468  isxmet2d  24651  xmetgt0  24682  prdsxmetlem  24692  imasdsf1olem  24697  xblss2  24726  stdbdbl  24841  prdsxmslem2  24853  xrtgioo  25131  xrsxmet  25134  cnmpopc  25254  elpi1i  25372  minveclem7  25761  elovolmr  25802  ismbf  25954  mbfmax  25975  itg1val2  26010  mbfi1fseqlem4  26044  itgresr  26104  iblrelem  26116  iblpos  26118  rlimcnp  27298  rlimcnp2  27299  chpchtsum  27551  lgsneg  27653  lgsdilem  27656  2lgslem1a  27723  eqcuts2  28177  n0subs  28754  n0lts1e0  28759  zsoring  28800  bdaypw2n0bndlem  28854  lmiinv  29302  isspthonpth  30340  s3wwlks2on  30550  sps3wwlks2on  30551  clwlkclwwlk  30598  clwwlknonel  30691  clwwlknun  30708  eupth2lem2  30825  frgr3vlem2  30880  numclwwlk2lem1  30982  nrt2irr  31079  minvecolem7  31490  shle0  32049  mdsl2bi  32930  dmdbr5ati  33029  cdj3lem1  33041  rlocisunit  33883  qsfld  34068  eulerpartlemr  35052  subfacp1lem3  36033  satefvfmla1  36276  hfext  37026  bj-issetwt  37879  poimirlem25  38656  poimirlem26  38657  poimirlem27  38658  mblfinlem3  38670  mblfinlem4  38671  mbfresfi  38677  itg2addnclem  38682  itg2addnc  38685  heiborlem10  38847  relssinxpdmrn  39374  dffunsALTV2  39794  dffunsALTV3  39795  dffunsALTV4  39796  elfunsALTV2  39803  elfunsALTV3  39804  elfunsALTV4  39805  elfunsALTV5  39806  dfdisjs2  39819  dfdisjs5  39822  disjimdmqseq  39834  eldisjs2  39845  ople0  40337  atlle0  40455  cdlemg10c  41789  cdlemg33c  41858  hdmap14lem13  43030  mrefg3  43812  onsupneqmaxlim0  44319  onsupnmax  44323  radcnvrat  45391  2ffzoeq  48491