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-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1d  75  ancld  325  ancrd  326  anim12d  335  anim1d  336  anim2d  337  orel2  726  pm2.621  747  orim1d  787  orim2d  788  pm2.63  800  pm2.74  807  simprimdc  859  oplem1  975  equsex  1728  equsexd  1729  r19.36av  2628  r19.44av  2636  r19.45av  2637  reuss  3416  opthpr  3770  relop  4772  swoord2  6558  indpi  7319  lelttr  8023  elnnz  9239  ztri3or0  9271  xrlelttr  9780  icossicc  9934  iocssicc  9935  ioossico  9936  lmconst  13349  cnptopresti  13371  sslm  13380  bj-exlimmp  14143
  Copyright terms: Public domain W3C validator