Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 \/ w3o 972 |
This theorem is referenced by: 3mix3i
1170 3mix3d
1173 3jaob
1290 tpid3g
4145 tppreqb
4171 onzsl
6681 sornom
8678 fpwwe2lem13
9041 nn01to3
11204 qbtwnxr
11428 hash1to3
12530 cshwshashlem1
14580 ostth
23824 sltsolem1
29428 btwncolinear1
29719 limcicciooub
31643 tpres
32554 nn0le2is012
32956 tpid3gVD
33642 |
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 185 df-or 370
df-3or 974 |