Theorem biantrud 540

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ifptru  1089  cad1  1640  raldifeq  4450  rexreusng  4641  posn  5738  dmxp  5910  elrnmpt1  5941  dfres3  5974  opelres  5975  ffrnbd  6711  fliftf  7303  eroveu  8798  ixpfi2  9295  elfi2  9362  dffi3  9379  cfss  10237  wunex2  10711  nnle1eq1  12257  nn0le0eq0  12523  ixxun  13379  ioopos  13442  injresinj  13811  hashle00  14427  prprrab  14500  xpcogend  15001  cnpart  15281  fz1f1o  15751  nndivdvds  16309  dvdsmultr2  16346  bitsmod  16484  sadadd  16515  sadass  16519  smuval2  16530  smumul  16541  pcmpt  16942  pcmpt2  16943  prmreclem2  16967  prmreclem5  16970  ramcl  17079  mrcidb2  17664  acsfn  17705  fncnvimaeqv  18166  latleeqj1  18497  resmndismnd  18856  pgpssslw  19675  subgdmdprd  20097  resrhm2b  20678  acsfn1p  20871  lssle0  21040  islpir2  21458  islinds3  21944  iscld4  23183  cncnpi  23396  cnprest2  23408  lmss  23416  isconn2  23532  dfconn2  23537  subislly  23599  lly1stc  23614  elptr  23691  txcn  23744  xkoinjcn  23805  tsmsres  24262  isxmet2d  24445  xmetgt0  24476  prdsxmetlem  24486  imasdsf1olem  24491  xblss2  24520  stdbdbl  24635  prdsxmslem2  24647  xrtgioo  24925  xrsxmet  24928  cnmpopc  25048  elpi1i  25166  minveclem7  25555  elovolmr  25596  ismbf  25748  mbfmax  25769  itg1val2  25804  mbfi1fseqlem4  25838  itgresr  25899  iblrelem  25911  iblpos  25913  rlimcnp  27088  rlimcnp2  27089  chpchtsum  27341  lgsneg  27443  lgsdilem  27446  2lgslem1a  27513  eqcuts2  27937  n0subs  28514  n0lts1e0  28519  zsoring  28560  bdaypw2n0bndlem  28614  lmiinv  29044  isspthonpth  30007  s3wwlks2on  30214  sps3wwlks2on  30215  clwlkclwwlk  30262  clwwlknonel  30355  clwwlknun  30372  eupth2lem2  30479  frgr3vlem2  30534  numclwwlk2lem1  30636  nrt2irr  30733  minvecolem7  31144  shle0  31703  mdsl2bi  32584  dmdbr5ati  32683  cdj3lem1  32695  rlocisunit  33509  qsfld  33697  eulerpartlemr  34681  subfacp1lem3  35545  satefvfmla1  35788  hfext  36546  bj-issetwt  37372  poimirlem25  38156  poimirlem26  38157  poimirlem27  38158  mblfinlem3  38170  mblfinlem4  38171  mbfresfi  38177  itg2addnclem  38182  itg2addnc  38185  heiborlem10  38331  relssinxpdmrn  38860  dffunsALTV2  39280  dffunsALTV3  39281  dffunsALTV4  39282  elfunsALTV2  39289  elfunsALTV3  39290  elfunsALTV4  39291  elfunsALTV5  39292  dfdisjs2  39305  dfdisjs5  39308  disjimdmqseq  39320  eldisjs2  39331  ople0  39823  atlle0  39941  cdlemg10c  41275  cdlemg33c  41344  hdmap14lem13  42516  mrefg3  43301  onsupneqmaxlim0  43813  onsupnmax  43817  radcnvrat  44888  2ffzoeq  47920