Theorem biantrud 541

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ifptru  1091  cad1  1650  nrmod  3839  raldifeq  4449  rexreusng  4640  posn  5737  dmxp  5911  elrnmpt1  5942  dfres3  5975  opelres  5976  ffrnbd  6717  fliftf  7315  eroveu  8817  ixpfi2  9323  elfi2  9390  dffi3  9407  cfss  10324  wunex2  10804  nnle1eq1  12349  nn0le0eq0  12615  ixxun  13473  ioopos  13536  injresinj  13906  hashle00  14524  prprrab  14598  xpcogend  15107  cnpart  15387  fz1f1o  15856  nndivdvds  16411  dvdsmultr2  16448  bitsmod  16586  sadadd  16617  sadass  16621  smuval2  16632  smumul  16643  pcmpt  17050  pcmpt2  17051  prmreclem2  17075  prmreclem5  17078  ramcl  17187  mrcidb2  17772  acsfn  17813  fncnvimaeqv  18274  latleeqj1  18605  resmndismnd  18983  pgpssslw  19808  subgdmdprd  20230  resrhm2b  20834  acsfn1p  21036  lssle0  21205  islpir2  21634  islinds3  22120  iscld4  23363  cncnpi  23576  cnprest2  23588  lmss  23596  isconn2  23712  dfconn2  23717  subislly  23780  lly1stc  23795  elptr  23872  txcn  23925  xkoinjcn  23986  tsmsres  24443  isxmet2d  24626  xmetgt0  24657  prdsxmetlem  24667  imasdsf1olem  24672  xblss2  24701  stdbdbl  24816  prdsxmslem2  24828  xrtgioo  25106  xrsxmet  25109  cnmpopc  25229  elpi1i  25347  minveclem7  25736  elovolmr  25777  ismbf  25929  mbfmax  25950  itg1val2  25985  mbfi1fseqlem4  26019  itgresr  26079  iblrelem  26091  iblpos  26093  rlimcnp  27275  rlimcnp2  27276  chpchtsum  27528  lgsneg  27630  lgsdilem  27633  2lgslem1a  27700  eqcuts2  28154  n0subs  28731  n0lts1e0  28736  zsoring  28777  bdaypw2n0bndlem  28831  lmiinv  29279  isspthonpth  30317  s3wwlks2on  30527  sps3wwlks2on  30528  clwlkclwwlk  30575  clwwlknonel  30668  clwwlknun  30685  eupth2lem2  30802  frgr3vlem2  30857  numclwwlk2lem1  30959  nrt2irr  31056  minvecolem7  31467  shle0  32026  mdsl2bi  32907  dmdbr5ati  33006  cdj3lem1  33018  rlocisunit  33819  qsfld  34004  eulerpartlemr  34989  subfacp1lem3  35916  satefvfmla1  36159  hfext  36904  bj-issetwt  37757  poimirlem25  38531  poimirlem26  38532  poimirlem27  38533  mblfinlem3  38545  mblfinlem4  38546  mbfresfi  38552  itg2addnclem  38557  itg2addnc  38560  heiborlem10  38722  relssinxpdmrn  39249  dffunsALTV2  39669  dffunsALTV3  39670  dffunsALTV4  39671  elfunsALTV2  39678  elfunsALTV3  39679  elfunsALTV4  39680  elfunsALTV5  39681  dfdisjs2  39694  dfdisjs5  39697  disjimdmqseq  39709  eldisjs2  39720  ople0  40212  atlle0  40330  cdlemg10c  41664  cdlemg33c  41733  hdmap14lem13  42905  mrefg3  43672  onsupneqmaxlim0  44184  onsupnmax  44188  radcnvrat  45257  2ffzoeq  48342