Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 394
∧ w3a 1085 |
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-an 395
df-3an 1087 |
This theorem is referenced by: ps-2c
38702 cdlema1N
38965 trlval3
39361 cdleme12
39445 cdlemednpq
39473 cdleme19d
39480 cdleme19e
39481 cdleme20f
39488 cdleme20h
39490 cdleme20l2
39495 cdleme20l
39496 cdleme20m
39497 cdleme21j
39510 cdleme22a
39514 cdleme22cN
39516 cdleme22f2
39521 cdleme32b
39616 cdlemg12f
39822 cdlemg12g
39823 cdlemg12
39824 cdlemg28a
39867 cdlemg31b0N
39868 cdlemg29
39879 cdlemg33a
39880 cdlemg36
39888 cdlemg42
39903 cdlemk16a
40030 cdlemk21-2N
40065 cdlemk32
40071 cdlemkid2
40098 cdlemk54
40132 cdlemk55a
40133 dihord10
40397 |