Theorem biantrud 531

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  ifptru  1073  cad1  1617  raldifeq  4494  rexreusng  4684  posn  5762  elrnmpt1  5958  dfres3  5987  opelres  5988  ffrnbd  6734  fliftf  7315  eroveu  8809  ixpfi2  9353  elfi2  9412  dffi3  9429  cfss  10263  wunex2  10736  nnle1eq1  12247  nn0le0eq0  12505  ixxun  13345  ioopos  13406  injresinj  13758  hashle00  14365  prprrab  14439  xpcogend  14926  cnpart  15192  fz1f1o  15661  nndivdvds  16211  dvdsmultr2  16246  bitsmod  16382  sadadd  16413  sadass  16417  smuval2  16428  smumul  16439  pcmpt  16830  pcmpt2  16831  prmreclem2  16855  prmreclem5  16858  ramcl  16967  mrcidb2  17567  acsfn  17608  fncnvimaeqv  18076  latleeqj1  18409  resmndismnd  18726  pgpssslw  19524  subgdmdprd  19946  resrhm2b  20493  acsfn1p  20559  lssle0  20705  islpir2  21090  islinds3  21609  iscld4  22790  cncnpi  23003  cnprest2  23015  lmss  23023  isconn2  23139  dfconn2  23144  subislly  23206  lly1stc  23221  elptr  23298  txcn  23351  xkoinjcn  23412  tsmsres  23869  isxmet2d  24054  xmetgt0  24085  prdsxmetlem  24095  imasdsf1olem  24100  xblss2  24129  stdbdbl  24247  prdsxmslem2  24259  xrtgioo  24543  xrsxmet  24546  cnmpopc  24670  elpi1i  24794  minveclem7  25184  elovolmr  25226  ismbf  25378  mbfmax  25399  itg1val2  25434  mbfi1fseqlem4  25469  itgresr  25529  iblrelem  25541  iblpos  25543  rlimcnp  26703  rlimcnp2  26704  chpchtsum  26955  lgsneg  27057  lgsdilem  27060  2lgslem1a  27127  eqscut2  27541  lmiinv  28307  isspthonpth  29270  s3wwlks2on  29474  clwlkclwwlk  29519  clwwlknonel  29612  clwwlknun  29629  eupth2lem2  29736  frgr3vlem2  29791  numclwwlk2lem1  29893  nrt2irr  29990  minvecolem7  30400  shle0  30959  mdsl2bi  31840  dmdbr5ati  31939  cdj3lem1  31951  qsfld  32883  eulerpartlemr  33668  subfacp1lem3  34468  satefvfmla1  34711  hfext  35456  bj-issetwt  36058  poimirlem25  36817  poimirlem26  36818  poimirlem27  36819  mblfinlem3  36831  mblfinlem4  36832  mbfresfi  36838  itg2addnclem  36843  itg2addnc  36846  heiborlem10  36992  relssinxpdmrn  37522  dffunsALTV2  37858  dffunsALTV3  37859  dffunsALTV4  37860  elfunsALTV2  37867  elfunsALTV3  37868  elfunsALTV4  37869  elfunsALTV5  37870  dfdisjs2  37883  dfdisjs5  37886  eldisjs2  37897  ople0  38361  atlle0  38479  cdlemg10c  39814  cdlemg33c  39883  hdmap14lem13  41055  mrefg3  41749  onsupneqmaxlim0  42276  onsupnmax  42280  radcnvrat  43376  2ffzoeq  46336