Theorem biantrud 540

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ifptru  1091  cad1  1647  nrmod  3846  raldifeq  4455  rexreusng  4646  posn  5749  dmxp  5921  elrnmpt1  5952  dfres3  5985  opelres  5986  ffrnbd  6723  fliftf  7315  eroveu  8811  ixpfi2  9308  elfi2  9375  dffi3  9392  cfss  10250  wunex2  10724  nnle1eq1  12267  nn0le0eq0  12533  ixxun  13389  ioopos  13452  injresinj  13822  hashle00  14438  prprrab  14512  xpcogend  15013  cnpart  15293  fz1f1o  15763  nndivdvds  16320  dvdsmultr2  16357  bitsmod  16495  sadadd  16526  sadass  16530  smuval2  16541  smumul  16552  pcmpt  16953  pcmpt2  16954  prmreclem2  16978  prmreclem5  16981  ramcl  17090  mrcidb2  17675  acsfn  17716  fncnvimaeqv  18177  latleeqj1  18508  resmndismnd  18867  pgpssslw  19685  subgdmdprd  20107  resrhm2b  20688  acsfn1p  20883  lssle0  21052  islpir2  21479  islinds3  21965  iscld4  23203  cncnpi  23416  cnprest2  23428  lmss  23436  isconn2  23552  dfconn2  23557  subislly  23619  lly1stc  23634  elptr  23711  txcn  23764  xkoinjcn  23825  tsmsres  24282  isxmet2d  24465  xmetgt0  24496  prdsxmetlem  24506  imasdsf1olem  24511  xblss2  24540  stdbdbl  24655  prdsxmslem2  24667  xrtgioo  24945  xrsxmet  24948  cnmpopc  25068  elpi1i  25186  minveclem7  25575  elovolmr  25616  ismbf  25768  mbfmax  25789  itg1val2  25824  mbfi1fseqlem4  25858  itgresr  25919  iblrelem  25931  iblpos  25933  rlimcnp  27108  rlimcnp2  27109  chpchtsum  27361  lgsneg  27463  lgsdilem  27466  2lgslem1a  27533  eqcuts2  27957  n0subs  28534  n0lts1e0  28539  zsoring  28580  bdaypw2n0bndlem  28634  lmiinv  29079  isspthonpth  30076  s3wwlks2on  30283  sps3wwlks2on  30284  clwlkclwwlk  30331  clwwlknonel  30424  clwwlknun  30441  eupth2lem2  30548  frgr3vlem2  30603  numclwwlk2lem1  30705  nrt2irr  30802  minvecolem7  31213  shle0  31772  mdsl2bi  32653  dmdbr5ati  32752  cdj3lem1  32764  rlocisunit  33574  qsfld  33758  eulerpartlemr  34742  subfacp1lem3  35652  satefvfmla1  35895  hfext  36653  bj-issetwt  37488  poimirlem25  38274  poimirlem26  38275  poimirlem27  38276  mblfinlem3  38288  mblfinlem4  38289  mbfresfi  38295  itg2addnclem  38300  itg2addnc  38303  heiborlem10  38449  relssinxpdmrn  38976  dffunsALTV2  39396  dffunsALTV3  39397  dffunsALTV4  39398  elfunsALTV2  39405  elfunsALTV3  39406  elfunsALTV4  39407  elfunsALTV5  39408  dfdisjs2  39421  dfdisjs5  39424  disjimdmqseq  39436  eldisjs2  39447  ople0  39939  atlle0  40057  cdlemg10c  41391  cdlemg33c  41460  hdmap14lem13  42632  mrefg3  43419  onsupneqmaxlim0  43931  onsupnmax  43935  radcnvrat  45004  2ffzoeq  48042