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  3842  raldifeq  4452  rexreusng  4643  posn  5745  dmxp  5917  elrnmpt1  5948  dfres3  5981  opelres  5982  ffrnbd  6722  fliftf  7320  eroveu  8816  ixpfi2  9321  elfi2  9388  dffi3  9405  cfss  10271  wunex2  10751  nnle1eq1  12294  nn0le0eq0  12560  ixxun  13418  ioopos  13481  injresinj  13851  hashle00  14468  prprrab  14542  xpcogend  15051  cnpart  15331  fz1f1o  15800  nndivdvds  16357  dvdsmultr2  16394  bitsmod  16532  sadadd  16563  sadass  16567  smuval2  16578  smumul  16589  pcmpt  16990  pcmpt2  16991  prmreclem2  17015  prmreclem5  17018  ramcl  17127  mrcidb2  17712  acsfn  17753  fncnvimaeqv  18214  latleeqj1  18545  resmndismnd  18922  pgpssslw  19747  subgdmdprd  20169  resrhm2b  20770  acsfn1p  20971  lssle0  21140  islpir2  21567  islinds3  22053  iscld4  23296  cncnpi  23509  cnprest2  23521  lmss  23529  isconn2  23645  dfconn2  23650  subislly  23713  lly1stc  23728  elptr  23805  txcn  23858  xkoinjcn  23919  tsmsres  24376  isxmet2d  24559  xmetgt0  24590  prdsxmetlem  24600  imasdsf1olem  24605  xblss2  24634  stdbdbl  24749  prdsxmslem2  24761  xrtgioo  25039  xrsxmet  25042  cnmpopc  25162  elpi1i  25280  minveclem7  25669  elovolmr  25710  ismbf  25862  mbfmax  25883  itg1val2  25918  mbfi1fseqlem4  25952  itgresr  26013  iblrelem  26025  iblpos  26027  rlimcnp  27210  rlimcnp2  27211  chpchtsum  27463  lgsneg  27565  lgsdilem  27568  2lgslem1a  27635  eqcuts2  28059  n0subs  28636  n0lts1e0  28641  zsoring  28682  bdaypw2n0bndlem  28736  lmiinv  29184  isspthonpth  30222  s3wwlks2on  30432  sps3wwlks2on  30433  clwlkclwwlk  30480  clwwlknonel  30573  clwwlknun  30590  eupth2lem2  30707  frgr3vlem2  30762  numclwwlk2lem1  30864  nrt2irr  30961  minvecolem7  31372  shle0  31931  mdsl2bi  32812  dmdbr5ati  32911  cdj3lem1  32923  rlocisunit  33724  qsfld  33908  eulerpartlemr  34893  subfacp1lem3  35769  satefvfmla1  36012  hfext  36771  bj-issetwt  37626  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  mblfinlem3  38416  mblfinlem4  38417  mbfresfi  38423  itg2addnclem  38428  itg2addnc  38431  heiborlem10  38578  relssinxpdmrn  39105  dffunsALTV2  39525  dffunsALTV3  39526  dffunsALTV4  39527  elfunsALTV2  39534  elfunsALTV3  39535  elfunsALTV4  39536  elfunsALTV5  39537  dfdisjs2  39550  dfdisjs5  39553  disjimdmqseq  39565  eldisjs2  39576  ople0  40068  atlle0  40186  cdlemg10c  41520  cdlemg33c  41589  hdmap14lem13  42761  mrefg3  43561  onsupneqmaxlim0  44073  onsupnmax  44077  radcnvrat  45146  2ffzoeq  48224