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  1617  raldifeq  4447  rexreusng  4633  posn  5709  dmxp  5875  elrnmpt1  5906  dfres3  5939  opelres  5940  ffrnbd  6671  fliftf  7256  eroveu  8746  ixpfi2  9259  elfi2  9323  dffi3  9340  cfss  10178  wunex2  10651  nnle1eq1  12176  nn0le0eq0  12430  ixxun  13282  ioopos  13345  injresinj  13709  hashle00  14325  prprrab  14398  xpcogend  14899  cnpart  15165  fz1f1o  15635  nndivdvds  16190  dvdsmultr2  16227  bitsmod  16365  sadadd  16396  sadass  16400  smuval2  16411  smumul  16422  pcmpt  16822  pcmpt2  16823  prmreclem2  16847  prmreclem5  16850  ramcl  16959  mrcidb2  17542  acsfn  17583  fncnvimaeqv  18044  latleeqj1  18375  resmndismnd  18700  pgpssslw  19511  subgdmdprd  19933  resrhm2b  20505  acsfn1p  20702  lssle0  20871  islpir2  21255  islinds3  21759  iscld4  22968  cncnpi  23181  cnprest2  23193  lmss  23201  isconn2  23317  dfconn2  23322  subislly  23384  lly1stc  23399  elptr  23476  txcn  23529  xkoinjcn  23590  tsmsres  24047  isxmet2d  24231  xmetgt0  24262  prdsxmetlem  24272  imasdsf1olem  24277  xblss2  24306  stdbdbl  24421  prdsxmslem2  24433  xrtgioo  24711  xrsxmet  24714  cnmpopc  24838  elpi1i  24962  minveclem7  25351  elovolmr  25393  ismbf  25545  mbfmax  25566  itg1val2  25601  mbfi1fseqlem4  25635  itgresr  25696  iblrelem  25708  iblpos  25710  rlimcnp  26891  rlimcnp2  26892  chpchtsum  27146  lgsneg  27248  lgsdilem  27251  2lgslem1a  27318  eqscut2  27735  n0subs  28276  zsoring  28319  lmiinv  28755  isspthonpth  29712  s3wwlks2on  29919  clwlkclwwlk  29964  clwwlknonel  30057  clwwlknun  30074  eupth2lem2  30181  frgr3vlem2  30236  numclwwlk2lem1  30338  nrt2irr  30435  minvecolem7  30845  shle0  31404  mdsl2bi  32285  dmdbr5ati  32384  cdj3lem1  32396  qsfld  33445  eulerpartlemr  34341  subfacp1lem3  35154  satefvfmla1  35397  hfext  36156  bj-issetwt  36848  poimirlem25  37624  poimirlem26  37625  poimirlem27  37626  mblfinlem3  37638  mblfinlem4  37639  mbfresfi  37645  itg2addnclem  37650  itg2addnc  37653  heiborlem10  37799  relssinxpdmrn  38316  dffunsALTV2  38661  dffunsALTV3  38662  dffunsALTV4  38663  elfunsALTV2  38670  elfunsALTV3  38671  elfunsALTV4  38672  elfunsALTV5  38673  dfdisjs2  38686  dfdisjs5  38689  eldisjs2  38700  ople0  39165  atlle0  39283  cdlemg10c  40618  cdlemg33c  40687  hdmap14lem13  41859  mrefg3  42681  onsupneqmaxlim0  43197  onsupnmax  43201  radcnvrat  44287  2ffzoeq  47312