![]() |
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 1443 |
. . 3
![]() ![]() ![]() ![]() | |
2 | nfralxy.1 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | nfralxy.2 |
. . . 4
![]() ![]() ![]() ![]() | |
5 | 4 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 3, 5 | nfraldxy 2470 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | mptru 1341 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ral 2422 |
This theorem is referenced by: nfra2xy 2478 rspc2 2804 sbcralt 2989 sbcralg 2991 raaanlem 3473 nfint 3789 nfiinxy 3848 nfpo 4231 nfso 4232 nfse 4271 nffrfor 4278 nfwe 4285 ralxpf 4693 funimaexglem 5214 fun11iun 5396 dff13f 5679 nfiso 5715 mpoeq123 5838 nfofr 5996 fmpox 6106 nfrecs 6212 xpf1o 6746 ac6sfi 6800 ismkvnex 7037 lble 8729 fzrevral 9916 nfsum1 11157 nfsum 11158 fsum2dlemstep 11235 fisumcom2 11239 nfcprod1 11355 nfcprod 11356 bezoutlemmain 11722 cnmpt21 12499 setindis 13336 bdsetindis 13338 strcollnfALT 13355 isomninnlem 13400 iswomninnlem 13417 ismkvnnlem 13419 |
Copyright terms: Public domain | W3C validator |