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  1790  exdistrfor  1811  a16g  1875  rr19.3v  2900  rr19.28v  2901  euxfr2dc  2946  dfif3  3571  undifexmid  4223  exmidexmid  4226  exmidsssnc  4233  copsexg  4274  ordtriexmidlem2  4553  ordtriexmid  4554  ontriexmidim  4555  ordtri2orexmid  4556  ontr2exmid  4558  ordtri2or2exmidlem  4559  onsucsssucexmid  4560  ordsoexmid  4595  0elsucexmid  4598  ordpwsucexmid  4603  ordtri2or2exmid  4604  ontri2orexmidim  4605  dcextest  4614  riotabidv  5876  ov6g  6058  ovg  6059  dfxp3  6249  ssfilem  6933  diffitest  6945  inffiexmid  6964  unfiexmid  6976  snexxph  7011  ctssexmid  7211  exmidonfinlem  7255  ltsopi  7382  pitri3or  7384  creur  8980  creui  8981  pceu  12436  2irrexpqap  15151  subctctexmid  15561