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  1308  3anbi13d  1309  3anbi23d  1310  3anbi1d  1311  3anbi2d  1312  3anbi3d  1313  sb6x  1772  exdistrfor  1793  a16g  1857  rr19.3v  2869  rr19.28v  2870  euxfr2dc  2915  dfif3  3538  undifexmid  4177  exmidexmid  4180  exmidsssnc  4187  copsexg  4227  ordtriexmidlem2  4502  ordtriexmid  4503  ontriexmidim  4504  ordtri2orexmid  4505  ontr2exmid  4507  ordtri2or2exmidlem  4508  onsucsssucexmid  4509  ordsoexmid  4544  0elsucexmid  4547  ordpwsucexmid  4552  ordtri2or2exmid  4553  ontri2orexmidim  4554  dcextest  4563  riotabidv  5808  ov6g  5987  ovg  5988  dfxp3  6170  ssfilem  6849  diffitest  6861  inffiexmid  6880  unfiexmid  6891  snexxph  6923  ctssexmid  7122  exmidonfinlem  7157  ltsopi  7269  pitri3or  7271  creur  8862  creui  8863  pceu  12236  2irrexpqap  13611  subctctexmid  13956