![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexralbidv | Unicode version |
Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2ralbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rexralbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ralbidv 2477 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexbidv 2478 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 df-rex 2461 |
This theorem is referenced by: caucvgpr 7659 caucvgprpr 7689 caucvgsrlemgt1 7772 caucvgsrlemoffres 7777 axcaucvglemres 7876 cvg1nlemres 10965 rexfiuz 10969 resqrexlemgt0 11000 resqrexlemoverl 11001 resqrexlemglsq 11002 resqrexlemsqa 11004 resqrexlemex 11005 cau3lem 11094 caubnd2 11097 climi 11266 2clim 11280 ennnfonelemim 12395 lmcvg 13350 lmss 13379 txlm 13412 metcnpi 13648 metcnpi2 13649 elcncf 13693 cncfi 13698 limcimo 13767 cnplimclemr 13771 limccoap 13780 |
Copyright terms: Public domain | W3C validator |