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  1002  3anbi12d  1350  3anbi13d  1351  3anbi23d  1352  3anbi1d  1353  3anbi2d  1354  3anbi3d  1355  sb6x  1828  exdistrfor  1849  a16g  1913  rr19.3v  2959  rr19.28v  2960  euxfr2dc  3005  dfif3  3640  undifexmid  4311  exmidexmid  4314  exmidsssnc  4321  copsexg  4365  ordtriexmidlem2  4647  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  ontr2exmid  4652  ordtri2or2exmidlem  4653  onsucsssucexmid  4654  ordsoexmid  4689  0elsucexmid  4692  ordpwsucexmid  4697  ordtri2or2exmid  4698  ontri2orexmidim  4699  dcextest  4708  riotabidv  6013  ov6g  6200  ovg  6201  dfxp3  6403  ssfilem  7143  ssfilemd  7145  diffitest  7157  inffiexmid  7179  unfiexmid  7191  snexxph  7233  ctssexmid  7454  exmidonfinlem  7509  ltsopi  7651  pitri3or  7653  creur  9250  creui  9251  pceu  13018  2irrexpqap  15969  3dom  16888  subctctexmid  16900