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  1292  3anbi13d  1293  3anbi23d  1294  3anbi1d  1295  3anbi2d  1296  3anbi3d  1297  sb6x  1753  exdistrfor  1773  a16g  1837  rr19.3v  2827  rr19.28v  2828  euxfr2dc  2873  dfif3  3492  undifexmid  4125  exmidexmid  4128  exmidsssnc  4134  copsexg  4174  ordtriexmidlem2  4444  ordtriexmid  4445  ordtri2orexmid  4446  ontr2exmid  4448  ordtri2or2exmidlem  4449  onsucsssucexmid  4450  ordsoexmid  4485  0elsucexmid  4488  ordpwsucexmid  4493  ordtri2or2exmid  4494  dcextest  4503  riotabidv  5740  ov6g  5916  ovg  5917  dfxp3  6100  ssfilem  6777  diffitest  6789  inffiexmid  6808  unfiexmid  6814  snexxph  6846  ctssexmid  7032  exmidonfinlem  7066  ltsopi  7152  pitri3or  7154  creur  8741  creui  8742  2irrexpqap  13103  subctctexmid  13369