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

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

Proof of Theorem idd
StepHypRef Expression
1 id 19 . 2 (𝜓𝜓)
21a1i 9 1 (𝜑 → (𝜓𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  imim1d  69  ancld  308  ancrd  309  anim12d  318  anim1d  319  anim2d  320  orel2  645  pm2.621  666  orim1d  701  orim2d  702  pm2.63  713  pm2.74  720  simprimdc  756  oplem1  882  equsex  1616  equsexd  1617  r19.36av  2461  r19.44av  2469  r19.45av  2470  eqsbc3r  2819  reuss  3218  opthpr  3543  relop  4486  swoord2  6136  indpi  6438  lelttr  7104  elnnz  8253  ztri3or0  8285  xrlelttr  8720  icossicc  8827  iocssicc  8828  ioossico  8829  bj-exlimmp  9883
  Copyright terms: Public domain W3C validator