![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfralxy | Unicode version |
Description: Not-free for restricted
universal quantification where ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfralxy.1 |
![]() ![]() ![]() ![]() |
nfralxy.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfralxy |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1410 |
. . 3
![]() ![]() ![]() ![]() | |
2 | nfralxy.1 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | nfralxy.2 |
. . . 4
![]() ![]() ![]() ![]() | |
5 | 4 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 3, 5 | nfraldxy 2426 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | mptru 1308 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 ax-17 1474 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ral 2380 |
This theorem is referenced by: nfra2xy 2434 rspc2 2754 sbcralt 2937 sbcralg 2939 raaanlem 3415 nfint 3728 nfiinxy 3787 nfpo 4161 nfso 4162 nfse 4201 nffrfor 4208 nfwe 4215 ralxpf 4623 funimaexglem 5142 fun11iun 5322 dff13f 5603 nfiso 5639 mpoeq123 5762 nfofr 5920 fmpox 6028 nfrecs 6134 xpf1o 6667 ac6sfi 6721 lble 8563 fzrevral 9726 nfsum1 10964 nfsum 10965 fsum2dlemstep 11042 fisumcom2 11046 bezoutlemmain 11479 cnmpt21 12241 setindis 12750 bdsetindis 12752 isomninnlem 12809 |
Copyright terms: Public domain | W3C validator |