Theorem biantrud 527

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ifptru  1017  cad1  1546  raldifeq  4011  posn  5110  elrnmpt1  5295  fliftf  6465  eroveu  7729  ixpfi2  8147  funsnfsupp  8182  elfi2  8203  dffi3  8220  cfss  8970  wunex2  9439  nn2ge  10922  nnle1eq1  10925  nn0le0eq0  11198  ixxun  12062  ioopos  12121  injresinj  12451  hashle00  13049  prprrab  13112  xpcogend  13561  cnpart  13828  fz1f1o  14288  nndivdvds  14827  dvdsmultr2  14859  bitsmod  14996  sadadd  15027  sadass  15031  smuval2  15042  smumul  15053  pcmpt  15434  pcmpt2  15435  prmreclem2  15459  prmreclem5  15462  ramcl  15571  mrcidb2  16101  acsfn  16143  fncnvimaeqv  16583  latleeqj1  16886  pgpssslw  17852  subgdmdprd  18256  lssle0  18771  islpir2  19072  islinds3  19992  iscld4  20679  discld  20703  cncnpi  20892  cnprest2  20904  lmss  20912  iscon2  21027  dfcon2  21032  subislly  21094  lly1stc  21109  elptr  21186  txcn  21239  hauseqlcld  21259  xkoinjcn  21300  tsmsres  21757  isxmet2d  21942  xmetgt0  21973  prdsxmetlem  21983  imasdsf1olem  21988  xblss2  22017  stdbdbl  22132  prdsxmslem2  22144  xrtgioo  22417  xrsxmet  22420  cncffvrn  22509  cnmpt2pc  22535  elpi1i  22654  minveclem7  23014  elovolmr  23051  ismbf  23203  mbfmax  23222  itg1val2  23257  mbfi1fseqlem4  23291  itgresr  23351  iblrelem  23363  iblpos  23365  itgfsum  23399  rlimcnp  24492  rlimcnp2  24493  chpchtsum  24744  dchreq  24783  lgsneg  24846  lgsdilem  24849  lgsquadlem2  24906  2lgslem1a  24916  lmiinv  25484  isusgra0  25876  usgraop  25879  dfconngra1  26199  eupath2lem2  26505  frgra3vlem2  26528  numclwwlk2lem1  26629  minvecolem7  27123  shle0  27685  mdsl2bi  28566  dmdbr5ati  28665  cdj3lem1  28677  eulerpartlemr  29763  subfacp1lem3  30418  dfres3  30902  hfext  31460  bj-issetwt  32053  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  mblfinlem3  32618  mblfinlem4  32619  mbfresfi  32626  itg2addnclem  32631  itg2addnc  32634  cover2  32678  heiborlem10  32789  ople0  33492  atlle0  33610  cdlemg10c  34945  cdlemg33c  35014  hdmap14lem13  36190  mrefg3  36289  acsfn1p  36788  radcnvrat  37535  funressnfv  39857  dfdfat2  39860  2ffzoeq  40361  isspthonpth-av  40955  s3wwlks2on  41160  clwlkclwwlk  41211  clwwlksnun  41281  dfconngr1  41355  eupth2lem2  41387  frgr3vlem2  41444  av-numclwwlk2lem1  41532