Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 ∧
wa 358 |
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 df-an 360 |
This theorem is referenced by: simp1lr
1019 simp2lr
1023 simp3lr
1027 ax11indalem
2197 ax11inda2ALT
2198 ifboth
3694 intab
3957 prepeano4
4452 leltfintr
4459 lenltfin
4470 tfinnn
4535 phi11lem1
4596 imainss
5043 ncssfin
6152 nntccl
6171 sbth
6207 leconnnc
6219 tlecg
6231 lemuc1
6254 ncslesuc
6268 spacind
6288 nchoicelem8
6297 nchoicelem19
6308 nchoice
6309 fnfrec
6321 |