Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 395
∧ 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 396
df-3an 1087 |
This theorem is referenced by: ps-2c
38938 cdlema1N
39201 trlval3
39597 cdleme12
39681 cdlemednpq
39709 cdleme19d
39716 cdleme19e
39717 cdleme20f
39724 cdleme20h
39726 cdleme20l2
39731 cdleme20l
39732 cdleme20m
39733 cdleme21j
39746 cdleme22a
39750 cdleme22cN
39752 cdleme22f2
39757 cdleme32b
39852 cdlemg12f
40058 cdlemg12g
40059 cdlemg12
40060 cdlemg28a
40103 cdlemg31b0N
40104 cdlemg29
40115 cdlemg33a
40116 cdlemg36
40124 cdlemg42
40139 cdlemk16a
40266 cdlemk21-2N
40301 cdlemk32
40307 cdlemkid2
40334 cdlemk54
40368 cdlemk55a
40369 dihord10
40633 |