Colors of
variables: term |
Syntax hints: =
wb 1 ⊥ wn 4
∪ wo 6 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 |
This theorem is referenced by: or1r
105 an0
108 le1
146 sklem
230 0i1
273 wle1
389 ska2
432 woml6
436 oml6
488 i3con
551 ud1lem3
562 ud3lem1c
568 ud3lem3
576 ud4lem1c
579 ud4lem1
581 ud4lem3b
584 ud5lem1
589 u1lemoa
620 u4lemoa
623 u2lemonb
636 u3lemonb
637 u4lem5
764 u4lem6
768 u1lem11
780 u3lem8
783 u3lem11
786 test
802 2oalem1
825 oa6v4v
933 lem3.3.7i0e1
1057 lem3.3.7i3e2
1067 |