Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
⟨“cs1 14545 |
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-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-s1 14546 |
This theorem is referenced by: s1prc
14554 ccat1st1st
14578 swrds1
14616 swrdlsw
14617 reuccatpfxs1lem
14696 s2eqd
14814 s3eqd
14815 s4eqd
14816 s5eqd
14817 s6eqd
14818 s7eqd
14819 s8eqd
14820 frmdgsum
18743 psgnunilem5
19362 efgredlemc
19613 vrgpval
19635 vrgpinv
19637 frgpup2
19644 frgpup3lem
19645 pfx1s2
32105 pfxlsw2ccat
32116 iwrdsplit
33386 sseqval
33387 sseqf
33391 sseqp1
33394 signsvtn0
33581 signstfveq0
33588 mrsubcv
34501 |