Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 ∧
w3a 934 |
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
df-3an 936 |
This theorem is referenced by: simpl2
959 simpr2
962 simp2i
965 simp2d
968 simp12
986 simp22
989 simp32
992 syld3an3
1227 opkthg
4132 nnsucelrlem3
4427 ltfintri
4467 ncfindi
4476 sfintfin
4533 vfintle
4547 phi11lem1
4596 fvopab4t
5386 xpassen
6058 nenpw1pwlem2
6086 ceclnn1
6190 spacssnc
6285 spaccl
6287 nchoicelem17
6306 |