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  1002  3anbi12d  1350  3anbi13d  1351  3anbi23d  1352  3anbi1d  1353  3anbi2d  1354  3anbi3d  1355  sb6x  1827  exdistrfor  1848  a16g  1912  rr19.3v  2946  rr19.28v  2947  euxfr2dc  2992  dfif3  3623  undifexmid  4289  exmidexmid  4292  exmidsssnc  4299  copsexg  4342  ordtriexmidlem2  4624  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  ontr2exmid  4629  ordtri2or2exmidlem  4630  onsucsssucexmid  4631  ordsoexmid  4666  0elsucexmid  4669  ordpwsucexmid  4674  ordtri2or2exmid  4675  ontri2orexmidim  4676  dcextest  4685  riotabidv  5983  ov6g  6170  ovg  6171  dfxp3  6368  ssfilem  7105  ssfilemd  7107  diffitest  7119  inffiexmid  7141  unfiexmid  7153  snexxph  7192  ctssexmid  7392  exmidonfinlem  7447  ltsopi  7583  pitri3or  7585  creur  9181  creui  9182  pceu  12931  2irrexpqap  15772  3dom  16691  subctctexmid  16705