Colors of
variables: wff set class |
Syntax hints:
= wceq 1353 ifcif 3536 |
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 3537 |
This theorem is referenced by: ctmlemr
7109 xnegpnf
9830 xnegmnf
9831 xaddpnf1
9848 xaddpnf2
9849 xaddmnf1
9850 xaddmnf2
9851 pnfaddmnf
9852 mnfaddpnf
9853 iseqf1olemqk
10496 exp0
10526 sumsnf
11419 prodsnf
11602 lcm0val
12067 ennnfonelemj0
12404 ennnfonelem0
12408 mulg0
12993 lgs0
14453 lgs2
14457 peano3nninf
14795 dceqnconst
14847 |