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
5870 nndceq
6499 nndcel
6500 znegcl
9283 xrltnr
9778 nltpnft
9813 ngtmnft
9816 xrrebnd
9818 xnegcl
9831 xnegneg
9832 xltnegi
9834 xrpnfdc
9841 xrmnfdc
9842 xnegid
9858 xaddid1
9861 xposdif
9881 prm23lt5
12262 zabsle1
14370 |