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  1323  3anbi13d  1324  3anbi23d  1325  3anbi1d  1326  3anbi2d  1327  3anbi3d  1328  sb6x  1789  exdistrfor  1810  a16g  1874  rr19.3v  2888  rr19.28v  2889  euxfr2dc  2934  dfif3  3559  undifexmid  4205  exmidexmid  4208  exmidsssnc  4215  copsexg  4256  ordtriexmidlem2  4531  ordtriexmid  4532  ontriexmidim  4533  ordtri2orexmid  4534  ontr2exmid  4536  ordtri2or2exmidlem  4537  onsucsssucexmid  4538  ordsoexmid  4573  0elsucexmid  4576  ordpwsucexmid  4581  ordtri2or2exmid  4582  ontri2orexmidim  4583  dcextest  4592  riotabidv  5846  ov6g  6026  ovg  6027  dfxp3  6209  ssfilem  6889  diffitest  6901  inffiexmid  6920  unfiexmid  6931  snexxph  6963  ctssexmid  7162  exmidonfinlem  7206  ltsopi  7333  pitri3or  7335  creur  8930  creui  8931  pceu  12309  2irrexpqap  14749  subctctexmid  15104