Theorem biantrud 541

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ifptru  1091  cad1  1650  nrmod  3848  raldifeq  4459  rexreusng  4650  posn  5752  dmxp  5924  elrnmpt1  5955  dfres3  5988  opelres  5989  ffrnbd  6728  fliftf  7324  eroveu  8819  ixpfi2  9317  elfi2  9384  dffi3  9401  cfss  10267  wunex2  10741  nnle1eq1  12284  nn0le0eq0  12550  ixxun  13406  ioopos  13469  injresinj  13839  hashle00  14456  prprrab  14530  xpcogend  15037  cnpart  15317  fz1f1o  15787  nndivdvds  16344  dvdsmultr2  16381  bitsmod  16519  sadadd  16550  sadass  16554  smuval2  16565  smumul  16576  pcmpt  16977  pcmpt2  16978  prmreclem2  17002  prmreclem5  17005  ramcl  17114  mrcidb2  17699  acsfn  17740  fncnvimaeqv  18201  latleeqj1  18532  resmndismnd  18897  pgpssslw  19715  subgdmdprd  20137  resrhm2b  20738  acsfn1p  20939  lssle0  21108  islpir2  21535  islinds3  22021  iscld4  23259  cncnpi  23472  cnprest2  23484  lmss  23492  isconn2  23608  dfconn2  23613  subislly  23675  lly1stc  23690  elptr  23767  txcn  23820  xkoinjcn  23881  tsmsres  24338  isxmet2d  24521  xmetgt0  24552  prdsxmetlem  24562  imasdsf1olem  24567  xblss2  24596  stdbdbl  24711  prdsxmslem2  24723  xrtgioo  25001  xrsxmet  25004  cnmpopc  25124  elpi1i  25242  minveclem7  25631  elovolmr  25672  ismbf  25824  mbfmax  25845  itg1val2  25880  mbfi1fseqlem4  25914  itgresr  25975  iblrelem  25987  iblpos  25989  rlimcnp  27167  rlimcnp2  27168  chpchtsum  27420  lgsneg  27522  lgsdilem  27525  2lgslem1a  27592  eqcuts2  28016  n0subs  28593  n0lts1e0  28598  zsoring  28639  bdaypw2n0bndlem  28693  lmiinv  29138  isspthonpth  30135  s3wwlks2on  30342  sps3wwlks2on  30343  clwlkclwwlk  30390  clwwlknonel  30483  clwwlknun  30500  eupth2lem2  30607  frgr3vlem2  30662  numclwwlk2lem1  30764  nrt2irr  30861  minvecolem7  31272  shle0  31831  mdsl2bi  32712  dmdbr5ati  32811  cdj3lem1  32823  rlocisunit  33627  qsfld  33811  eulerpartlemr  34796  subfacp1lem3  35695  satefvfmla1  35938  hfext  36696  bj-issetwt  37551  poimirlem25  38337  poimirlem26  38338  poimirlem27  38339  mblfinlem3  38351  mblfinlem4  38352  mbfresfi  38358  itg2addnclem  38363  itg2addnc  38366  heiborlem10  38512  relssinxpdmrn  39039  dffunsALTV2  39459  dffunsALTV3  39460  dffunsALTV4  39461  elfunsALTV2  39468  elfunsALTV3  39469  elfunsALTV4  39470  elfunsALTV5  39471  dfdisjs2  39484  dfdisjs5  39487  disjimdmqseq  39499  eldisjs2  39510  ople0  40002  atlle0  40120  cdlemg10c  41454  cdlemg33c  41523  hdmap14lem13  42695  mrefg3  43480  onsupneqmaxlim0  43992  onsupnmax  43996  radcnvrat  45065  2ffzoeq  48106