![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2ralbidv | Unicode version |
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
Ref | Expression |
---|---|
2ralbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2ralbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ralbidv 2487 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralbidv 2487 |
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 1457 ax-gen 1459 ax-4 1520 ax-17 1536 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-ral 2470 |
This theorem is referenced by: cbvral3v 2730 poeq1 4311 soeq1 4327 isoeq1 5815 isoeq2 5816 isoeq3 5817 fnmpoovd 6229 smoeq 6304 xpf1o 6857 tapeq1 7264 elinp 7486 cauappcvgpr 7674 seq3caopr2 10495 addcn2 11331 mulcn2 11333 sgrp1 12834 ismhm 12872 issubm 12882 isnsg 13091 nmznsg 13102 iscmn 13127 ring1 13294 issubrg3 13431 islmod 13444 lmodlema 13445 lsssetm 13509 islssmd 13512 islidlm 13632 ispsmet 14063 ismet 14084 isxmet 14085 addcncntoplem 14291 elcncf 14300 |
Copyright terms: Public domain | W3C validator |