Colors of
variables: wff
setvar class |
Syntax hints: ⊤wtru 1542 Ⅎwnfc 2883 ⦋csb 3893 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-sbc 3778 df-csb 3894 |
This theorem is referenced by: nfcsb1v
3918 fsumsplit1
15695 iundisj
25289 disjabrex
32068 disjabrexf
32069 iundisjf
32075 iundisjfi
32262 rdgssun
36562 disjinfi
44190 fsumsermpt
44594 climsubmpt
44675 climeldmeqmpt
44683 climfveqmpt
44686 climfveqmpt3
44697 climeldmeqmpt3
44704 climinf2mpt
44729 climinfmpt
44730 dvmptmulf
44952 dvnmptdivc
44953 sge0f1o
45397 sge0lempt
45425 sge0isummpt2
45447 meadjiun
45481 hoimbl2
45680 vonhoire
45687 |