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: simp1rr
1021 simp2rr
1025 simp3rr
1029 prepeano4
4452 preaddccan2
4456 tfinltfin
4502 tfinnn
4535 vfinspsslem1
4551 weds
5939 ertr
5955 erth
5969 enadj
6061 enprmaplem3
6079 nntccl
6171 sbthlem1
6204 sbthlem3
6206 sbth
6207 tlecg
6231 nchoicelem6
6295 nchoicelem8
6297 nchoicelem19
6308 nchoice
6309 |