![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rabbidv | Unicode version |
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
Ref | Expression |
---|---|
rabbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rabbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 270 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rabbidva 2607 |
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-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-11 1442 ax-4 1445 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-tru 1292 df-nf 1395 df-sb 1693 df-clab 2075 df-cleq 2081 df-ral 2364 df-rab 2368 |
This theorem is referenced by: rabeqbidv 2614 difeq2 3112 seex 4162 mptiniseg 4925 supeq1 6681 supeq2 6684 supeq3 6685 cardcl 6809 isnumi 6810 cardval3ex 6813 carden2bex 6817 genpdflem 7066 genipv 7068 genpelxp 7070 addcomprg 7137 mulcomprg 7139 uzval 9021 ixxval 9314 fzval 9426 hashinfom 10186 hashennn 10188 shftfn 10258 gcdval 11229 lcmval 11323 isprm 11369 istopon 11610 toponsspwpwg 11618 |
Copyright terms: Public domain | W3C validator |