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  999  3anbi12d  1347  3anbi13d  1348  3anbi23d  1349  3anbi1d  1350  3anbi2d  1351  3anbi3d  1352  sb6x  1825  exdistrfor  1846  a16g  1910  rr19.3v  2943  rr19.28v  2944  euxfr2dc  2989  dfif3  3617  undifexmid  4281  exmidexmid  4284  exmidsssnc  4291  copsexg  4334  ordtriexmidlem2  4616  ordtriexmid  4617  ontriexmidim  4618  ordtri2orexmid  4619  ontr2exmid  4621  ordtri2or2exmidlem  4622  onsucsssucexmid  4623  ordsoexmid  4658  0elsucexmid  4661  ordpwsucexmid  4666  ordtri2or2exmid  4667  ontri2orexmidim  4668  dcextest  4677  riotabidv  5968  ov6g  6155  ovg  6156  dfxp3  6354  ssfilem  7057  diffitest  7069  inffiexmid  7091  unfiexmid  7103  snexxph  7140  ctssexmid  7340  exmidonfinlem  7394  ltsopi  7530  pitri3or  7532  creur  9129  creui  9130  pceu  12858  2irrexpqap  15692  3dom  16523  subctctexmid  16537