New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > biidd | Unicode version |
Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.) |
Ref | Expression |
---|---|
biidd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 227 | . 2 | |
2 | 1 | a1i 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 |