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  74  ancld  318  ancrd  319  anim12d  328  anim1d  329  anim2d  330  orel2  680  pm2.621  701  orim1d  736  orim2d  737  pm2.63  749  pm2.74  756  simprimdc  794  oplem1  921  equsex  1663  equsexd  1664  r19.36av  2518  r19.44av  2526  r19.45av  2527  reuss  3278  opthpr  3611  relop  4574  swoord2  6302  indpi  6880  lelttr  7552  elnnz  8730  ztri3or0  8762  xrlelttr  9240  icossicc  9347  iocssicc  9348  ioossico  9349  bj-exlimmp  11327
  Copyright terms: Public domain W3C validator