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  1326  3anbi13d  1327  3anbi23d  1328  3anbi1d  1329  3anbi2d  1330  3anbi3d  1331  sb6x  1803  exdistrfor  1824  a16g  1888  rr19.3v  2916  rr19.28v  2917  euxfr2dc  2962  dfif3  3588  undifexmid  4244  exmidexmid  4247  exmidsssnc  4254  copsexg  4295  ordtriexmidlem2  4575  ordtriexmid  4576  ontriexmidim  4577  ordtri2orexmid  4578  ontr2exmid  4580  ordtri2or2exmidlem  4581  onsucsssucexmid  4582  ordsoexmid  4617  0elsucexmid  4620  ordpwsucexmid  4625  ordtri2or2exmid  4626  ontri2orexmidim  4627  dcextest  4636  riotabidv  5913  ov6g  6096  ovg  6097  dfxp3  6292  ssfilem  6986  diffitest  6998  inffiexmid  7017  unfiexmid  7029  snexxph  7066  ctssexmid  7266  exmidonfinlem  7316  ltsopi  7448  pitri3or  7450  creur  9047  creui  9048  pceu  12688  2irrexpqap  15520  subctctexmid  16072