Theorem biantrud 530

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ifptru  1072  cad1  1616  raldifeq  4492  rexreusng  4682  posn  5760  elrnmpt1  5956  dfres3  5985  opelres  5986  ffrnbd  6732  fliftf  7314  eroveu  8808  ixpfi2  9352  elfi2  9411  dffi3  9428  cfss  10262  wunex2  10735  nnle1eq1  12246  nn0le0eq0  12504  ixxun  13344  ioopos  13405  injresinj  13757  hashle00  14364  prprrab  14438  xpcogend  14925  cnpart  15191  fz1f1o  15660  nndivdvds  16210  dvdsmultr2  16245  bitsmod  16381  sadadd  16412  sadass  16416  smuval2  16427  smumul  16438  pcmpt  16829  pcmpt2  16830  prmreclem2  16854  prmreclem5  16857  ramcl  16966  mrcidb2  17566  acsfn  17607  fncnvimaeqv  18075  latleeqj1  18408  resmndismnd  18725  pgpssslw  19523  subgdmdprd  19945  resrhm2b  20492  acsfn1p  20558  lssle0  20704  islpir2  21089  islinds3  21608  iscld4  22789  cncnpi  23002  cnprest2  23014  lmss  23022  isconn2  23138  dfconn2  23143  subislly  23205  lly1stc  23220  elptr  23297  txcn  23350  xkoinjcn  23411  tsmsres  23868  isxmet2d  24053  xmetgt0  24084  prdsxmetlem  24094  imasdsf1olem  24099  xblss2  24128  stdbdbl  24246  prdsxmslem2  24258  xrtgioo  24542  xrsxmet  24545  cnmpopc  24669  elpi1i  24793  minveclem7  25183  elovolmr  25225  ismbf  25377  mbfmax  25398  itg1val2  25433  mbfi1fseqlem4  25468  itgresr  25528  iblrelem  25540  iblpos  25542  rlimcnp  26706  rlimcnp2  26707  chpchtsum  26958  lgsneg  27060  lgsdilem  27063  2lgslem1a  27130  eqscut2  27544  lmiinv  28310  isspthonpth  29273  s3wwlks2on  29477  clwlkclwwlk  29522  clwwlknonel  29615  clwwlknun  29632  eupth2lem2  29739  frgr3vlem2  29794  numclwwlk2lem1  29896  nrt2irr  29993  minvecolem7  30403  shle0  30962  mdsl2bi  31843  dmdbr5ati  31942  cdj3lem1  31954  qsfld  32886  eulerpartlemr  33671  subfacp1lem3  34471  satefvfmla1  34714  hfext  35459  bj-issetwt  36057  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  mblfinlem3  36830  mblfinlem4  36831  mbfresfi  36837  itg2addnclem  36842  itg2addnc  36845  heiborlem10  36991  relssinxpdmrn  37521  dffunsALTV2  37857  dffunsALTV3  37858  dffunsALTV4  37859  elfunsALTV2  37866  elfunsALTV3  37867  elfunsALTV4  37868  elfunsALTV5  37869  dfdisjs2  37882  dfdisjs5  37885  eldisjs2  37896  ople0  38360  atlle0  38478  cdlemg10c  39813  cdlemg33c  39882  hdmap14lem13  41054  mrefg3  41748  onsupneqmaxlim0  42275  onsupnmax  42279  radcnvrat  43375  2ffzoeq  46334