Theorem biidd 171

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 170	. 2 |- ( ps <-> ps )
2	1	a1i 9	1 |- ( ph -> ( ps <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anbi12d  1303  3anbi13d  1304  3anbi23d  1305  3anbi1d  1306  3anbi2d  1307  3anbi3d  1308  sb6x  1767  exdistrfor  1788  a16g  1852  rr19.3v  2865  rr19.28v  2866  euxfr2dc  2911  dfif3  3533  undifexmid  4172  exmidexmid  4175  exmidsssnc  4182  copsexg  4222  ordtriexmidlem2  4497  ordtriexmid  4498  ontriexmidim  4499  ordtri2orexmid  4500  ontr2exmid  4502  ordtri2or2exmidlem  4503  onsucsssucexmid  4504  ordsoexmid  4539  0elsucexmid  4542  ordpwsucexmid  4547  ordtri2or2exmid  4548  ontri2orexmidim  4549  dcextest  4558  riotabidv  5800  ov6g  5979  ovg  5980  dfxp3  6162  ssfilem  6841  diffitest  6853  inffiexmid  6872  unfiexmid  6883  snexxph  6915  ctssexmid  7114  exmidonfinlem  7149  ltsopi  7261  pitri3or  7263  creur  8854  creui  8855  pceu  12227  2irrexpqap  13536  subctctexmid  13881