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  1324  3anbi13d  1325  3anbi23d  1326  3anbi1d  1327  3anbi2d  1328  3anbi3d  1329  sb6x  1790  exdistrfor  1811  a16g  1875  rr19.3v  2891  rr19.28v  2892  euxfr2dc  2937  dfif3  3562  undifexmid  4211  exmidexmid  4214  exmidsssnc  4221  copsexg  4262  ordtriexmidlem2  4537  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  ontr2exmid  4542  ordtri2or2exmidlem  4543  onsucsssucexmid  4544  ordsoexmid  4579  0elsucexmid  4582  ordpwsucexmid  4587  ordtri2or2exmid  4588  ontri2orexmidim  4589  dcextest  4598  riotabidv  5853  ov6g  6033  ovg  6034  dfxp3  6218  ssfilem  6902  diffitest  6914  inffiexmid  6933  unfiexmid  6945  snexxph  6978  ctssexmid  7177  exmidonfinlem  7221  ltsopi  7348  pitri3or  7350  creur  8945  creui  8946  pceu  12326  2irrexpqap  14848  subctctexmid  15204