Theorem biantrud 539

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ifptru  1085  cad1  1636  raldifeq  4446  rexreusng  4637  posn  5731  dmxp  5903  elrnmpt1  5934  dfres3  5968  opelres  5969  ffrnbd  6703  fliftf  7295  eroveu  8789  ixpfi2  9290  elfi2  9357  dffi3  9374  cfss  10219  wunex2  10693  nnle1eq1  12240  nn0le0eq0  12506  ixxun  13362  ioopos  13425  injresinj  13794  hashle00  14410  prprrab  14483  xpcogend  14984  cnpart  15250  fz1f1o  15720  nndivdvds  16278  dvdsmultr2  16315  bitsmod  16453  sadadd  16484  sadass  16488  smuval2  16499  smumul  16510  pcmpt  16911  pcmpt2  16912  prmreclem2  16936  prmreclem5  16939  ramcl  17048  mrcidb2  17633  acsfn  17674  fncnvimaeqv  18135  latleeqj1  18466  resmndismnd  18825  pgpssslw  19637  subgdmdprd  20059  resrhm2b  20631  acsfn1p  20828  lssle0  20997  islpir2  21380  islinds3  21866  iscld4  23105  cncnpi  23318  cnprest2  23330  lmss  23338  isconn2  23454  dfconn2  23459  subislly  23521  lly1stc  23536  elptr  23613  txcn  23666  xkoinjcn  23727  tsmsres  24184  isxmet2d  24367  xmetgt0  24398  prdsxmetlem  24408  imasdsf1olem  24413  xblss2  24442  stdbdbl  24557  prdsxmslem2  24569  xrtgioo  24847  xrsxmet  24850  cnmpopc  24970  elpi1i  25088  minveclem7  25477  elovolmr  25518  ismbf  25670  mbfmax  25691  itg1val2  25726  mbfi1fseqlem4  25760  itgresr  25821  iblrelem  25833  iblpos  25835  rlimcnp  27007  rlimcnp2  27008  chpchtsum  27260  lgsneg  27362  lgsdilem  27365  2lgslem1a  27432  eqcuts2  27856  n0subs  28433  n0lts1e0  28438  zsoring  28479  bdaypw2n0bndlem  28533  lmiinv  28938  isspthonpth  29895  s3wwlks2on  30102  sps3wwlks2on  30103  clwlkclwwlk  30150  clwwlknonel  30243  clwwlknun  30260  eupth2lem2  30367  frgr3vlem2  30422  numclwwlk2lem1  30524  nrt2irr  30621  minvecolem7  31032  shle0  31591  mdsl2bi  32472  dmdbr5ati  32571  cdj3lem1  32583  rlocisunit  33418  qsfld  33647  eulerpartlemr  34632  subfacp1lem3  35496  satefvfmla1  35739  hfext  36497  bj-issetwt  37324  poimirlem25  38108  poimirlem26  38109  poimirlem27  38110  mblfinlem3  38122  mblfinlem4  38123  mbfresfi  38129  itg2addnclem  38134  itg2addnc  38137  heiborlem10  38283  relssinxpdmrn  38812  dffunsALTV2  39232  dffunsALTV3  39233  dffunsALTV4  39234  elfunsALTV2  39241  elfunsALTV3  39242  elfunsALTV4  39243  elfunsALTV5  39244  dfdisjs2  39257  dfdisjs5  39260  disjimdmqseq  39272  eldisjs2  39283  ople0  39775  atlle0  39893  cdlemg10c  41227  cdlemg33c  41296  hdmap14lem13  42468  mrefg3  43253  onsupneqmaxlim0  43765  onsupnmax  43769  radcnvrat  44854  2ffzoeq  47886