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  632  pm2.621  653  orim1d  688  orim2d  689  pm2.63  700  pm2.74  707  simprimdc  749  oplem1  870  equsex  1598  equsexd  1599  r19.36av  2439  r19.44av  2447  r19.45av  2448  eqsbc3r  2796  reuss  3195  opthpr  3517  relop  4413  swoord2  6047  bj-exlimmp  7016
  Copyright terms: Public domain W3C validator