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  4277  exmidexmid  4280  exmidsssnc  4287  copsexg  4330  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucsssucexmid  4619  ordsoexmid  4654  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  ontri2orexmidim  4664  dcextest  4673  riotabidv  5962  ov6g  6149  ovg  6150  dfxp3  6346  ssfilem  7045  diffitest  7057  inffiexmid  7079  unfiexmid  7091  snexxph  7128  ctssexmid  7328  exmidonfinlem  7382  ltsopi  7518  pitri3or  7520  creur  9117  creui  9118  pceu  12833  2irrexpqap  15667  3dom  16411  subctctexmid  16425