ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biidd Structured version   GIF version

Theorem biidd 161
Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
Assertion
Ref Expression
biidd (φ → (ψψ))

Proof of Theorem biidd
StepHypRef Expression
1 biid 160 . 2 (ψψ)
21a1i 9 1 (φ → (ψψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3anbi12d  1207  3anbi13d  1208  3anbi23d  1209  3anbi1d  1210  3anbi2d  1211  3anbi3d  1212  sb6x  1659  exdistrfor  1678  a16g  1741  rr19.3v  2676  rr19.28v  2677  euxfr2dc  2720  dfif3  3337  copsexg  3972  ordtriexmidlem2  4209  ordtriexmid  4210  ordtri2orexmid  4211  onsucsssucexmid  4212  ordsoexmid  4240  ordpwsucexmid  4246  riotabidv  5413  ov6g  5580  ovg  5581  dfxp3  5762  ssfiexmid  6254  ltsopi  6304  pitri3or  6306  creur  7672  creui  7673
  Copyright terms: Public domain W3C validator