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  4434  rexreusng  4624  posn  5710  dmxp  5878  elrnmpt1  5909  dfres3  5943  opelres  5944  ffrnbd  6677  fliftf  7263  eroveu  8752  ixpfi2  9253  elfi2  9320  dffi3  9337  cfss  10178  wunex2  10652  nnle1eq1  12198  nn0le0eq0  12456  ixxun  13305  ioopos  13368  injresinj  13737  hashle00  14353  prprrab  14426  xpcogend  14927  cnpart  15193  fz1f1o  15663  nndivdvds  16221  dvdsmultr2  16258  bitsmod  16396  sadadd  16427  sadass  16431  smuval2  16442  smumul  16453  pcmpt  16854  pcmpt2  16855  prmreclem2  16879  prmreclem5  16882  ramcl  16991  mrcidb2  17575  acsfn  17616  fncnvimaeqv  18077  latleeqj1  18408  resmndismnd  18767  pgpssslw  19580  subgdmdprd  20002  resrhm2b  20570  acsfn1p  20767  lssle0  20936  islpir2  21320  islinds3  21824  iscld4  23040  cncnpi  23253  cnprest2  23265  lmss  23273  isconn2  23389  dfconn2  23394  subislly  23456  lly1stc  23471  elptr  23548  txcn  23601  xkoinjcn  23662  tsmsres  24119  isxmet2d  24302  xmetgt0  24333  prdsxmetlem  24343  imasdsf1olem  24348  xblss2  24377  stdbdbl  24492  prdsxmslem2  24504  xrtgioo  24782  xrsxmet  24785  cnmpopc  24905  elpi1i  25023  minveclem7  25412  elovolmr  25453  ismbf  25605  mbfmax  25626  itg1val2  25661  mbfi1fseqlem4  25695  itgresr  25756  iblrelem  25768  iblpos  25770  rlimcnp  26942  rlimcnp2  26943  chpchtsum  27196  lgsneg  27298  lgsdilem  27301  2lgslem1a  27368  eqcuts2  27792  n0subs  28369  n0lts1e0  28374  zsoring  28415  bdaypw2n0bndlem  28469  lmiinv  28874  isspthonpth  29832  s3wwlks2on  30039  sps3wwlks2on  30040  clwlkclwwlk  30087  clwwlknonel  30180  clwwlknun  30197  eupth2lem2  30304  frgr3vlem2  30359  numclwwlk2lem1  30461  nrt2irr  30558  minvecolem7  30969  shle0  31528  mdsl2bi  32409  dmdbr5ati  32508  cdj3lem1  32520  qsfld  33573  eulerpartlemr  34534  subfacp1lem3  35380  satefvfmla1  35623  hfext  36381  bj-issetwt  37198  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  mblfinlem3  37994  mblfinlem4  37995  mbfresfi  38001  itg2addnclem  38006  itg2addnc  38009  heiborlem10  38155  relssinxpdmrn  38684  dffunsALTV2  39104  dffunsALTV3  39105  dffunsALTV4  39106  elfunsALTV2  39113  elfunsALTV3  39114  elfunsALTV4  39115  elfunsALTV5  39116  dfdisjs2  39129  dfdisjs5  39132  disjimdmqseq  39144  eldisjs2  39155  ople0  39647  atlle0  39765  cdlemg10c  41099  cdlemg33c  41168  hdmap14lem13  42340  mrefg3  43154  onsupneqmaxlim0  43670  onsupnmax  43674  radcnvrat  44759  2ffzoeq  47788