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  1613  raldifeq  4499  rexreusng  4683  posn  5773  dmxp  5941  elrnmpt1  5973  dfres3  6004  opelres  6005  ffrnbd  6751  fliftf  7334  eroveu  8850  ixpfi2  9387  elfi2  9451  dffi3  9468  cfss  10302  wunex2  10775  nnle1eq1  12293  nn0le0eq0  12551  ixxun  13399  ioopos  13460  injresinj  13823  hashle00  14435  prprrab  14508  xpcogend  15009  cnpart  15275  fz1f1o  15742  nndivdvds  16295  dvdsmultr2  16331  bitsmod  16469  sadadd  16500  sadass  16504  smuval2  16515  smumul  16526  pcmpt  16925  pcmpt2  16926  prmreclem2  16950  prmreclem5  16953  ramcl  17062  mrcidb2  17662  acsfn  17703  fncnvimaeqv  18174  latleeqj1  18508  resmndismnd  18833  pgpssslw  19646  subgdmdprd  20068  resrhm2b  20618  acsfn1p  20816  lssle0  20965  islpir2  21357  islinds3  21871  iscld4  23088  cncnpi  23301  cnprest2  23313  lmss  23321  isconn2  23437  dfconn2  23442  subislly  23504  lly1stc  23519  elptr  23596  txcn  23649  xkoinjcn  23710  tsmsres  24167  isxmet2d  24352  xmetgt0  24383  prdsxmetlem  24393  imasdsf1olem  24398  xblss2  24427  stdbdbl  24545  prdsxmslem2  24557  xrtgioo  24841  xrsxmet  24844  cnmpopc  24968  elpi1i  25092  minveclem7  25482  elovolmr  25524  ismbf  25676  mbfmax  25697  itg1val2  25732  mbfi1fseqlem4  25767  itgresr  25828  iblrelem  25840  iblpos  25842  rlimcnp  27022  rlimcnp2  27023  chpchtsum  27277  lgsneg  27379  lgsdilem  27382  2lgslem1a  27449  eqscut2  27865  n0subs  28374  lmiinv  28814  isspthonpth  29781  s3wwlks2on  29985  clwlkclwwlk  30030  clwwlknonel  30123  clwwlknun  30140  eupth2lem2  30247  frgr3vlem2  30302  numclwwlk2lem1  30404  nrt2irr  30501  minvecolem7  30911  shle0  31470  mdsl2bi  32351  dmdbr5ati  32450  cdj3lem1  32462  qsfld  33505  eulerpartlemr  34355  subfacp1lem3  35166  satefvfmla1  35409  hfext  36164  bj-issetwt  36857  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  mblfinlem3  37645  mblfinlem4  37646  mbfresfi  37652  itg2addnclem  37657  itg2addnc  37660  heiborlem10  37806  relssinxpdmrn  38330  dffunsALTV2  38665  dffunsALTV3  38666  dffunsALTV4  38667  elfunsALTV2  38674  elfunsALTV3  38675  elfunsALTV4  38676  elfunsALTV5  38677  dfdisjs2  38690  dfdisjs5  38693  eldisjs2  38704  ople0  39168  atlle0  39286  cdlemg10c  40621  cdlemg33c  40690  hdmap14lem13  41862  mrefg3  42695  onsupneqmaxlim0  43212  onsupnmax  43216  radcnvrat  44309  2ffzoeq  47276