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  1616  raldifeq  4442  rexreusng  4620  posn  5640  elrnmpt1  5833  dfres3  5861  opelres  5862  fliftf  7071  eroveu  8395  ixpfi2  8825  elfi2  8881  dffi3  8898  cfss  9690  wunex2  10163  nnle1eq1  11670  nn0le0eq0  11928  ixxun  12757  ioopos  12816  injresinj  13161  hashle00  13764  prprrab  13834  xpcogend  14337  cnpart  14602  fz1f1o  15070  nndivdvds  15619  dvdsmultr2  15652  bitsmod  15788  sadadd  15819  sadass  15823  smuval2  15834  smumul  15845  pcmpt  16231  pcmpt2  16232  prmreclem2  16256  prmreclem5  16259  ramcl  16368  mrcidb2  16892  acsfn  16933  fncnvimaeqv  17373  latleeqj1  17676  resmndismnd  17976  pgpssslw  18742  subgdmdprd  19159  acsfn1p  19581  lssle0  19724  islpir2  20027  islinds3  20981  iscld4  21676  cncnpi  21889  cnprest2  21901  lmss  21909  isconn2  22025  dfconn2  22030  subislly  22092  lly1stc  22107  elptr  22184  txcn  22237  xkoinjcn  22298  tsmsres  22755  isxmet2d  22940  xmetgt0  22971  prdsxmetlem  22981  imasdsf1olem  22986  xblss2  23015  stdbdbl  23130  prdsxmslem2  23142  xrtgioo  23417  xrsxmet  23420  cnmpopc  23535  elpi1i  23653  minveclem7  24041  elovolmr  24080  ismbf  24232  mbfmax  24253  itg1val2  24288  mbfi1fseqlem4  24322  itgresr  24382  iblrelem  24394  iblpos  24396  rlimcnp  25546  rlimcnp2  25547  chpchtsum  25798  lgsneg  25900  lgsdilem  25903  2lgslem1a  25970  lmiinv  26581  isspthonpth  27533  s3wwlks2on  27738  clwlkclwwlk  27783  clwwlknonel  27877  clwwlknun  27894  eupth2lem2  28001  frgr3vlem2  28056  numclwwlk2lem1  28158  minvecolem7  28663  shle0  29222  mdsl2bi  30103  dmdbr5ati  30202  cdj3lem1  30214  eulerpartlemr  31636  subfacp1lem3  32433  satefvfmla1  32676  hfext  33648  bj-issetwt  34193  poimirlem25  34921  poimirlem26  34922  poimirlem27  34923  mblfinlem3  34935  mblfinlem4  34936  mbfresfi  34942  itg2addnclem  34947  itg2addnc  34950  heiborlem10  35102  dffunsALTV2  35921  dffunsALTV3  35922  dffunsALTV4  35923  elfunsALTV2  35930  elfunsALTV3  35931  elfunsALTV4  35932  elfunsALTV5  35933  dfdisjs2  35946  dfdisjs5  35949  eldisjs2  35960  ople0  36327  atlle0  36445  cdlemg10c  37779  cdlemg33c  37848  hdmap14lem13  39020  mrefg3  39311  radcnvrat  40652  2ffzoeq  43535