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:  ifpbi23d  999  3anbi12d  1347  3anbi13d  1348  3anbi23d  1349  3anbi1d  1350  3anbi2d  1351  3anbi3d  1352  sb6x  1825  exdistrfor  1846  a16g  1910  rr19.3v  2942  rr19.28v  2943  euxfr2dc  2988  dfif3  3616  undifexmid  4277  exmidexmid  4280  exmidsssnc  4287  copsexg  4330  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucsssucexmid  4619  ordsoexmid  4654  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  ontri2orexmidim  4664  dcextest  4673  riotabidv  5956  ov6g  6143  ovg  6144  dfxp3  6340  ssfilem  7037  diffitest  7049  inffiexmid  7068  unfiexmid  7080  snexxph  7117  ctssexmid  7317  exmidonfinlem  7371  ltsopi  7507  pitri3or  7509  creur  9106  creui  9107  pceu  12818  2irrexpqap  15652  subctctexmid  16366