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  4443  rexreusng  4631  posn  5705  dmxp  5873  elrnmpt1  5904  dfres3  5937  opelres  5938  ffrnbd  6671  fliftf  7255  eroveu  8742  ixpfi2  9241  elfi2  9305  dffi3  9322  cfss  10163  wunex2  10636  nnle1eq1  12162  nn0le0eq0  12416  ixxun  13263  ioopos  13326  injresinj  13693  hashle00  14309  prprrab  14382  xpcogend  14883  cnpart  15149  fz1f1o  15619  nndivdvds  16174  dvdsmultr2  16211  bitsmod  16349  sadadd  16380  sadass  16384  smuval2  16395  smumul  16406  pcmpt  16806  pcmpt2  16807  prmreclem2  16831  prmreclem5  16834  ramcl  16943  mrcidb2  17526  acsfn  17567  fncnvimaeqv  18028  latleeqj1  18359  resmndismnd  18718  pgpssslw  19528  subgdmdprd  19950  resrhm2b  20519  acsfn1p  20716  lssle0  20885  islpir2  21269  islinds3  21773  iscld4  22981  cncnpi  23194  cnprest2  23206  lmss  23214  isconn2  23330  dfconn2  23335  subislly  23397  lly1stc  23412  elptr  23489  txcn  23542  xkoinjcn  23603  tsmsres  24060  isxmet2d  24243  xmetgt0  24274  prdsxmetlem  24284  imasdsf1olem  24289  xblss2  24318  stdbdbl  24433  prdsxmslem2  24445  xrtgioo  24723  xrsxmet  24726  cnmpopc  24850  elpi1i  24974  minveclem7  25363  elovolmr  25405  ismbf  25557  mbfmax  25578  itg1val2  25613  mbfi1fseqlem4  25647  itgresr  25708  iblrelem  25720  iblpos  25722  rlimcnp  26903  rlimcnp2  26904  chpchtsum  27158  lgsneg  27260  lgsdilem  27263  2lgslem1a  27330  eqscut2  27748  n0subs  28290  zsoring  28333  lmiinv  28771  isspthonpth  29729  s3wwlks2on  29936  sps3wwlks2on  29937  clwlkclwwlk  29984  clwwlknonel  30077  clwwlknun  30094  eupth2lem2  30201  frgr3vlem2  30256  numclwwlk2lem1  30358  nrt2irr  30455  minvecolem7  30865  shle0  31424  mdsl2bi  32305  dmdbr5ati  32404  cdj3lem1  32416  qsfld  33470  eulerpartlemr  34408  subfacp1lem3  35247  satefvfmla1  35490  hfext  36248  bj-issetwt  36940  poimirlem25  37705  poimirlem26  37706  poimirlem27  37707  mblfinlem3  37719  mblfinlem4  37720  mbfresfi  37726  itg2addnclem  37731  itg2addnc  37734  heiborlem10  37880  relssinxpdmrn  38401  dffunsALTV2  38802  dffunsALTV3  38803  dffunsALTV4  38804  elfunsALTV2  38811  elfunsALTV3  38812  elfunsALTV4  38813  elfunsALTV5  38814  dfdisjs2  38827  dfdisjs5  38830  eldisjs2  38841  ople0  39306  atlle0  39424  cdlemg10c  40758  cdlemg33c  40827  hdmap14lem13  41999  mrefg3  42825  onsupneqmaxlim0  43341  onsupnmax  43345  radcnvrat  44431  2ffzoeq  47451