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

Theorem idd 21
Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
idd  |-  ( ph  ->  ( ps  ->  ps ) )

Proof of Theorem idd
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
21a1i 9 1  |-  ( ph  ->  ( ps  ->  ps ) )
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  3772  relop  4777  swoord2  6564  indpi  7340  lelttr  8044  elnnz  9261  ztri3or0  9293  xrlelttr  9804  icossicc  9958  iocssicc  9959  ioossico  9960  lmconst  13609  cnptopresti  13631  sslm  13640  bj-exlimmp  14403
  Copyright terms: Public domain W3C validator