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  1313  3anbi13d  1314  3anbi23d  1315  3anbi1d  1316  3anbi2d  1317  3anbi3d  1318  sb6x  1777  exdistrfor  1798  a16g  1862  rr19.3v  2874  rr19.28v  2875  euxfr2dc  2920  dfif3  3545  undifexmid  4188  exmidexmid  4191  exmidsssnc  4198  copsexg  4238  ordtriexmidlem2  4513  ordtriexmid  4514  ontriexmidim  4515  ordtri2orexmid  4516  ontr2exmid  4518  ordtri2or2exmidlem  4519  onsucsssucexmid  4520  ordsoexmid  4555  0elsucexmid  4558  ordpwsucexmid  4563  ordtri2or2exmid  4564  ontri2orexmidim  4565  dcextest  4574  riotabidv  5823  ov6g  6002  ovg  6003  dfxp3  6185  ssfilem  6865  diffitest  6877  inffiexmid  6896  unfiexmid  6907  snexxph  6939  ctssexmid  7138  exmidonfinlem  7182  ltsopi  7294  pitri3or  7296  creur  8889  creui  8890  pceu  12262  2irrexpqap  13967  subctctexmid  14311