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

Theorem biidd 165
Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
Assertion
Ref Expression
biidd (𝜑 → (𝜓𝜓))

Proof of Theorem biidd
StepHypRef Expression
1 biid 164 . 2 (𝜓𝜓)
21a1i 9 1 (𝜑 → (𝜓𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3anbi12d  1219  3anbi13d  1220  3anbi23d  1221  3anbi1d  1222  3anbi2d  1223  3anbi3d  1224  sb6x  1678  exdistrfor  1697  a16g  1760  rr19.3v  2705  rr19.28v  2706  euxfr2dc  2749  dfif3  3371  copsexg  4009  ordtriexmidlem2  4274  ordtriexmid  4275  ordtri2orexmid  4276  ontr2exmid  4278  ordtri2or2exmidlem  4279  onsucsssucexmid  4280  ordsoexmid  4314  0elsucexmid  4317  ordpwsucexmid  4322  ordtri2or2exmid  4324  riotabidv  5498  ov6g  5666  ovg  5667  dfxp3  5848  ssfiexmid  6367  diffitest  6375  ltsopi  6476  pitri3or  6478  creur  7987  creui  7988
  Copyright terms: Public domain W3C validator