Colors of
variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4
∧ wa 104 ⊥wfal 1358 |
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-in1 614 ax-in2 615 |
This theorem depends on definitions:
df-bi 117 df-tru 1356 df-fal 1359 |
This theorem is referenced by: genpdisj
7522 cauappcvgprlemdisj
7650 caucvgprlemdisj
7673 caucvgprprlemdisj
7701 suplocexprlemdisj
7719 suplocexprlemub
7722 suplocsrlem
7807 resqrexlemgt0
11029 resqrexlemoverl
11030 leabs
11083 climge0
11333 isprm5lem
12141 ennnfonelemex
12415 dedekindeu
14104 dedekindicclemicc
14113 pw1nct
14755 |