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  4460  rexreusng  4646  posn  5727  dmxp  5895  elrnmpt1  5927  dfres3  5958  opelres  5959  ffrnbd  6706  fliftf  7293  eroveu  8788  ixpfi2  9308  elfi2  9372  dffi3  9389  cfss  10225  wunex2  10698  nnle1eq1  12223  nn0le0eq0  12477  ixxun  13329  ioopos  13392  injresinj  13756  hashle00  14372  prprrab  14445  xpcogend  14947  cnpart  15213  fz1f1o  15683  nndivdvds  16238  dvdsmultr2  16275  bitsmod  16413  sadadd  16444  sadass  16448  smuval2  16459  smumul  16470  pcmpt  16870  pcmpt2  16871  prmreclem2  16895  prmreclem5  16898  ramcl  17007  mrcidb2  17586  acsfn  17627  fncnvimaeqv  18088  latleeqj1  18417  resmndismnd  18742  pgpssslw  19551  subgdmdprd  19973  resrhm2b  20518  acsfn1p  20715  lssle0  20863  islpir2  21247  islinds3  21750  iscld4  22959  cncnpi  23172  cnprest2  23184  lmss  23192  isconn2  23308  dfconn2  23313  subislly  23375  lly1stc  23390  elptr  23467  txcn  23520  xkoinjcn  23581  tsmsres  24038  isxmet2d  24222  xmetgt0  24253  prdsxmetlem  24263  imasdsf1olem  24268  xblss2  24297  stdbdbl  24412  prdsxmslem2  24424  xrtgioo  24702  xrsxmet  24705  cnmpopc  24829  elpi1i  24953  minveclem7  25342  elovolmr  25384  ismbf  25536  mbfmax  25557  itg1val2  25592  mbfi1fseqlem4  25626  itgresr  25687  iblrelem  25699  iblpos  25701  rlimcnp  26882  rlimcnp2  26883  chpchtsum  27137  lgsneg  27239  lgsdilem  27242  2lgslem1a  27309  eqscut2  27725  n0subs  28260  lmiinv  28726  isspthonpth  29686  s3wwlks2on  29893  clwlkclwwlk  29938  clwwlknonel  30031  clwwlknun  30048  eupth2lem2  30155  frgr3vlem2  30210  numclwwlk2lem1  30312  nrt2irr  30409  minvecolem7  30819  shle0  31378  mdsl2bi  32259  dmdbr5ati  32358  cdj3lem1  32370  qsfld  33476  eulerpartlemr  34372  subfacp1lem3  35176  satefvfmla1  35419  hfext  36178  bj-issetwt  36870  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  mblfinlem3  37660  mblfinlem4  37661  mbfresfi  37667  itg2addnclem  37672  itg2addnc  37675  heiborlem10  37821  relssinxpdmrn  38338  dffunsALTV2  38683  dffunsALTV3  38684  dffunsALTV4  38685  elfunsALTV2  38692  elfunsALTV3  38693  elfunsALTV4  38694  elfunsALTV5  38695  dfdisjs2  38708  dfdisjs5  38711  eldisjs2  38722  ople0  39187  atlle0  39305  cdlemg10c  40640  cdlemg33c  40709  hdmap14lem13  41881  mrefg3  42703  onsupneqmaxlim0  43220  onsupnmax  43224  radcnvrat  44310  2ffzoeq  47332