Theorem biantrud 527

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 523	. 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  1043  cad1  1595  raldifeq  4092  posn  5221  elrnmpt1  5406  dfres3  5433  fliftf  6605  eroveu  7885  ixpfi2  8305  funsnfsupp  8340  elfi2  8361  dffi3  8378  cfss  9125  wunex2  9598  nn2ge  11083  nnle1eq1  11086  nn0le0eq0  11359  ixxun  12229  ioopos  12288  injresinj  12629  hashle00  13226  prprrab  13293  xpcogend  13759  cnpart  14024  fz1f1o  14485  nndivdvds  15036  dvdsmultr2  15068  bitsmod  15205  sadadd  15236  sadass  15240  smuval2  15251  smumul  15262  pcmpt  15643  pcmpt2  15644  prmreclem2  15668  prmreclem5  15671  ramcl  15780  mrcidb2  16325  acsfn  16367  fncnvimaeqv  16807  latleeqj1  17110  pgpssslw  18075  subgdmdprd  18479  lssle0  18998  islpir2  19299  islinds3  20221  iscld4  20917  discld  20941  cncnpi  21130  cnprest2  21142  lmss  21150  isconn2  21265  dfconn2  21270  subislly  21332  lly1stc  21347  elptr  21424  txcn  21477  hauseqlcld  21497  xkoinjcn  21538  tsmsres  21994  isxmet2d  22179  xmetgt0  22210  prdsxmetlem  22220  imasdsf1olem  22225  xblss2  22254  stdbdbl  22369  prdsxmslem2  22381  xrtgioo  22656  xrsxmet  22659  cncffvrn  22748  cnmpt2pc  22774  elpi1i  22892  minveclem7  23252  elovolmr  23290  ismbf  23442  mbfmax  23461  itg1val2  23496  mbfi1fseqlem4  23530  itgresr  23590  iblrelem  23602  iblpos  23604  itgfsum  23638  rlimcnp  24737  rlimcnp2  24738  chpchtsum  24989  dchreq  25028  lgsneg  25091  lgsdilem  25094  lgsquadlem2  25151  2lgslem1a  25161  lmiinv  25729  isspthonpth  26701  s3wwlks2on  26922  clwlkclwwlk  26968  clwwlknonel  27070  clwwlknun  27087  clwwlknunOLD  27091  dfconngr1  27166  eupth2lem2  27197  frgr3vlem2  27254  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  minvecolem7  27867  shle0  28429  mdsl2bi  29310  dmdbr5ati  29409  cdj3lem1  29421  eulerpartlemr  30564  subfacp1lem3  31290  hfext  32415  bj-issetwt  32984  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  mblfinlem3  33578  mblfinlem4  33579  mbfresfi  33586  itg2addnclem  33591  itg2addnc  33594  cover2  33638  heiborlem10  33749  opelresALTV  34172  ople0  34792  atlle0  34910  cdlemg10c  36244  cdlemg33c  36313  hdmap14lem13  37489  mrefg3  37588  acsfn1p  38086  radcnvrat  38830  funressnfv  41529  dfdfat2  41532  2ffzoeq  41663