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  1001  3anbi12d  1349  3anbi13d  1350  3anbi23d  1351  3anbi1d  1352  3anbi2d  1353  3anbi3d  1354  sb6x  1827  exdistrfor  1848  a16g  1912  rr19.3v  2945  rr19.28v  2946  euxfr2dc  2991  dfif3  3619  undifexmid  4283  exmidexmid  4286  exmidsssnc  4293  copsexg  4336  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  ordtri2or2exmidlem  4624  onsucsssucexmid  4625  ordsoexmid  4660  0elsucexmid  4663  ordpwsucexmid  4668  ordtri2or2exmid  4669  ontri2orexmidim  4670  dcextest  4679  riotabidv  5972  ov6g  6159  ovg  6160  dfxp3  6358  ssfilem  7061  ssfilemd  7063  diffitest  7075  inffiexmid  7097  unfiexmid  7109  snexxph  7148  ctssexmid  7348  exmidonfinlem  7403  ltsopi  7539  pitri3or  7541  creur  9138  creui  9139  pceu  12867  2irrexpqap  15701  3dom  16587  subctctexmid  16601