Theorem biantrud 532

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  ifptru  1073  cad1  1619  raldifeq  4425  rexreusng  4616  posn  5673  elrnmpt1  5870  dfres3  5899  opelres  5900  ffrnbd  6625  fliftf  7195  eroveu  8610  ixpfi2  9126  elfi2  9182  dffi3  9199  cfss  10030  wunex2  10503  nnle1eq1  12012  nn0le0eq0  12270  ixxun  13104  ioopos  13165  injresinj  13517  hashle00  14124  prprrab  14196  xpcogend  14694  cnpart  14960  fz1f1o  15431  nndivdvds  15981  dvdsmultr2  16016  bitsmod  16152  sadadd  16183  sadass  16187  smuval2  16198  smumul  16209  pcmpt  16602  pcmpt2  16603  prmreclem2  16627  prmreclem5  16630  ramcl  16739  mrcidb2  17336  acsfn  17377  fncnvimaeqv  17845  latleeqj1  18178  resmndismnd  18456  pgpssslw  19228  subgdmdprd  19646  acsfn1p  20076  lssle0  20220  islpir2  20531  islinds3  21050  iscld4  22225  cncnpi  22438  cnprest2  22450  lmss  22458  isconn2  22574  dfconn2  22579  subislly  22641  lly1stc  22656  elptr  22733  txcn  22786  xkoinjcn  22847  tsmsres  23304  isxmet2d  23489  xmetgt0  23520  prdsxmetlem  23530  imasdsf1olem  23535  xblss2  23564  stdbdbl  23682  prdsxmslem2  23694  xrtgioo  23978  xrsxmet  23981  cnmpopc  24100  elpi1i  24218  minveclem7  24608  elovolmr  24649  ismbf  24801  mbfmax  24822  itg1val2  24857  mbfi1fseqlem4  24892  itgresr  24952  iblrelem  24964  iblpos  24966  rlimcnp  26124  rlimcnp2  26125  chpchtsum  26376  lgsneg  26478  lgsdilem  26481  2lgslem1a  26548  lmiinv  27162  isspthonpth  28126  s3wwlks2on  28330  clwlkclwwlk  28375  clwwlknonel  28468  clwwlknun  28485  eupth2lem2  28592  frgr3vlem2  28647  numclwwlk2lem1  28749  minvecolem7  29254  shle0  29813  mdsl2bi  30694  dmdbr5ati  30793  cdj3lem1  30805  eulerpartlemr  32350  subfacp1lem3  33153  satefvfmla1  33396  eqscut2  34009  hfext  34494  bj-issetwt  35068  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  mblfinlem3  35825  mblfinlem4  35826  mbfresfi  35832  itg2addnclem  35837  itg2addnc  35840  heiborlem10  35987  dffunsALTV2  36802  dffunsALTV3  36803  dffunsALTV4  36804  elfunsALTV2  36811  elfunsALTV3  36812  elfunsALTV4  36813  elfunsALTV5  36814  dfdisjs2  36827  dfdisjs5  36830  eldisjs2  36841  ople0  37208  atlle0  37326  cdlemg10c  38660  cdlemg33c  38729  hdmap14lem13  39901  mrefg3  40537  radcnvrat  41939  2ffzoeq  44831