Theorem biantrud 538

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

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

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 399

This theorem is referenced by:  ifptru  1083  cad1  1627  raldifeq  4437  rexreusng  4628  posn  5722  dmxp  5894  elrnmpt1  5925  dfres3  5959  opelres  5960  ffrnbd  6692  fliftf  7284  eroveu  8778  ixpfi2  9279  elfi2  9346  dffi3  9363  cfss  10208  wunex2  10682  nnle1eq1  12229  nn0le0eq0  12495  ixxun  13351  ioopos  13414  injresinj  13783  hashle00  14399  prprrab  14472  xpcogend  14973  cnpart  15239  fz1f1o  15709  nndivdvds  16267  dvdsmultr2  16304  bitsmod  16442  sadadd  16473  sadass  16477  smuval2  16488  smumul  16499  pcmpt  16900  pcmpt2  16901  prmreclem2  16925  prmreclem5  16928  ramcl  17037  mrcidb2  17622  acsfn  17663  fncnvimaeqv  18124  latleeqj1  18455  resmndismnd  18814  pgpssslw  19626  subgdmdprd  20048  resrhm2b  20620  acsfn1p  20817  lssle0  20986  islpir2  21369  islinds3  21855  iscld4  23094  cncnpi  23307  cnprest2  23319  lmss  23327  isconn2  23443  dfconn2  23448  subislly  23510  lly1stc  23525  elptr  23602  txcn  23655  xkoinjcn  23716  tsmsres  24173  isxmet2d  24356  xmetgt0  24387  prdsxmetlem  24397  imasdsf1olem  24402  xblss2  24431  stdbdbl  24546  prdsxmslem2  24558  xrtgioo  24836  xrsxmet  24839  cnmpopc  24959  elpi1i  25077  minveclem7  25466  elovolmr  25507  ismbf  25659  mbfmax  25680  itg1val2  25715  mbfi1fseqlem4  25749  itgresr  25810  iblrelem  25822  iblpos  25824  rlimcnp  26996  rlimcnp2  26997  chpchtsum  27249  lgsneg  27351  lgsdilem  27354  2lgslem1a  27421  eqcuts2  27845  n0subs  28422  n0lts1e0  28427  zsoring  28468  bdaypw2n0bndlem  28522  lmiinv  28927  isspthonpth  29884  s3wwlks2on  30091  sps3wwlks2on  30092  clwlkclwwlk  30139  clwwlknonel  30232  clwwlknun  30249  eupth2lem2  30356  frgr3vlem2  30411  numclwwlk2lem1  30513  nrt2irr  30610  minvecolem7  31021  shle0  31580  mdsl2bi  32461  dmdbr5ati  32560  cdj3lem1  32572  qsfld  33630  eulerpartlemr  34615  subfacp1lem3  35470  satefvfmla1  35713  hfext  36471  bj-issetwt  37298  poimirlem25  38082  poimirlem26  38083  poimirlem27  38084  mblfinlem3  38096  mblfinlem4  38097  mbfresfi  38103  itg2addnclem  38108  itg2addnc  38111  heiborlem10  38257  relssinxpdmrn  38786  dffunsALTV2  39206  dffunsALTV3  39207  dffunsALTV4  39208  elfunsALTV2  39215  elfunsALTV3  39216  elfunsALTV4  39217  elfunsALTV5  39218  dfdisjs2  39231  dfdisjs5  39234  disjimdmqseq  39246  eldisjs2  39257  ople0  39749  atlle0  39867  cdlemg10c  41201  cdlemg33c  41270  hdmap14lem13  42442  mrefg3  43227  onsupneqmaxlim0  43739  onsupnmax  43743  radcnvrat  44828  2ffzoeq  47860