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  1291  3anbi13d  1292  3anbi23d  1293  3anbi1d  1294  3anbi2d  1295  3anbi3d  1296  sb6x  1752  exdistrfor  1772  a16g  1836  rr19.3v  2818  rr19.28v  2819  euxfr2dc  2864  dfif3  3482  undifexmid  4112  exmidexmid  4115  exmidsssnc  4121  copsexg  4161  ordtriexmidlem2  4431  ordtriexmid  4432  ordtri2orexmid  4433  ontr2exmid  4435  ordtri2or2exmidlem  4436  onsucsssucexmid  4437  ordsoexmid  4472  0elsucexmid  4475  ordpwsucexmid  4480  ordtri2or2exmid  4481  dcextest  4490  riotabidv  5725  ov6g  5901  ovg  5902  dfxp3  6085  ssfilem  6762  diffitest  6774  inffiexmid  6793  unfiexmid  6799  snexxph  6831  ctssexmid  7017  exmidonfinlem  7042  ltsopi  7121  pitri3or  7123  creur  8710  creui  8711  subctctexmid  13185