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  1802  exdistrfor  1823  a16g  1887  rr19.3v  2912  rr19.28v  2913  euxfr2dc  2958  dfif3  3584  undifexmid  4238  exmidexmid  4241  exmidsssnc  4248  copsexg  4289  ordtriexmidlem2  4569  ordtriexmid  4570  ontriexmidim  4571  ordtri2orexmid  4572  ontr2exmid  4574  ordtri2or2exmidlem  4575  onsucsssucexmid  4576  ordsoexmid  4611  0elsucexmid  4614  ordpwsucexmid  4619  ordtri2or2exmid  4620  ontri2orexmidim  4621  dcextest  4630  riotabidv  5903  ov6g  6086  ovg  6087  dfxp3  6282  ssfilem  6974  diffitest  6986  inffiexmid  7005  unfiexmid  7017  snexxph  7054  ctssexmid  7254  exmidonfinlem  7303  ltsopi  7435  pitri3or  7437  creur  9034  creui  9035  pceu  12651  2irrexpqap  15483  subctctexmid  15974