Theorem biantrud 529

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  ifptru  1061  cad1  1704  raldifeq  4203  posn  5344  elrnmpt1  5529  dfres3  5556  fliftf  6729  eroveu  8011  ixpfi2  8431  funsnfsupp  8466  elfi2  8487  dffi3  8504  cfss  9299  wunex2  9772  nn2ge  11257  nnle1eq1  11260  nn0le0eq0  11533  ixxun  12404  ioopos  12463  injresinj  12803  hashle00  13400  prprrab  13467  xpcogend  13934  cnpart  14199  fz1f1o  14660  nndivdvds  15211  dvdsmultr2  15243  bitsmod  15380  sadadd  15411  sadass  15415  smuval2  15426  smumul  15437  pcmpt  15818  pcmpt2  15819  prmreclem2  15843  prmreclem5  15846  ramcl  15955  mrcidb2  16500  acsfn  16541  fncnvimaeqv  16981  latleeqj1  17284  pgpssslw  18249  subgdmdprd  18653  lssle0  19172  islpir2  19473  islinds3  20395  iscld4  21091  discld  21115  cncnpi  21304  cnprest2  21316  lmss  21324  isconn2  21439  dfconn2  21444  subislly  21506  lly1stc  21521  elptr  21598  txcn  21651  hauseqlcld  21671  xkoinjcn  21712  tsmsres  22168  isxmet2d  22353  xmetgt0  22384  prdsxmetlem  22394  imasdsf1olem  22399  xblss2  22428  stdbdbl  22543  prdsxmslem2  22555  xrtgioo  22830  xrsxmet  22833  cncffvrn  22922  cnmpt2pc  22948  elpi1i  23066  minveclem7  23426  elovolmr  23464  ismbf  23616  mbfmax  23635  itg1val2  23670  mbfi1fseqlem4  23704  itgresr  23764  iblrelem  23776  iblpos  23778  itgfsum  23812  rlimcnp  24912  rlimcnp2  24913  chpchtsum  25164  dchreq  25203  lgsneg  25266  lgsdilem  25269  lgsquadlem2  25326  2lgslem1a  25336  lmiinv  25904  isspthonpth  26876  s3wwlks2on  27098  clwlkclwwlk  27146  clwwlknonel  27263  clwwlknun  27282  clwwlknunOLD  27286  dfconngr1  27361  eupth2lem2  27392  frgr3vlem2  27449  numclwwlk2lem1  27558  numclwwlk2lem1OLD  27565  minvecolem7  28069  shle0  28631  mdsl2bi  29512  dmdbr5ati  29611  cdj3lem1  29623  eulerpartlemr  30766  subfacp1lem3  31492  hfext  32617  bj-issetwt  33181  poimirlem25  33765  poimirlem26  33766  poimirlem27  33767  mblfinlem3  33779  mblfinlem4  33780  mbfresfi  33787  itg2addnclem  33792  itg2addnc  33795  cover2  33839  heiborlem10  33950  opelresALTV  34373  ople0  34995  atlle0  35113  cdlemg10c  36447  cdlemg33c  36516  hdmap14lem13  37692  mrefg3  37791  acsfn1p  38289  radcnvrat  39033  funressnfv  41732  dfdfat2  41735  2ffzoeq  41866