Colors of
variables: term |
Syntax hints: ≤
wle 2 1wt 8 |
This theorem was proved from axioms:
ax-a2 31 ax-a4 33 ax-r1 35
ax-r2 36 ax-r5 38 |
This theorem depends on definitions:
df-t 41 df-le1 130 |
This theorem is referenced by: ka4lemo
228 wlem1
243 bina5
286 wql1lem
287 wql2lem
288 womle2a
295 womle2b
296 womle3b
297 nom23
316 2vwomlem
365 wr5-2v
366 wom3
367 wdf-c2
384 ska2
432 ska4
433 wom2
434 ka4ot
435 cmtr1com
493 i3or
497 u3lemax4
796 u3lemax5
797 3vded11
814 3vded12
815 3vroa
831 oa3-2to4
988 oa3-u1
991 oa3-u2
992 lem3.3.5lem
1054 lem4.6.7
1103 wdwom
1106 dp15lema
1154 xdp15
1199 xxdp15
1202 xdp45lem
1204 xdp43lem
1205 xdp45
1206 xdp43
1207 3dp43
1208 |