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  1618  raldifeq  4446  rexreusng  4636  posn  5710  dmxp  5878  elrnmpt1  5909  dfres3  5943  opelres  5944  ffrnbd  6677  fliftf  7261  eroveu  8749  ixpfi2  9250  elfi2  9317  dffi3  9334  cfss  10175  wunex2  10649  nnle1eq1  12175  nn0le0eq0  12429  ixxun  13277  ioopos  13340  injresinj  13707  hashle00  14323  prprrab  14396  xpcogend  14897  cnpart  15163  fz1f1o  15633  nndivdvds  16188  dvdsmultr2  16225  bitsmod  16363  sadadd  16394  sadass  16398  smuval2  16409  smumul  16420  pcmpt  16820  pcmpt2  16821  prmreclem2  16845  prmreclem5  16848  ramcl  16957  mrcidb2  17541  acsfn  17582  fncnvimaeqv  18043  latleeqj1  18374  resmndismnd  18733  pgpssslw  19543  subgdmdprd  19965  resrhm2b  20535  acsfn1p  20732  lssle0  20901  islpir2  21285  islinds3  21789  iscld4  23009  cncnpi  23222  cnprest2  23234  lmss  23242  isconn2  23358  dfconn2  23363  subislly  23425  lly1stc  23440  elptr  23517  txcn  23570  xkoinjcn  23631  tsmsres  24088  isxmet2d  24271  xmetgt0  24302  prdsxmetlem  24312  imasdsf1olem  24317  xblss2  24346  stdbdbl  24461  prdsxmslem2  24473  xrtgioo  24751  xrsxmet  24754  cnmpopc  24878  elpi1i  25002  minveclem7  25391  elovolmr  25433  ismbf  25585  mbfmax  25606  itg1val2  25641  mbfi1fseqlem4  25675  itgresr  25736  iblrelem  25748  iblpos  25750  rlimcnp  26931  rlimcnp2  26932  chpchtsum  27186  lgsneg  27288  lgsdilem  27291  2lgslem1a  27358  eqcuts2  27782  n0subs  28359  n0lts1e0  28364  zsoring  28405  bdaypw2n0bndlem  28459  lmiinv  28864  isspthonpth  29822  s3wwlks2on  30029  sps3wwlks2on  30030  clwlkclwwlk  30077  clwwlknonel  30170  clwwlknun  30187  eupth2lem2  30294  frgr3vlem2  30349  numclwwlk2lem1  30451  nrt2irr  30548  minvecolem7  30958  shle0  31517  mdsl2bi  32398  dmdbr5ati  32497  cdj3lem1  32509  qsfld  33579  eulerpartlemr  34531  subfacp1lem3  35376  satefvfmla1  35619  hfext  36377  bj-issetwt  37076  poimirlem25  37842  poimirlem26  37843  poimirlem27  37844  mblfinlem3  37856  mblfinlem4  37857  mbfresfi  37863  itg2addnclem  37868  itg2addnc  37871  heiborlem10  38017  relssinxpdmrn  38538  dffunsALTV2  38939  dffunsALTV3  38940  dffunsALTV4  38941  elfunsALTV2  38948  elfunsALTV3  38949  elfunsALTV4  38950  elfunsALTV5  38951  dfdisjs2  38964  dfdisjs5  38967  eldisjs2  38978  ople0  39443  atlle0  39561  cdlemg10c  40895  cdlemg33c  40964  hdmap14lem13  42136  mrefg3  42946  onsupneqmaxlim0  43462  onsupnmax  43466  radcnvrat  44551  2ffzoeq  47569