Theorem biantrud 531

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  ifptru  1072  cad1  1620  raldifeq  4421  rexreusng  4612  posn  5663  elrnmpt1  5856  dfres3  5885  opelres  5886  ffrnbd  6600  fliftf  7166  eroveu  8559  ixpfi2  9047  elfi2  9103  dffi3  9120  cfss  9952  wunex2  10425  nnle1eq1  11933  nn0le0eq0  12191  ixxun  13024  ioopos  13085  injresinj  13436  hashle00  14043  prprrab  14115  xpcogend  14613  cnpart  14879  fz1f1o  15350  nndivdvds  15900  dvdsmultr2  15935  bitsmod  16071  sadadd  16102  sadass  16106  smuval2  16117  smumul  16128  pcmpt  16521  pcmpt2  16522  prmreclem2  16546  prmreclem5  16549  ramcl  16658  mrcidb2  17244  acsfn  17285  fncnvimaeqv  17752  latleeqj1  18084  resmndismnd  18362  pgpssslw  19134  subgdmdprd  19552  acsfn1p  19982  lssle0  20126  islpir2  20435  islinds3  20951  iscld4  22124  cncnpi  22337  cnprest2  22349  lmss  22357  isconn2  22473  dfconn2  22478  subislly  22540  lly1stc  22555  elptr  22632  txcn  22685  xkoinjcn  22746  tsmsres  23203  isxmet2d  23388  xmetgt0  23419  prdsxmetlem  23429  imasdsf1olem  23434  xblss2  23463  stdbdbl  23579  prdsxmslem2  23591  xrtgioo  23875  xrsxmet  23878  cnmpopc  23997  elpi1i  24115  minveclem7  24504  elovolmr  24545  ismbf  24697  mbfmax  24718  itg1val2  24753  mbfi1fseqlem4  24788  itgresr  24848  iblrelem  24860  iblpos  24862  rlimcnp  26020  rlimcnp2  26021  chpchtsum  26272  lgsneg  26374  lgsdilem  26377  2lgslem1a  26444  lmiinv  27057  isspthonpth  28018  s3wwlks2on  28222  clwlkclwwlk  28267  clwwlknonel  28360  clwwlknun  28377  eupth2lem2  28484  frgr3vlem2  28539  numclwwlk2lem1  28641  minvecolem7  29146  shle0  29705  mdsl2bi  30586  dmdbr5ati  30685  cdj3lem1  30697  eulerpartlemr  32241  subfacp1lem3  33044  satefvfmla1  33287  eqscut2  33927  hfext  34412  bj-issetwt  34986  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  mblfinlem3  35743  mblfinlem4  35744  mbfresfi  35750  itg2addnclem  35755  itg2addnc  35758  heiborlem10  35905  dffunsALTV2  36722  dffunsALTV3  36723  dffunsALTV4  36724  elfunsALTV2  36731  elfunsALTV3  36732  elfunsALTV4  36733  elfunsALTV5  36734  dfdisjs2  36747  dfdisjs5  36750  eldisjs2  36761  ople0  37128  atlle0  37246  cdlemg10c  38580  cdlemg33c  38649  hdmap14lem13  39821  mrefg3  40446  radcnvrat  41821  2ffzoeq  44708