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  4457  rexreusng  4643  posn  5724  dmxp  5892  elrnmpt1  5924  dfres3  5955  opelres  5956  ffrnbd  6703  fliftf  7290  eroveu  8785  ixpfi2  9301  elfi2  9365  dffi3  9382  cfss  10218  wunex2  10691  nnle1eq1  12216  nn0le0eq0  12470  ixxun  13322  ioopos  13385  injresinj  13749  hashle00  14365  prprrab  14438  xpcogend  14940  cnpart  15206  fz1f1o  15676  nndivdvds  16231  dvdsmultr2  16268  bitsmod  16406  sadadd  16437  sadass  16441  smuval2  16452  smumul  16463  pcmpt  16863  pcmpt2  16864  prmreclem2  16888  prmreclem5  16891  ramcl  17000  mrcidb2  17579  acsfn  17620  fncnvimaeqv  18081  latleeqj1  18410  resmndismnd  18735  pgpssslw  19544  subgdmdprd  19966  resrhm2b  20511  acsfn1p  20708  lssle0  20856  islpir2  21240  islinds3  21743  iscld4  22952  cncnpi  23165  cnprest2  23177  lmss  23185  isconn2  23301  dfconn2  23306  subislly  23368  lly1stc  23383  elptr  23460  txcn  23513  xkoinjcn  23574  tsmsres  24031  isxmet2d  24215  xmetgt0  24246  prdsxmetlem  24256  imasdsf1olem  24261  xblss2  24290  stdbdbl  24405  prdsxmslem2  24417  xrtgioo  24695  xrsxmet  24698  cnmpopc  24822  elpi1i  24946  minveclem7  25335  elovolmr  25377  ismbf  25529  mbfmax  25550  itg1val2  25585  mbfi1fseqlem4  25619  itgresr  25680  iblrelem  25692  iblpos  25694  rlimcnp  26875  rlimcnp2  26876  chpchtsum  27130  lgsneg  27232  lgsdilem  27235  2lgslem1a  27302  eqscut2  27718  n0subs  28253  lmiinv  28719  isspthonpth  29679  s3wwlks2on  29886  clwlkclwwlk  29931  clwwlknonel  30024  clwwlknun  30041  eupth2lem2  30148  frgr3vlem2  30203  numclwwlk2lem1  30305  nrt2irr  30402  minvecolem7  30812  shle0  31371  mdsl2bi  32252  dmdbr5ati  32351  cdj3lem1  32363  qsfld  33469  eulerpartlemr  34365  subfacp1lem3  35169  satefvfmla1  35412  hfext  36171  bj-issetwt  36863  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  mblfinlem3  37653  mblfinlem4  37654  mbfresfi  37660  itg2addnclem  37665  itg2addnc  37668  heiborlem10  37814  relssinxpdmrn  38331  dffunsALTV2  38676  dffunsALTV3  38677  dffunsALTV4  38678  elfunsALTV2  38685  elfunsALTV3  38686  elfunsALTV4  38687  elfunsALTV5  38688  dfdisjs2  38701  dfdisjs5  38704  eldisjs2  38715  ople0  39180  atlle0  39298  cdlemg10c  40633  cdlemg33c  40702  hdmap14lem13  41874  mrefg3  42696  onsupneqmaxlim0  43213  onsupnmax  43217  radcnvrat  44303  2ffzoeq  47328