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  4237  exmidexmid  4240  exmidsssnc  4247  copsexg  4288  ordtriexmidlem2  4568  ordtriexmid  4569  ontriexmidim  4570  ordtri2orexmid  4571  ontr2exmid  4573  ordtri2or2exmidlem  4574  onsucsssucexmid  4575  ordsoexmid  4610  0elsucexmid  4613  ordpwsucexmid  4618  ordtri2or2exmid  4619  ontri2orexmidim  4620  dcextest  4629  riotabidv  5901  ov6g  6084  ovg  6085  dfxp3  6280  ssfilem  6972  diffitest  6984  inffiexmid  7003  unfiexmid  7015  snexxph  7052  ctssexmid  7252  exmidonfinlem  7301  ltsopi  7433  pitri3or  7435  creur  9032  creui  9033  pceu  12618  2irrexpqap  15450  subctctexmid  15937