Colors of
variables: term |
Syntax hints: C
wc 3 ∩ wa 7 |
This theorem was proved from axioms:
ax-a1 30 ax-a2 31 ax-a5 34
ax-r1 35 ax-r2 36 ax-r4 37
ax-r5 38 |
This theorem depends on definitions:
df-a 40 df-le1 130 df-le2 131 df-c1 132
df-c2 133 |
This theorem is referenced by: comanr2
465 gsth
489 dfi3b
499 i3con
551 ud1lem1
560 ud2lem3
565 ud3lem1a
566 ud3lem1c
568 ud3lem1
570 ud3lem3d
575 ud3lem3
576 ud4lem1a
577 ud4lem1b
578 ud4lem1c
579 ud4lem1
581 ud5lem1a
586 ud5lem1b
587 ud5lem1
589 ud5lem3a
591 ud5lem3
594 u2lemaa
601 u2lemana
606 u1lemab
610 u3lemab
612 u1lemanb
615 u3lemanb
617 u2lemle2
716 u1lembi
720 u2lembi
721 u1lem4
757 u4lem6
768 u1lem8
776 u3lem11
786 u3lem13b
790 1oa
820 mlalem
832 bi3
839 mlaconj4
844 neg3antlem2
865 comanblem1
870 cancellem
891 govar
896 lem4.6.2e1
1082 |