Theorem biidd 172

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 171	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 9	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3anbi12d  1324  3anbi13d  1325  3anbi23d  1326  3anbi1d  1327  3anbi2d  1328  3anbi3d  1329  sb6x  1790  exdistrfor  1811  a16g  1875  rr19.3v  2899  rr19.28v  2900  euxfr2dc  2945  dfif3  3570  undifexmid  4222  exmidexmid  4225  exmidsssnc  4232  copsexg  4273  ordtriexmidlem2  4552  ordtriexmid  4553  ontriexmidim  4554  ordtri2orexmid  4555  ontr2exmid  4557  ordtri2or2exmidlem  4558  onsucsssucexmid  4559  ordsoexmid  4594  0elsucexmid  4597  ordpwsucexmid  4602  ordtri2or2exmid  4603  ontri2orexmidim  4604  dcextest  4613  riotabidv  5875  ov6g  6056  ovg  6057  dfxp3  6247  ssfilem  6931  diffitest  6943  inffiexmid  6962  unfiexmid  6974  snexxph  7009  ctssexmid  7209  exmidonfinlem  7253  ltsopi  7380  pitri3or  7382  creur  8978  creui  8979  pceu  12433  2irrexpqap  15110  subctctexmid  15491