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  73  ancld  312  ancrd  313  anim12d  322  anim1d  323  anim2d  324  orel2  655  pm2.621  676  orim1d  711  orim2d  712  pm2.63  724  pm2.74  731  simprimdc  767  oplem1  893  equsex  1632  equsexd  1633  r19.36av  2478  r19.44av  2486  r19.45av  2487  reuss  3246  opthpr  3571  relop  4514  swoord2  6167  indpi  6498  lelttr  7165  elnnz  8312  ztri3or0  8344  xrlelttr  8823  icossicc  8930  iocssicc  8931  ioossico  8932  bj-exlimmp  10296
  Copyright terms: Public domain W3C validator