NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  biidd Unicode version

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

Proof of Theorem biidd
StepHypRef Expression
1 biid 227 . 2
21a1i 10 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  3anbi12d  1253  3anbi13d  1254  3anbi23d  1255  3anbi1d  1256  3anbi2d  1257  3anbi3d  1258  had1  1402  spnfwOLD  1692  spvwOLD  1695  exdistrf  1971  nfald2  1972  sb6x  2029  a16gALT  2049  ax11  2155  a16g-o  2186  ax11indalem  2197  ax11inda2ALT  2198  rr19.3v  2980  rr19.28v  2981  moeq3  3013  euxfr2  3021  dfif3  3672  otkelins2kg  4253  otkelins3kg  4254  copsexg  4607  br1stg  4730  dmsnopg  5066  rnsnop  5075  opbr1st  5501  opbr2nd  5502  ov6g  5600  ovg  5601  pmvalg  6010
  Copyright terms: Public domain W3C validator