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: 3imtr4d
259 ax11eq
2193 ax11el
2194 leltfintr
4459 tfin11
4494 sfinltfin
4536 phi11lem1
4596 xp11
5057 xpcan
5058 xpcan2
5059 enprmaplem3
6079 enprmaplem6
6082 ce0addcnnul
6180 ceclb
6184 fce
6189 sbth
6207 dflec2
6211 lectr
6212 leaddc1
6215 leconnnc
6219 tlecg
6231 letc
6232 ce0lenc1
6240 nclenn
6250 lemuc1
6254 lecadd2
6267 ncslesuc
6268 nchoicelem9
6298 nchoicelem12
6301 nchoicelem17
6306 dmfrec
6317 fnfreclem2
6319 fnfreclem3
6320 |