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  1779  exdistrfor  1800  a16g  1864  rr19.3v  2876  rr19.28v  2877  euxfr2dc  2922  dfif3  3547  undifexmid  4193  exmidexmid  4196  exmidsssnc  4203  copsexg  4244  ordtriexmidlem2  4519  ordtriexmid  4520  ontriexmidim  4521  ordtri2orexmid  4522  ontr2exmid  4524  ordtri2or2exmidlem  4525  onsucsssucexmid  4526  ordsoexmid  4561  0elsucexmid  4564  ordpwsucexmid  4569  ordtri2or2exmid  4570  ontri2orexmidim  4571  dcextest  4580  riotabidv  5832  ov6g  6011  ovg  6012  dfxp3  6194  ssfilem  6874  diffitest  6886  inffiexmid  6905  unfiexmid  6916  snexxph  6948  ctssexmid  7147  exmidonfinlem  7191  ltsopi  7318  pitri3or  7320  creur  8915  creui  8916  pceu  12294  2irrexpqap  14366  subctctexmid  14720