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
2981 rr19.28v
2982 moeq3
3014 euxfr2
3022 dfif3
3673 otkelins2kg
4254 otkelins3kg
4255 copsexg
4608 br1stg
4731 dmsnopg
5067 rnsnop
5076 opbr1st
5502 opbr2nd
5503 ov6g
5601 ovg
5602 pmvalg
6011 |