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  1075  cad1  1619  raldifeq  4433  rexreusng  4623  posn  5717  dmxp  5884  elrnmpt1  5915  dfres3  5949  opelres  5950  ffrnbd  6683  fliftf  7270  eroveu  8759  ixpfi2  9260  elfi2  9327  dffi3  9344  cfss  10187  wunex2  10661  nnle1eq1  12207  nn0le0eq0  12465  ixxun  13314  ioopos  13377  injresinj  13746  hashle00  14362  prprrab  14435  xpcogend  14936  cnpart  15202  fz1f1o  15672  nndivdvds  16230  dvdsmultr2  16267  bitsmod  16405  sadadd  16436  sadass  16440  smuval2  16451  smumul  16462  pcmpt  16863  pcmpt2  16864  prmreclem2  16888  prmreclem5  16891  ramcl  17000  mrcidb2  17584  acsfn  17625  fncnvimaeqv  18086  latleeqj1  18417  resmndismnd  18776  pgpssslw  19589  subgdmdprd  20011  resrhm2b  20579  acsfn1p  20776  lssle0  20945  islpir2  21328  islinds3  21814  iscld4  23030  cncnpi  23243  cnprest2  23255  lmss  23263  isconn2  23379  dfconn2  23384  subislly  23446  lly1stc  23461  elptr  23538  txcn  23591  xkoinjcn  23652  tsmsres  24109  isxmet2d  24292  xmetgt0  24323  prdsxmetlem  24333  imasdsf1olem  24338  xblss2  24367  stdbdbl  24482  prdsxmslem2  24494  xrtgioo  24772  xrsxmet  24775  cnmpopc  24895  elpi1i  25013  minveclem7  25402  elovolmr  25443  ismbf  25595  mbfmax  25616  itg1val2  25651  mbfi1fseqlem4  25685  itgresr  25746  iblrelem  25758  iblpos  25760  rlimcnp  26929  rlimcnp2  26930  chpchtsum  27182  lgsneg  27284  lgsdilem  27287  2lgslem1a  27354  eqcuts2  27778  n0subs  28355  n0lts1e0  28360  zsoring  28401  bdaypw2n0bndlem  28455  lmiinv  28860  isspthonpth  29817  s3wwlks2on  30024  sps3wwlks2on  30025  clwlkclwwlk  30072  clwwlknonel  30165  clwwlknun  30182  eupth2lem2  30289  frgr3vlem2  30344  numclwwlk2lem1  30446  nrt2irr  30543  minvecolem7  30954  shle0  31513  mdsl2bi  32394  dmdbr5ati  32493  cdj3lem1  32505  qsfld  33558  eulerpartlemr  34518  subfacp1lem3  35364  satefvfmla1  35607  hfext  36365  bj-issetwt  37182  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  mblfinlem3  37980  mblfinlem4  37981  mbfresfi  37987  itg2addnclem  37992  itg2addnc  37995  heiborlem10  38141  relssinxpdmrn  38670  dffunsALTV2  39090  dffunsALTV3  39091  dffunsALTV4  39092  elfunsALTV2  39099  elfunsALTV3  39100  elfunsALTV4  39101  elfunsALTV5  39102  dfdisjs2  39115  dfdisjs5  39118  disjimdmqseq  39130  eldisjs2  39141  ople0  39633  atlle0  39751  cdlemg10c  41085  cdlemg33c  41154  hdmap14lem13  42326  mrefg3  43140  onsupneqmaxlim0  43652  onsupnmax  43656  radcnvrat  44741  2ffzoeq  47776