Theorem biidd 170

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 169	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 9	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3anbi12d  1244  3anbi13d  1245  3anbi23d  1246  3anbi1d  1247  3anbi2d  1248  3anbi3d  1249  sb6x  1702  exdistrfor  1721  a16g  1785  rr19.3v  2733  rr19.28v  2734  euxfr2dc  2777  dfif3  3364  copsexg  3999  ordtriexmidlem2  4264  ordtriexmid  4265  ordtri2orexmid  4266  ontr2exmid  4268  ordtri2or2exmidlem  4269  onsucsssucexmid  4270  ordsoexmid  4305  0elsucexmid  4308  ordpwsucexmid  4313  ordtri2or2exmid  4314  riotabidv  5490  ov6g  5658  ovg  5659  dfxp3  5840  ssfilem  6360  diffitest  6371  ltsopi  6510  pitri3or  6512  creur  8036  creui  8037