ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biidd Unicode version

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
StepHypRef Expression
1 biid 170 . 2  |-  ( ps  <->  ps )
21a1i 9 1  |-  ( ph  ->  ( ps  <->  ps )
)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator