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-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3anbi12d  1291  3anbi13d  1292  3anbi23d  1293  3anbi1d  1294  3anbi2d  1295  3anbi3d  1296  sb6x  1752  exdistrfor  1772  a16g  1836  rr19.3v  2823  rr19.28v  2824  euxfr2dc  2869  dfif3  3487  undifexmid  4117  exmidexmid  4120  exmidsssnc  4126  copsexg  4166  ordtriexmidlem2  4436  ordtriexmid  4437  ordtri2orexmid  4438  ontr2exmid  4440  ordtri2or2exmidlem  4441  onsucsssucexmid  4442  ordsoexmid  4477  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  dcextest  4495  riotabidv  5732  ov6g  5908  ovg  5909  dfxp3  6092  ssfilem  6769  diffitest  6781  inffiexmid  6800  unfiexmid  6806  snexxph  6838  ctssexmid  7024  exmidonfinlem  7054  ltsopi  7140  pitri3or  7142  creur  8729  creui  8730  subctctexmid  13280
 Copyright terms: Public domain W3C validator