![]() |
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 1539 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralbidva.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralbida 2484 |
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 1458 ax-gen 1460 ax-4 1521 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 |
This theorem is referenced by: raleqbidva 2700 poinxp 4713 funimass4 5586 fnmptfvd 5640 funimass3 5652 funconstss 5654 cocan1 5808 cocan2 5809 isocnv2 5833 isores2 5834 isoini2 5840 ofrfval 6114 ofrfval2 6122 dfsmo2 6311 smores 6316 smores2 6318 ac6sfi 6925 supisolem 7036 ordiso2 7063 ismkvnex 7182 nninfwlporlemd 7199 caucvgsrlemcau 7821 suplocsrlempr 7835 axsuploc 8059 suprleubex 8940 dfinfre 8942 zextlt 9374 prime 9381 infregelbex 9627 fzshftral 10137 fimaxq 10838 clim 11320 clim2 11322 clim2c 11323 clim0c 11325 climabs0 11346 climrecvg1n 11387 mertenslem2 11575 mertensabs 11576 dfgcd2 12046 sqrt2irr 12193 pc11 12362 pcz 12363 1arith 12398 infpn2 12506 grpidpropdg 12847 sgrppropd 12873 mndpropd 12898 grppropd 12959 issubg4m 13129 rngpropd 13306 ringpropd 13389 oppr1g 13429 lsspropdg 13744 isridlrng 13795 isridl 13816 tgss2 14031 neipsm 14106 ssidcn 14162 lmbrf 14167 cnnei 14184 cnrest2 14188 lmss 14198 lmres 14200 ismet2 14306 elmopn2 14401 metss 14446 metrest 14458 metcnp 14464 metcnp2 14465 metcn 14466 txmetcnp 14470 divcnap 14507 elcncf2 14513 mulc1cncf 14528 cncfmet 14531 cdivcncfap 14539 limcdifap 14583 limcmpted 14584 cnlimc 14593 2sqlem6 14920 iswomni0 15253 cndcap 15261 |
Copyright terms: Public domain | W3C validator |