![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralbidva | Unicode version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralbidva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1466 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralbidva.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralbida 2374 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-4 1445 ax-17 1464 |
This theorem depends on definitions: df-bi 115 df-nf 1395 df-ral 2364 |
This theorem is referenced by: raleqbidva 2576 poinxp 4507 funimass4 5355 funimass3 5415 funconstss 5417 cocan1 5566 cocan2 5567 isocnv2 5591 isores2 5592 isoini2 5598 ofrfval 5864 ofrfval2 5871 dfsmo2 6052 smores 6057 smores2 6059 ac6sfi 6612 supisolem 6701 ordiso2 6726 caucvgsrlemcau 7336 suprleubex 8413 dfinfre 8415 zextlt 8836 prime 8843 fzshftral 9518 fimaxq 10231 clim 10665 clim2 10667 clim2c 10668 clim0c 10670 climabs0 10692 climrecvg1n 10733 mertenslem2 10926 mertensabs 10927 dfgcd2 11277 sqrt2irr 11415 elcncf2 11585 mulc1cncf 11600 |
Copyright terms: Public domain | W3C validator |