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  2942  rr19.28v  2943  euxfr2dc  2988  dfif3  3616  undifexmid  4276  exmidexmid  4279  exmidsssnc  4286  copsexg  4329  ordtriexmidlem2  4611  ordtriexmid  4612  ontriexmidim  4613  ordtri2orexmid  4614  ontr2exmid  4616  ordtri2or2exmidlem  4617  onsucsssucexmid  4618  ordsoexmid  4653  0elsucexmid  4656  ordpwsucexmid  4661  ordtri2or2exmid  4662  ontri2orexmidim  4663  dcextest  4672  riotabidv  5955  ov6g  6142  ovg  6143  dfxp3  6338  ssfilem  7033  diffitest  7045  inffiexmid  7064  unfiexmid  7076  snexxph  7113  ctssexmid  7313  exmidonfinlem  7367  ltsopi  7503  pitri3or  7505  creur  9102  creui  9103  pceu  12813  2irrexpqap  15646  subctctexmid  16325