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  1191  3anbi13d  1192  3anbi23d  1193  3anbi1d  1194  3anbi2d  1195  3anbi3d  1196  sb6x  1640  exdistrfor  1659  a16g  1722  rr19.3v  2655  rr19.28v  2656  euxfr2dc  2699  dfif3  3316  copsexg  3951  ordtriexmidlem2  4189  ordtriexmid  4190  ordtri2orexmid  4191  onsucsssucexmid  4192  ordsoexmid  4220  ordpwsucexmid  4226  riotabidv  5391  ov6g  5557  ovg  5558  dfxp3  5739  ltsopi  6174  pitri3or  6176
  Copyright terms: Public domain W3C validator