Theorem biantrud 535

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

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

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 400

This theorem is referenced by:  ifptru  1071  cad1  1618  raldifeq  4397  rexreusng  4577  posn  5601  elrnmpt1  5794  dfres3  5823  opelres  5824  fliftf  7047  eroveu  8375  ixpfi2  8806  elfi2  8862  dffi3  8879  cfss  9676  wunex2  10149  nnle1eq1  11655  nn0le0eq0  11913  ixxun  12742  ioopos  12802  injresinj  13153  hashle00  13757  prprrab  13827  xpcogend  14325  cnpart  14591  fz1f1o  15059  nndivdvds  15608  dvdsmultr2  15641  bitsmod  15775  sadadd  15806  sadass  15810  smuval2  15821  smumul  15832  pcmpt  16218  pcmpt2  16219  prmreclem2  16243  prmreclem5  16246  ramcl  16355  mrcidb2  16881  acsfn  16922  fncnvimaeqv  17362  latleeqj1  17665  resmndismnd  17965  pgpssslw  18731  subgdmdprd  19149  acsfn1p  19571  lssle0  19714  islpir2  20017  islinds3  20523  iscld4  21670  cncnpi  21883  cnprest2  21895  lmss  21903  isconn2  22019  dfconn2  22024  subislly  22086  lly1stc  22101  elptr  22178  txcn  22231  xkoinjcn  22292  tsmsres  22749  isxmet2d  22934  xmetgt0  22965  prdsxmetlem  22975  imasdsf1olem  22980  xblss2  23009  stdbdbl  23124  prdsxmslem2  23136  xrtgioo  23411  xrsxmet  23414  cnmpopc  23533  elpi1i  23651  minveclem7  24039  elovolmr  24080  ismbf  24232  mbfmax  24253  itg1val2  24288  mbfi1fseqlem4  24322  itgresr  24382  iblrelem  24394  iblpos  24396  rlimcnp  25551  rlimcnp2  25552  chpchtsum  25803  lgsneg  25905  lgsdilem  25908  2lgslem1a  25975  lmiinv  26586  isspthonpth  27538  s3wwlks2on  27742  clwlkclwwlk  27787  clwwlknonel  27880  clwwlknun  27897  eupth2lem2  28004  frgr3vlem2  28059  numclwwlk2lem1  28161  minvecolem7  28666  shle0  29225  mdsl2bi  30106  dmdbr5ati  30205  cdj3lem1  30217  eulerpartlemr  31742  subfacp1lem3  32542  satefvfmla1  32785  hfext  33757  bj-issetwt  34313  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  mblfinlem3  35096  mblfinlem4  35097  mbfresfi  35103  itg2addnclem  35108  itg2addnc  35111  heiborlem10  35258  dffunsALTV2  36077  dffunsALTV3  36078  dffunsALTV4  36079  elfunsALTV2  36086  elfunsALTV3  36087  elfunsALTV4  36088  elfunsALTV5  36089  dfdisjs2  36102  dfdisjs5  36105  eldisjs2  36116  ople0  36483  atlle0  36601  cdlemg10c  37935  cdlemg33c  38004  hdmap14lem13  39176  mrefg3  39649  radcnvrat  41018  2ffzoeq  43885