Theorem biidd 171

Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)

Assertion

Ref	Expression
biidd	⊢ (𝜑 → (𝜓 ↔ 𝜓))

Proof of Theorem biidd

Step	Hyp	Ref	Expression
1		biid 170	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 9	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anbi12d  1303  3anbi13d  1304  3anbi23d  1305  3anbi1d  1306  3anbi2d  1307  3anbi3d  1308  sb6x  1767  exdistrfor  1788  a16g  1852  rr19.3v  2864  rr19.28v  2865  euxfr2dc  2910  dfif3  3532  undifexmid  4171  exmidexmid  4174  exmidsssnc  4181  copsexg  4221  ordtriexmidlem2  4496  ordtriexmid  4497  ontriexmidim  4498  ordtri2orexmid  4499  ontr2exmid  4501  ordtri2or2exmidlem  4502  onsucsssucexmid  4503  ordsoexmid  4538  0elsucexmid  4541  ordpwsucexmid  4546  ordtri2or2exmid  4547  ontri2orexmidim  4548  dcextest  4557  riotabidv  5799  ov6g  5975  ovg  5976  dfxp3  6159  ssfilem  6837  diffitest  6849  inffiexmid  6868  unfiexmid  6879  snexxph  6911  ctssexmid  7110  exmidonfinlem  7145  ltsopi  7257  pitri3or  7259  creur  8850  creui  8851  pceu  12223  2irrexpqap  13496  subctctexmid  13841