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

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

Proof of Theorem biidd
StepHypRef Expression
1 biid 170 . 2 (𝜓𝜓)
21a1i 9 1 (𝜑 → (𝜓𝜓))
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  1256  3anbi13d  1257  3anbi23d  1258  3anbi1d  1259  3anbi2d  1260  3anbi3d  1261  sb6x  1716  exdistrfor  1735  a16g  1799  rr19.3v  2769  rr19.28v  2770  euxfr2dc  2814  dfif3  3426  undifexmid  4049  exmidexmid  4052  copsexg  4095  ordtriexmidlem2  4365  ordtriexmid  4366  ordtri2orexmid  4367  ontr2exmid  4369  ordtri2or2exmidlem  4370  onsucsssucexmid  4371  ordsoexmid  4406  0elsucexmid  4409  ordpwsucexmid  4414  ordtri2or2exmid  4415  dcextest  4424  riotabidv  5648  ov6g  5820  ovg  5821  dfxp3  6002  ssfilem  6671  diffitest  6683  inffiexmid  6702  unfiexmid  6708  snexxph  6739  ltsopi  6976  pitri3or  6978  creur  8517  creui  8518
  Copyright terms: Public domain W3C validator