Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∨ wo 846
∨ w3o 1087 |
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 206 df-or 847
df-3or 1089 |
This theorem is referenced by: 3mix2
1332 3mix3
1333 3mix1i
1334 3mix1d
1337 3jaob
1427 tppreqb
4809 onzsl
7835 sornom
10272 fpwwe2lem12
10637 nn0le2is012
12626 hashv01gt1
14305 hash1to3
14452 cshwshashlem1
17029 zabsle1
26799 nogesgn1o
27176 sltsolem1
27178 nosep1o
27184 colinearalg
28168 frgrregorufr0
29577 frege129d
42514 |