Theorem biantrud 536

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ifptru  1080  cad1  1624  raldifeq  4428  rexreusng  4618  posn  5711  dmxp  5878  elrnmpt1  5909  dfres3  5943  opelres  5944  ffrnbd  6677  fliftf  7266  eroveu  8756  ixpfi2  9257  elfi2  9324  dffi3  9341  cfss  10185  wunex2  10659  nnle1eq1  12205  nn0le0eq0  12463  ixxun  13312  ioopos  13375  injresinj  13744  hashle00  14360  prprrab  14433  xpcogend  14934  cnpart  15200  fz1f1o  15670  nndivdvds  16228  dvdsmultr2  16265  bitsmod  16403  sadadd  16434  sadass  16438  smuval2  16449  smumul  16460  pcmpt  16861  pcmpt2  16862  prmreclem2  16886  prmreclem5  16889  ramcl  16998  mrcidb2  17582  acsfn  17623  fncnvimaeqv  18084  latleeqj1  18415  resmndismnd  18774  pgpssslw  19587  subgdmdprd  20009  resrhm2b  20581  acsfn1p  20778  lssle0  20947  islpir2  21330  islinds3  21816  iscld4  23055  cncnpi  23268  cnprest2  23280  lmss  23288  isconn2  23404  dfconn2  23409  subislly  23471  lly1stc  23486  elptr  23563  txcn  23616  xkoinjcn  23677  tsmsres  24134  isxmet2d  24317  xmetgt0  24348  prdsxmetlem  24358  imasdsf1olem  24363  xblss2  24392  stdbdbl  24507  prdsxmslem2  24519  xrtgioo  24797  xrsxmet  24800  cnmpopc  24920  elpi1i  25038  minveclem7  25427  elovolmr  25468  ismbf  25620  mbfmax  25641  itg1val2  25676  mbfi1fseqlem4  25710  itgresr  25771  iblrelem  25783  iblpos  25785  rlimcnp  26954  rlimcnp2  26955  chpchtsum  27207  lgsneg  27309  lgsdilem  27312  2lgslem1a  27379  eqcuts2  27803  n0subs  28380  n0lts1e0  28385  zsoring  28426  bdaypw2n0bndlem  28480  lmiinv  28885  isspthonpth  29842  s3wwlks2on  30049  sps3wwlks2on  30050  clwlkclwwlk  30097  clwwlknonel  30190  clwwlknun  30207  eupth2lem2  30314  frgr3vlem2  30369  numclwwlk2lem1  30471  nrt2irr  30568  minvecolem7  30979  shle0  31538  mdsl2bi  32419  dmdbr5ati  32518  cdj3lem1  32530  qsfld  33588  eulerpartlemr  34565  subfacp1lem3  35417  satefvfmla1  35660  hfext  36418  bj-issetwt  37235  poimirlem25  38019  poimirlem26  38020  poimirlem27  38021  mblfinlem3  38033  mblfinlem4  38034  mbfresfi  38040  itg2addnclem  38045  itg2addnc  38048  heiborlem10  38194  relssinxpdmrn  38723  dffunsALTV2  39143  dffunsALTV3  39144  dffunsALTV4  39145  elfunsALTV2  39152  elfunsALTV3  39153  elfunsALTV4  39154  elfunsALTV5  39155  dfdisjs2  39168  dfdisjs5  39171  disjimdmqseq  39183  eldisjs2  39194  ople0  39686  atlle0  39804  cdlemg10c  41138  cdlemg33c  41207  hdmap14lem13  42379  mrefg3  43164  onsupneqmaxlim0  43676  onsupnmax  43680  radcnvrat  44765  2ffzoeq  47798