Colors of
variables: term |
Syntax hints: =
wb 1 ⊥ wn 4
∪ wo 6 ∩ wa 7 |
This theorem was proved from axioms:
ax-a1 30 ax-r1 35 ax-r2 36
ax-r4 37 ax-r5 38 |
This theorem depends on definitions:
df-a 40 |
This theorem is referenced by: oran1
91 dff
101 omlem2
128 wwcomd
214 lei3
246 mccune2
247 ni31
250 ud4lem0c
280 ud5lem0c
281 2vwomlem
365 wfh3
425 wfh4
426 fh3
471 fh4
472 i3bi
496 ni32
502 i3th1
543 i3con
551 ud2lem2
564 ud3lem1d
569 ud3lem2
571 ud3lem3
576 ud4lem1a
577 ud4lem1c
579 ud4lem2
582 ud5lem2
590 ud5lem3b
592 ud5lem3c
593 ud5lem3
594 u1lemnaa
640 u2lemnaa
641 u3lemnaa
642 u4lemnaa
643 u5lemnaa
644 u3lemnana
647 u5lemnana
649 u4lemnab
653 u5lemnab
654 u2lemnoa
661 u3lemnoa
662 u4lemnoa
663 u5lemnoa
664 u1lemnonb
675 u3lemnonb
677 u4lemnonb
678 u5lemnonb
679 u3lem1n
741 u4lem1n
742 u5lem1n
743 u3lem3n
754 u1lem11
780 u3lem13a
789 u3lem13b
790 test
802 3vded11
814 neg3antlem2
865 elimcons
868 |