Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 394
∈ wcel 2104 Tr wtr 5264
Ord word 6362 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-in 3954 df-ss 3964 df-uni 4908 df-tr 5265 df-ord 6366 |
This theorem is referenced by: ontr1
6409 dfsmo2
8349 smores2
8356 smoel
8362 smogt
8369 ordiso2
9512 r1ordg
9775 r1pwss
9781 r1val1
9783 rankr1ai
9795 rankval3b
9823 rankonidlem
9825 onssr1
9828 cofsmo
10266 fpwwe2lem8
10635 nosepssdm
27425 bnj1098
34092 bnj594
34221 |