Colors of
variables: wff set class |
Syntax hints: wceq 1353 cif 3534 |
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-in2 615 ax-io 709
ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-if 3535 |
This theorem is referenced by: ctmlemr
7106 xnegpnf
9827 xnegmnf
9828 xaddpnf1
9845 xaddpnf2
9846 xaddmnf1
9847 xaddmnf2
9848 pnfaddmnf
9849 mnfaddpnf
9850 iseqf1olemqk
10493 exp0
10523 sumsnf
11416 prodsnf
11599 lcm0val
12064 ennnfonelemj0
12401 ennnfonelem0
12405 mulg0
12987 lgs0
14384 lgs2
14388 peano3nninf
14726 dceqnconst
14777 |