Colors of
variables: wff
setvar class |
Syntax hints: ⊤wtru 1543 Ⅎwnfc 2884 ⦋csb 3894 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-sbc 3779 df-csb 3895 |
This theorem is referenced by: nfcsb1v
3919 fsumsplit1
15691 iundisj
25065 disjabrex
31813 disjabrexf
31814 iundisjf
31820 iundisjfi
32007 rdgssun
36259 disjinfi
43891 fsumsermpt
44295 climsubmpt
44376 climeldmeqmpt
44384 climfveqmpt
44387 climfveqmpt3
44398 climeldmeqmpt3
44405 climinf2mpt
44430 climinfmpt
44431 dvmptmulf
44653 dvnmptdivc
44654 sge0f1o
45098 sge0lempt
45126 sge0isummpt2
45148 meadjiun
45182 hoimbl2
45381 vonhoire
45388 |