Theorem biantrud 534

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 530	. 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:  ifptru  1068  cad1  1617  raldifeq  4441  rexreusng  4619  posn  5639  elrnmpt1  5832  dfres3  5860  opelres  5861  fliftf  7070  eroveu  8394  ixpfi2  8824  elfi2  8880  dffi3  8897  cfss  9689  wunex2  10162  nnle1eq1  11670  nn0le0eq0  11928  ixxun  12757  ioopos  12816  injresinj  13161  hashle00  13764  prprrab  13834  xpcogend  14336  cnpart  14601  fz1f1o  15069  nndivdvds  15618  dvdsmultr2  15651  bitsmod  15787  sadadd  15818  sadass  15822  smuval2  15833  smumul  15844  pcmpt  16230  pcmpt2  16231  prmreclem2  16255  prmreclem5  16258  ramcl  16367  mrcidb2  16891  acsfn  16932  fncnvimaeqv  17372  latleeqj1  17675  resmndismnd  17975  pgpssslw  18741  subgdmdprd  19158  acsfn1p  19580  lssle0  19723  islpir2  20026  islinds3  20980  iscld4  21675  cncnpi  21888  cnprest2  21900  lmss  21908  isconn2  22024  dfconn2  22029  subislly  22091  lly1stc  22106  elptr  22183  txcn  22236  xkoinjcn  22297  tsmsres  22754  isxmet2d  22939  xmetgt0  22970  prdsxmetlem  22980  imasdsf1olem  22985  xblss2  23014  stdbdbl  23129  prdsxmslem2  23141  xrtgioo  23416  xrsxmet  23419  cnmpopc  23534  elpi1i  23652  minveclem7  24040  elovolmr  24079  ismbf  24231  mbfmax  24252  itg1val2  24287  mbfi1fseqlem4  24321  itgresr  24381  iblrelem  24393  iblpos  24395  rlimcnp  25545  rlimcnp2  25546  chpchtsum  25797  lgsneg  25899  lgsdilem  25902  2lgslem1a  25969  lmiinv  26580  isspthonpth  27532  s3wwlks2on  27737  clwlkclwwlk  27782  clwwlknonel  27876  clwwlknun  27893  eupth2lem2  28000  frgr3vlem2  28055  numclwwlk2lem1  28157  minvecolem7  28662  shle0  29221  mdsl2bi  30102  dmdbr5ati  30201  cdj3lem1  30213  eulerpartlemr  31634  subfacp1lem3  32431  satefvfmla1  32674  hfext  33646  bj-issetwt  34191  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  mblfinlem3  34933  mblfinlem4  34934  mbfresfi  34940  itg2addnclem  34945  itg2addnc  34948  heiborlem10  35100  dffunsALTV2  35919  dffunsALTV3  35920  dffunsALTV4  35921  elfunsALTV2  35928  elfunsALTV3  35929  elfunsALTV4  35930  elfunsALTV5  35931  dfdisjs2  35944  dfdisjs5  35947  eldisjs2  35958  ople0  36325  atlle0  36443  cdlemg10c  37777  cdlemg33c  37846  hdmap14lem13  39018  mrefg3  39312  radcnvrat  40653  2ffzoeq  43535