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

Theorem biidd 170
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 169 . 2  |-  ( ps  <->  ps )
21a1i 9 1  |-  ( ph  ->  ( ps  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3anbi12d  1245  3anbi13d  1246  3anbi23d  1247  3anbi1d  1248  3anbi2d  1249  3anbi3d  1250  sb6x  1703  exdistrfor  1722  a16g  1786  rr19.3v  2734  rr19.28v  2735  euxfr2dc  2778  dfif3  3372  copsexg  4007  ordtriexmidlem2  4272  ordtriexmid  4273  ordtri2orexmid  4274  ontr2exmid  4276  ordtri2or2exmidlem  4277  onsucsssucexmid  4278  ordsoexmid  4313  0elsucexmid  4316  ordpwsucexmid  4321  ordtri2or2exmid  4322  riotabidv  5501  ov6g  5669  ovg  5670  dfxp3  5851  ssfilem  6410  diffitest  6421  unfiexmid  6438  ltsopi  6572  pitri3or  6574  creur  8103  creui  8104
  Copyright terms: Public domain W3C validator