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  1074  cad1  1618  raldifeq  4492  rexreusng  4682  posn  5759  elrnmpt1  5955  dfres3  5984  opelres  5985  ffrnbd  6730  fliftf  7308  eroveu  8802  ixpfi2  9346  elfi2  9405  dffi3  9422  cfss  10256  wunex2  10729  nnle1eq1  12238  nn0le0eq0  12496  ixxun  13336  ioopos  13397  injresinj  13749  hashle00  14356  prprrab  14430  xpcogend  14917  cnpart  15183  fz1f1o  15652  nndivdvds  16202  dvdsmultr2  16237  bitsmod  16373  sadadd  16404  sadass  16408  smuval2  16419  smumul  16430  pcmpt  16821  pcmpt2  16822  prmreclem2  16846  prmreclem5  16849  ramcl  16958  mrcidb2  17558  acsfn  17599  fncnvimaeqv  18067  latleeqj1  18400  resmndismnd  18685  pgpssslw  19476  subgdmdprd  19898  resrhm2b  20386  acsfn1p  20407  lssle0  20552  islpir2  20881  islinds3  21380  iscld4  22560  cncnpi  22773  cnprest2  22785  lmss  22793  isconn2  22909  dfconn2  22914  subislly  22976  lly1stc  22991  elptr  23068  txcn  23121  xkoinjcn  23182  tsmsres  23639  isxmet2d  23824  xmetgt0  23855  prdsxmetlem  23865  imasdsf1olem  23870  xblss2  23899  stdbdbl  24017  prdsxmslem2  24029  xrtgioo  24313  xrsxmet  24316  cnmpopc  24435  elpi1i  24553  minveclem7  24943  elovolmr  24984  ismbf  25136  mbfmax  25157  itg1val2  25192  mbfi1fseqlem4  25227  itgresr  25287  iblrelem  25299  iblpos  25301  rlimcnp  26459  rlimcnp2  26460  chpchtsum  26711  lgsneg  26813  lgsdilem  26816  2lgslem1a  26883  eqscut2  27296  lmiinv  28032  isspthonpth  28995  s3wwlks2on  29199  clwlkclwwlk  29244  clwwlknonel  29337  clwwlknun  29354  eupth2lem2  29461  frgr3vlem2  29516  numclwwlk2lem1  29618  minvecolem7  30123  shle0  30682  mdsl2bi  31563  dmdbr5ati  31662  cdj3lem1  31674  qsfld  32600  eulerpartlemr  33361  subfacp1lem3  34161  satefvfmla1  34404  hfext  35143  bj-issetwt  35742  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  mblfinlem3  36515  mblfinlem4  36516  mbfresfi  36522  itg2addnclem  36527  itg2addnc  36530  heiborlem10  36676  relssinxpdmrn  37206  dffunsALTV2  37542  dffunsALTV3  37543  dffunsALTV4  37544  elfunsALTV2  37551  elfunsALTV3  37552  elfunsALTV4  37553  elfunsALTV5  37554  dfdisjs2  37567  dfdisjs5  37570  eldisjs2  37581  ople0  38045  atlle0  38163  cdlemg10c  39498  cdlemg33c  39567  hdmap14lem13  40739  mrefg3  41431  onsupneqmaxlim0  41958  onsupnmax  41962  radcnvrat  43058  2ffzoeq  46022