Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 395
∧ w3a 1084 |
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 1086 |
This theorem is referenced by: cdlema1N
39173 paddasslem15
39216 4atex2-0aOLDN
39460 4atex3
39463 cdleme19b
39686 cdleme19d
39688 cdleme19e
39689 cdleme20d
39694 cdleme20f
39696 cdleme20g
39697 cdleme21d
39712 cdleme21e
39713 cdleme22cN
39724 cdleme22e
39726 cdleme22f2
39729 cdleme26e
39741 cdleme28a
39752 cdleme37m
39844 cdlemg28b
40085 cdlemk3
40215 cdlemk12
40232 cdlemk12u
40254 cdlemkoatnle-2N
40257 cdlemk13-2N
40258 cdlemkole-2N
40259 cdlemk14-2N
40260 cdlemk15-2N
40261 cdlemk16-2N
40262 cdlemk17-2N
40263 cdlemk18-2N
40268 cdlemk19-2N
40269 cdlemk7u-2N
40270 cdlemk11u-2N
40271 cdlemk20-2N
40274 cdlemk30
40276 cdlemk23-3
40284 cdlemk24-3
40285 |