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 206   ∧ 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 207  df-an 396

This theorem is referenced by:  ifptru  1074  cad1  1618  raldifeq  4444  rexreusng  4632  posn  5702  dmxp  5869  elrnmpt1  5900  dfres3  5933  opelres  5934  ffrnbd  6666  fliftf  7249  eroveu  8736  ixpfi2  9234  elfi2  9298  dffi3  9315  cfss  10153  wunex2  10626  nnle1eq1  12152  nn0le0eq0  12406  ixxun  13258  ioopos  13321  injresinj  13688  hashle00  14304  prprrab  14377  xpcogend  14878  cnpart  15144  fz1f1o  15614  nndivdvds  16169  dvdsmultr2  16206  bitsmod  16344  sadadd  16375  sadass  16379  smuval2  16390  smumul  16401  pcmpt  16801  pcmpt2  16802  prmreclem2  16826  prmreclem5  16829  ramcl  16938  mrcidb2  17521  acsfn  17562  fncnvimaeqv  18023  latleeqj1  18354  resmndismnd  18713  pgpssslw  19524  subgdmdprd  19946  resrhm2b  20515  acsfn1p  20712  lssle0  20881  islpir2  21265  islinds3  21769  iscld4  22978  cncnpi  23191  cnprest2  23203  lmss  23211  isconn2  23327  dfconn2  23332  subislly  23394  lly1stc  23409  elptr  23486  txcn  23539  xkoinjcn  23600  tsmsres  24057  isxmet2d  24240  xmetgt0  24271  prdsxmetlem  24281  imasdsf1olem  24286  xblss2  24315  stdbdbl  24430  prdsxmslem2  24442  xrtgioo  24720  xrsxmet  24723  cnmpopc  24847  elpi1i  24971  minveclem7  25360  elovolmr  25402  ismbf  25554  mbfmax  25575  itg1val2  25610  mbfi1fseqlem4  25644  itgresr  25705  iblrelem  25717  iblpos  25719  rlimcnp  26900  rlimcnp2  26901  chpchtsum  27155  lgsneg  27257  lgsdilem  27260  2lgslem1a  27327  eqscut2  27745  n0subs  28287  zsoring  28330  lmiinv  28768  isspthonpth  29725  s3wwlks2on  29932  clwlkclwwlk  29977  clwwlknonel  30070  clwwlknun  30087  eupth2lem2  30194  frgr3vlem2  30249  numclwwlk2lem1  30351  nrt2irr  30448  minvecolem7  30858  shle0  31417  mdsl2bi  32298  dmdbr5ati  32397  cdj3lem1  32409  qsfld  33458  eulerpartlemr  34382  subfacp1lem3  35214  satefvfmla1  35457  hfext  36216  bj-issetwt  36908  poimirlem25  37684  poimirlem26  37685  poimirlem27  37686  mblfinlem3  37698  mblfinlem4  37699  mbfresfi  37705  itg2addnclem  37710  itg2addnc  37713  heiborlem10  37859  relssinxpdmrn  38376  dffunsALTV2  38721  dffunsALTV3  38722  dffunsALTV4  38723  elfunsALTV2  38730  elfunsALTV3  38731  elfunsALTV4  38732  elfunsALTV5  38733  dfdisjs2  38746  dfdisjs5  38749  eldisjs2  38760  ople0  39225  atlle0  39343  cdlemg10c  40677  cdlemg33c  40746  hdmap14lem13  41918  mrefg3  42740  onsupneqmaxlim0  43256  onsupnmax  43260  radcnvrat  44346  2ffzoeq  47357