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  1326  3anbi13d  1327  3anbi23d  1328  3anbi1d  1329  3anbi2d  1330  3anbi3d  1331  sb6x  1803  exdistrfor  1824  a16g  1888  rr19.3v  2919  rr19.28v  2920  euxfr2dc  2965  dfif3  3593  undifexmid  4253  exmidexmid  4256  exmidsssnc  4263  copsexg  4306  ordtriexmidlem2  4586  ordtriexmid  4587  ontriexmidim  4588  ordtri2orexmid  4589  ontr2exmid  4591  ordtri2or2exmidlem  4592  onsucsssucexmid  4593  ordsoexmid  4628  0elsucexmid  4631  ordpwsucexmid  4636  ordtri2or2exmid  4637  ontri2orexmidim  4638  dcextest  4647  riotabidv  5924  ov6g  6107  ovg  6108  dfxp3  6303  ssfilem  6998  diffitest  7010  inffiexmid  7029  unfiexmid  7041  snexxph  7078  ctssexmid  7278  exmidonfinlem  7332  ltsopi  7468  pitri3or  7470  creur  9067  creui  9068  pceu  12733  2irrexpqap  15565  subctctexmid  16139