Theorem biidd 171

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 170	. 2 |- ( ps <-> ps )
2	1	a1i 9	1 |- ( ph -> ( ps <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anbi12d  1274  3anbi13d  1275  3anbi23d  1276  3anbi1d  1277  3anbi2d  1278  3anbi3d  1279  sb6x  1735  exdistrfor  1754  a16g  1818  rr19.3v  2793  rr19.28v  2794  euxfr2dc  2838  dfif3  3453  undifexmid  4077  exmidexmid  4080  exmidsssnc  4086  copsexg  4126  ordtriexmidlem2  4396  ordtriexmid  4397  ordtri2orexmid  4398  ontr2exmid  4400  ordtri2or2exmidlem  4401  onsucsssucexmid  4402  ordsoexmid  4437  0elsucexmid  4440  ordpwsucexmid  4445  ordtri2or2exmid  4446  dcextest  4455  riotabidv  5686  ov6g  5862  ovg  5863  dfxp3  6046  ssfilem  6722  diffitest  6734  inffiexmid  6753  unfiexmid  6759  snexxph  6790  ctssexmid  6974  ltsopi  7076  pitri3or  7078  creur  8627  creui  8628  subctctexmid  12888