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  1075  cad1  1619  raldifeq  4448  rexreusng  4638  posn  5718  dmxp  5886  elrnmpt1  5917  dfres3  5951  opelres  5952  ffrnbd  6685  fliftf  7271  eroveu  8761  ixpfi2  9262  elfi2  9329  dffi3  9346  cfss  10187  wunex2  10661  nnle1eq1  12187  nn0le0eq0  12441  ixxun  13289  ioopos  13352  injresinj  13719  hashle00  14335  prprrab  14408  xpcogend  14909  cnpart  15175  fz1f1o  15645  nndivdvds  16200  dvdsmultr2  16237  bitsmod  16375  sadadd  16406  sadass  16410  smuval2  16421  smumul  16432  pcmpt  16832  pcmpt2  16833  prmreclem2  16857  prmreclem5  16860  ramcl  16969  mrcidb2  17553  acsfn  17594  fncnvimaeqv  18055  latleeqj1  18386  resmndismnd  18745  pgpssslw  19555  subgdmdprd  19977  resrhm2b  20547  acsfn1p  20744  lssle0  20913  islpir2  21297  islinds3  21801  iscld4  23021  cncnpi  23234  cnprest2  23246  lmss  23254  isconn2  23370  dfconn2  23375  subislly  23437  lly1stc  23452  elptr  23529  txcn  23582  xkoinjcn  23643  tsmsres  24100  isxmet2d  24283  xmetgt0  24314  prdsxmetlem  24324  imasdsf1olem  24329  xblss2  24358  stdbdbl  24473  prdsxmslem2  24485  xrtgioo  24763  xrsxmet  24766  cnmpopc  24890  elpi1i  25014  minveclem7  25403  elovolmr  25445  ismbf  25597  mbfmax  25618  itg1val2  25653  mbfi1fseqlem4  25687  itgresr  25748  iblrelem  25760  iblpos  25762  rlimcnp  26943  rlimcnp2  26944  chpchtsum  27198  lgsneg  27300  lgsdilem  27303  2lgslem1a  27370  eqcuts2  27794  n0subs  28371  n0lts1e0  28376  zsoring  28417  bdaypw2n0bndlem  28471  lmiinv  28876  isspthonpth  29834  s3wwlks2on  30041  sps3wwlks2on  30042  clwlkclwwlk  30089  clwwlknonel  30182  clwwlknun  30199  eupth2lem2  30306  frgr3vlem2  30361  numclwwlk2lem1  30463  nrt2irr  30560  minvecolem7  30970  shle0  31529  mdsl2bi  32410  dmdbr5ati  32509  cdj3lem1  32521  qsfld  33590  eulerpartlemr  34551  subfacp1lem3  35395  satefvfmla1  35638  hfext  36396  bj-issetwt  37117  poimirlem25  37890  poimirlem26  37891  poimirlem27  37892  mblfinlem3  37904  mblfinlem4  37905  mbfresfi  37911  itg2addnclem  37916  itg2addnc  37919  heiborlem10  38065  relssinxpdmrn  38594  dffunsALTV2  39014  dffunsALTV3  39015  dffunsALTV4  39016  elfunsALTV2  39023  elfunsALTV3  39024  elfunsALTV4  39025  elfunsALTV5  39026  dfdisjs2  39039  dfdisjs5  39042  disjimdmqseq  39054  eldisjs2  39065  ople0  39557  atlle0  39675  cdlemg10c  41009  cdlemg33c  41078  hdmap14lem13  42250  mrefg3  43059  onsupneqmaxlim0  43575  onsupnmax  43579  radcnvrat  44664  2ffzoeq  47681