Theorem biidd 171

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anbi12d  1256  3anbi13d  1257  3anbi23d  1258  3anbi1d  1259  3anbi2d  1260  3anbi3d  1261  sb6x  1716  exdistrfor  1735  a16g  1799  rr19.3v  2769  rr19.28v  2770  euxfr2dc  2814  dfif3  3426  undifexmid  4049  exmidexmid  4052  copsexg  4095  ordtriexmidlem2  4365  ordtriexmid  4366  ordtri2orexmid  4367  ontr2exmid  4369  ordtri2or2exmidlem  4370  onsucsssucexmid  4371  ordsoexmid  4406  0elsucexmid  4409  ordpwsucexmid  4414  ordtri2or2exmid  4415  dcextest  4424  riotabidv  5648  ov6g  5820  ovg  5821  dfxp3  6002  ssfilem  6671  diffitest  6683  inffiexmid  6702  unfiexmid  6708  snexxph  6739  ltsopi  6976  pitri3or  6978  creur  8517  creui  8518