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  1313  3anbi13d  1314  3anbi23d  1315  3anbi1d  1316  3anbi2d  1317  3anbi3d  1318  sb6x  1779  exdistrfor  1800  a16g  1864  rr19.3v  2877  rr19.28v  2878  euxfr2dc  2923  dfif3  3548  undifexmid  4194  exmidexmid  4197  exmidsssnc  4204  copsexg  4245  ordtriexmidlem2  4520  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  ontr2exmid  4525  ordtri2or2exmidlem  4526  onsucsssucexmid  4527  ordsoexmid  4562  0elsucexmid  4565  ordpwsucexmid  4570  ordtri2or2exmid  4571  ontri2orexmidim  4572  dcextest  4581  riotabidv  5833  ov6g  6012  ovg  6013  dfxp3  6195  ssfilem  6875  diffitest  6887  inffiexmid  6906  unfiexmid  6917  snexxph  6949  ctssexmid  7148  exmidonfinlem  7192  ltsopi  7319  pitri3or  7321  creur  8916  creui  8917  pceu  12295  2irrexpqap  14399  subctctexmid  14753