Colors of
variables: wff setvar class |
Syntax hints: wb 176
wtru 1316
wsbc 3047 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions:
df-bi 177 df-an 360
df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-sbc 3048 |
This theorem is referenced by: sbcbiiOLD
3103 eqsbc2
3104 sbccomlem
3117 sbccom
3118 sbcrext
3120 sbcabel
3124 csbco
3146 sbcnel12g
3154 sbcne12g
3155 sbccsbg
3165 sbccsb2g
3166 csbnestgf
3185 csbabg
3198 sbcss
3661 inopab
4863 eqerlem
5961 |