Theorem biidd 172

Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)

Assertion

Ref	Expression
biidd	|- ( ph -> ( ps <-> ps ) )

Proof of Theorem biidd

Step	Hyp	Ref	Expression
1		biid 171	. 2 |- ( ps <-> ps )
2	1	a1i 9	1 |- ( ph -> ( ps <-> ps ) )

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:  3anbi12d  1324  3anbi13d  1325  3anbi23d  1326  3anbi1d  1327  3anbi2d  1328  3anbi3d  1329  sb6x  1793  exdistrfor  1814  a16g  1878  rr19.3v  2903  rr19.28v  2904  euxfr2dc  2949  dfif3  3575  undifexmid  4227  exmidexmid  4230  exmidsssnc  4237  copsexg  4278  ordtriexmidlem2  4557  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  ontr2exmid  4562  ordtri2or2exmidlem  4563  onsucsssucexmid  4564  ordsoexmid  4599  0elsucexmid  4602  ordpwsucexmid  4607  ordtri2or2exmid  4608  ontri2orexmidim  4609  dcextest  4618  riotabidv  5882  ov6g  6065  ovg  6066  dfxp3  6261  ssfilem  6945  diffitest  6957  inffiexmid  6976  unfiexmid  6988  snexxph  7025  ctssexmid  7225  exmidonfinlem  7272  ltsopi  7404  pitri3or  7406  creur  9003  creui  9004  pceu  12489  2irrexpqap  15298  subctctexmid  15731