ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  idd Structured version   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  644  pm2.621  665  orim1d  700  orim2d  701  pm2.63  712  pm2.74  719  simprimdc  755  oplem1  881  equsex  1613  equsexd  1614  r19.36av  2455  r19.44av  2463  r19.45av  2464  eqsbc3r  2813  reuss  3212  opthpr  3534  relop  4429  swoord2  6072  indpi  6326  lelttr  6863  elnnz  7991  ztri3or0  8023  xrlelttr  8452  icossicc  8559  iocssicc  8560  ioossico  8561  bj-exlimmp  9178
  Copyright terms: Public domain W3C validator