Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 |
This theorem depends on definitions:
df-bi 206 |
This theorem is referenced by: nbbn
385 pm5.15
1012 nbi2
1015 xorass
1515 hadnot
1604 nabbib
3046 nmogtmnf
30023 nmopgtmnf
31121 limsucncmpi
35330 wl-3xorbi
36354 wl-3xornot
36362 oneptri
42006 oaordnrex
42045 omnord1ex
42054 oenord1ex
42065 aiffnbandciffatnotciffb
45614 axorbciffatcxorb
45615 abnotbtaxb
45625 afv2orxorb
45936 line2ylem
47437 line2xlem
47439 |