Theorem biantrud 526

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

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  ifptru  1016  cad1  1545  raldifeq  4010  posn  5100  elrnmpt1  5282  fliftf  6443  eroveu  7707  ixpfi2  8125  funsnfsupp  8160  elfi2  8181  dffi3  8198  cfss  8948  wunex2  9417  nn2ge  10895  nnle1eq1  10898  nn0le0eq0  11171  ixxun  12021  ioopos  12080  injresinj  12409  xpcogend  13510  cnpart  13777  fz1f1o  14237  nndivdvds  14776  dvdsmultr2  14808  bitsmod  14945  sadadd  14976  sadass  14980  smuval2  14991  smumul  15002  pcmpt  15383  pcmpt2  15384  prmreclem2  15408  prmreclem5  15411  ramcl  15520  mrcidb2  16050  acsfn  16092  fncnvimaeqv  16532  latleeqj1  16835  pgpssslw  17801  subgdmdprd  18205  lssle0  18720  islpir2  19021  islinds3  19940  iscld4  20627  discld  20651  cncnpi  20840  cnprest2  20852  lmss  20860  iscon2  20975  dfcon2  20980  subislly  21042  lly1stc  21057  elptr  21134  txcn  21187  hauseqlcld  21207  xkoinjcn  21248  tsmsres  21705  isxmet2d  21890  xmetgt0  21921  prdsxmetlem  21931  imasdsf1olem  21936  xblss2  21965  stdbdbl  22080  prdsxmslem2  22092  xrtgioo  22365  xrsxmet  22368  cncffvrn  22457  cnmpt2pc  22483  elpi1i  22602  minveclem7  22959  elovolmr  22996  ismbf  23148  mbfmax  23167  itg1val2  23202  mbfi1fseqlem4  23236  itgresr  23296  iblrelem  23308  iblpos  23310  itgfsum  23344  rlimcnp  24437  rlimcnp2  24438  chpchtsum  24689  dchreq  24728  lgsneg  24791  lgsdilem  24794  lgsquadlem2  24851  2lgslem1a  24861  lmiinv  25430  isusgra0  25670  usgraop  25673  dfconngra1  25993  eupath2lem2  26299  frgra3vlem2  26322  numclwwlk2lem1  26423  minvecolem7  26957  shle0  27519  mdsl2bi  28400  dmdbr5ati  28499  cdj3lem1  28511  eulerpartlemr  29597  subfacp1lem3  30252  dfres3  30736  hfext  31294  bj-issetwt  31877  poimirlem25  32428  poimirlem26  32429  poimirlem27  32430  mblfinlem3  32442  mblfinlem4  32443  mbfresfi  32450  itg2addnclem  32455  itg2addnc  32458  cover2  32502  heiborlem10  32613  ople0  33316  atlle0  33434  cdlemg10c  34769  cdlemg33c  34838  hdmap14lem13  36014  mrefg3  36113  acsfn1p  36612  radcnvrat  37359  funressnfv  39681  dfdfat2  39685  2ffzoeq  40208  prprrab  40217  isspthonpth-av  40977  s3wwlks2on  41182  clwlkclwwlk  41233  clwwlksnun  41303  dfconngr1  41377  eupth2lem2  41409  frgr3vlem2  41466  av-numclwwlk2lem1  41554