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 2437 | . 2 |
3 | 2 | ralbidv 2437 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wral 2416 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-ral 2421 |
This theorem is referenced by: cbvral3v 2667 poeq1 4221 soeq1 4237 isoeq1 5702 isoeq2 5703 isoeq3 5704 fnmpoovd 6112 smoeq 6187 xpf1o 6738 elinp 7282 cauappcvgpr 7470 seq3caopr2 10255 addcn2 11079 mulcn2 11081 ispsmet 12492 ismet 12513 isxmet 12514 addcncntoplem 12720 elcncf 12729 |
Copyright terms: Public domain | W3C validator |