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  1793  exdistrfor  1814  a16g  1878  rr19.3v  2903  rr19.28v  2904  euxfr2dc  2949  dfif3  3574  undifexmid  4226  exmidexmid  4229  exmidsssnc  4236  copsexg  4277  ordtriexmidlem2  4556  ordtriexmid  4557  ontriexmidim  4558  ordtri2orexmid  4559  ontr2exmid  4561  ordtri2or2exmidlem  4562  onsucsssucexmid  4563  ordsoexmid  4598  0elsucexmid  4601  ordpwsucexmid  4606  ordtri2or2exmid  4607  ontri2orexmidim  4608  dcextest  4617  riotabidv  5879  ov6g  6061  ovg  6062  dfxp3  6252  ssfilem  6936  diffitest  6948  inffiexmid  6967  unfiexmid  6979  snexxph  7016  ctssexmid  7216  exmidonfinlem  7260  ltsopi  7387  pitri3or  7389  creur  8986  creui  8987  pceu  12464  2irrexpqap  15214  subctctexmid  15645