Colors of
variables: wff set class |
Syntax hints: wi 4
w3o 977
w3a 978 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 |
This theorem depends on definitions:
df-bi 117 df-3or 979 df-3an 980 |
This theorem is referenced by: 3jaoian
1305 3ianorr
1309 acexmidlem1
5873 nndceq
6502 nndcel
6503 znegcl
9286 xrltnr
9781 nltpnft
9816 ngtmnft
9819 xrrebnd
9821 xnegcl
9834 xnegneg
9835 xltnegi
9837 xrpnfdc
9844 xrmnfdc
9845 xnegid
9861 xaddid1
9864 xposdif
9884 prm23lt5
12265 zabsle1
14439 |