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  1308  3anbi13d  1309  3anbi23d  1310  3anbi1d  1311  3anbi2d  1312  3anbi3d  1313  sb6x  1772  exdistrfor  1793  a16g  1857  rr19.3v  2869  rr19.28v  2870  euxfr2dc  2915  dfif3  3539  undifexmid  4179  exmidexmid  4182  exmidsssnc  4189  copsexg  4229  ordtriexmidlem2  4504  ordtriexmid  4505  ontriexmidim  4506  ordtri2orexmid  4507  ontr2exmid  4509  ordtri2or2exmidlem  4510  onsucsssucexmid  4511  ordsoexmid  4546  0elsucexmid  4549  ordpwsucexmid  4554  ordtri2or2exmid  4555  ontri2orexmidim  4556  dcextest  4565  riotabidv  5811  ov6g  5990  ovg  5991  dfxp3  6173  ssfilem  6853  diffitest  6865  inffiexmid  6884  unfiexmid  6895  snexxph  6927  ctssexmid  7126  exmidonfinlem  7170  ltsopi  7282  pitri3or  7284  creur  8875  creui  8876  pceu  12249  2irrexpqap  13690  subctctexmid  14034