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:  ifpbi23d  1006  3anbi12d  1354  3anbi13d  1355  3anbi23d  1356  3anbi1d  1357  3anbi2d  1358  3anbi3d  1359  sb6x  1832  exdistrfor  1853  a16g  1917  rr19.3v  2965  rr19.28v  2966  euxfr2dc  3011  dfif3  3651  undifexmid  4325  exmidexmid  4328  exmidsssnc  4335  copsexg  4379  ordtriexmidlem2  4662  ordtriexmid  4663  ontriexmidim  4664  ordtri2orexmid  4665  ontr2exmid  4667  ordtri2or2exmidlem  4668  onsucsssucexmid  4669  ordsoexmid  4704  0elsucexmid  4707  ordpwsucexmid  4712  ordtri2or2exmid  4713  ontri2orexmidim  4714  dcextest  4723  riotabidv  6030  ov6g  6217  ovg  6218  dfxp3  6420  ssfilem  7167  ssfilemd  7169  diffitest  7181  inffiexmid  7203  unfiexmid  7215  snexxph  7257  ctssexmid  7480  exmidonfinlem  7535  ltsopi  7677  pitri3or  7679  creur  9279  creui  9280  pceu  13052  2irrexpqap  16003  3dom  16932  subctctexmid  16944