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

This theorem is referenced by:  ifptru  1074  cad1  1617  raldifeq  4469  rexreusng  4655  posn  5740  dmxp  5908  elrnmpt1  5940  dfres3  5971  opelres  5972  ffrnbd  6720  fliftf  7307  eroveu  8824  ixpfi2  9360  elfi2  9424  dffi3  9441  cfss  10277  wunex2  10750  nnle1eq1  12268  nn0le0eq0  12527  ixxun  13376  ioopos  13439  injresinj  13802  hashle00  14416  prprrab  14489  xpcogend  14991  cnpart  15257  fz1f1o  15724  nndivdvds  16279  dvdsmultr2  16315  bitsmod  16453  sadadd  16484  sadass  16488  smuval2  16499  smumul  16510  pcmpt  16910  pcmpt2  16911  prmreclem2  16935  prmreclem5  16938  ramcl  17047  mrcidb2  17628  acsfn  17669  fncnvimaeqv  18130  latleeqj1  18459  resmndismnd  18784  pgpssslw  19593  subgdmdprd  20015  resrhm2b  20560  acsfn1p  20757  lssle0  20905  islpir2  21289  islinds3  21792  iscld4  23001  cncnpi  23214  cnprest2  23226  lmss  23234  isconn2  23350  dfconn2  23355  subislly  23417  lly1stc  23432  elptr  23509  txcn  23562  xkoinjcn  23623  tsmsres  24080  isxmet2d  24264  xmetgt0  24295  prdsxmetlem  24305  imasdsf1olem  24310  xblss2  24339  stdbdbl  24454  prdsxmslem2  24466  xrtgioo  24744  xrsxmet  24747  cnmpopc  24871  elpi1i  24995  minveclem7  25385  elovolmr  25427  ismbf  25579  mbfmax  25600  itg1val2  25635  mbfi1fseqlem4  25669  itgresr  25730  iblrelem  25742  iblpos  25744  rlimcnp  26925  rlimcnp2  26926  chpchtsum  27180  lgsneg  27282  lgsdilem  27285  2lgslem1a  27352  eqscut2  27768  n0subs  28277  lmiinv  28717  isspthonpth  29677  s3wwlks2on  29884  clwlkclwwlk  29929  clwwlknonel  30022  clwwlknun  30039  eupth2lem2  30146  frgr3vlem2  30201  numclwwlk2lem1  30303  nrt2irr  30400  minvecolem7  30810  shle0  31369  mdsl2bi  32250  dmdbr5ati  32349  cdj3lem1  32361  qsfld  33459  eulerpartlemr  34352  subfacp1lem3  35150  satefvfmla1  35393  hfext  36147  bj-issetwt  36839  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  mblfinlem3  37629  mblfinlem4  37630  mbfresfi  37636  itg2addnclem  37641  itg2addnc  37644  heiborlem10  37790  relssinxpdmrn  38313  dffunsALTV2  38648  dffunsALTV3  38649  dffunsALTV4  38650  elfunsALTV2  38657  elfunsALTV3  38658  elfunsALTV4  38659  elfunsALTV5  38660  dfdisjs2  38673  dfdisjs5  38676  eldisjs2  38687  ople0  39151  atlle0  39269  cdlemg10c  40604  cdlemg33c  40673  hdmap14lem13  41845  mrefg3  42678  onsupneqmaxlim0  43195  onsupnmax  43199  radcnvrat  44286  2ffzoeq  47304