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  1324  3anbi13d  1325  3anbi23d  1326  3anbi1d  1327  3anbi2d  1328  3anbi3d  1329  sb6x  1793  exdistrfor  1814  a16g  1878  rr19.3v  2903  rr19.28v  2904  euxfr2dc  2949  dfif3  3575  undifexmid  4227  exmidexmid  4230  exmidsssnc  4237  copsexg  4278  ordtriexmidlem2  4557  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  ontr2exmid  4562  ordtri2or2exmidlem  4563  onsucsssucexmid  4564  ordsoexmid  4599  0elsucexmid  4602  ordpwsucexmid  4607  ordtri2or2exmid  4608  ontri2orexmidim  4609  dcextest  4618  riotabidv  5880  ov6g  6062  ovg  6063  dfxp3  6253  ssfilem  6937  diffitest  6949  inffiexmid  6968  unfiexmid  6980  snexxph  7017  ctssexmid  7217  exmidonfinlem  7262  ltsopi  7389  pitri3or  7391  creur  8988  creui  8989  pceu  12474  2irrexpqap  15224  subctctexmid  15655