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  1002  3anbi12d  1350  3anbi13d  1351  3anbi23d  1352  3anbi1d  1353  3anbi2d  1354  3anbi3d  1355  sb6x  1828  exdistrfor  1849  a16g  1913  rr19.3v  2956  rr19.28v  2957  euxfr2dc  3002  dfif3  3636  undifexmid  4306  exmidexmid  4309  exmidsssnc  4316  copsexg  4360  ordtriexmidlem2  4642  ordtriexmid  4643  ontriexmidim  4644  ordtri2orexmid  4645  ontr2exmid  4647  ordtri2or2exmidlem  4648  onsucsssucexmid  4649  ordsoexmid  4684  0elsucexmid  4687  ordpwsucexmid  4692  ordtri2or2exmid  4693  ontri2orexmidim  4694  dcextest  4703  riotabidv  6005  ov6g  6192  ovg  6193  dfxp3  6390  ssfilem  7130  ssfilemd  7132  diffitest  7144  inffiexmid  7166  unfiexmid  7178  snexxph  7220  ctssexmid  7441  exmidonfinlem  7496  ltsopi  7635  pitri3or  7637  creur  9233  creui  9234  pceu  12993  2irrexpqap  15843  3dom  16762  subctctexmid  16774