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  1001  3anbi12d  1349  3anbi13d  1350  3anbi23d  1351  3anbi1d  1352  3anbi2d  1353  3anbi3d  1354  sb6x  1827  exdistrfor  1848  a16g  1912  rr19.3v  2945  rr19.28v  2946  euxfr2dc  2991  dfif3  3619  undifexmid  4283  exmidexmid  4286  exmidsssnc  4293  copsexg  4336  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  ordtri2or2exmidlem  4624  onsucsssucexmid  4625  ordsoexmid  4660  0elsucexmid  4663  ordpwsucexmid  4668  ordtri2or2exmid  4669  ontri2orexmidim  4670  dcextest  4679  riotabidv  5973  ov6g  6160  ovg  6161  dfxp3  6359  ssfilem  7062  ssfilemd  7064  diffitest  7076  inffiexmid  7098  unfiexmid  7110  snexxph  7149  ctssexmid  7349  exmidonfinlem  7404  ltsopi  7540  pitri3or  7542  creur  9139  creui  9140  pceu  12873  2irrexpqap  15708  3dom  16613  subctctexmid  16627