![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fvmptd3 | Unicode version |
Description: Deduction version of fvmpt 5606. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Ref | Expression |
---|---|
fvmptd3.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
fvmptd3.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
fvmptd3.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
fvmptd3.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fvmptd3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmptd3.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fvmptd3.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | nfcv 2329 |
. . 3
![]() ![]() ![]() ![]() | |
4 | nfcv 2329 |
. . 3
![]() ![]() ![]() ![]() | |
5 | fvmptd3.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | fvmptd3.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3, 4, 5, 6 | fvmptf 5621 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2, 7 | syl2anc 411 |
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-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-pr 4221 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-v 2751 df-sbc 2975 df-csb 3070 df-un 3145 df-in 3147 df-ss 3154 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-br 4016 df-opab 4077 df-mpt 4078 df-id 4305 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-iota 5190 df-fun 5230 df-fv 5236 |
This theorem is referenced by: ofvalg 6106 fival 6983 inl11 7078 djuss 7083 ctmlemr 7121 ctssdclemn0 7123 ctssdc 7126 enumctlemm 7127 nninfisollemne 7143 nninfisol 7145 fodjum 7158 fodju0 7159 ismkvnex 7167 nninfwlporlemd 7184 nninfwlpoimlemg 7187 nninfwlpoimlemginf 7188 cc2lem 7279 xrnegiso 11284 summodclem3 11402 fsumf1o 11412 fsum3ser 11419 fsumadd 11428 sumsnf 11431 prodfdivap 11569 prodmodclem3 11597 prodmodclem2a 11598 fprodseq 11605 fprodf1o 11610 prodsnf 11614 fprodshft 11640 fprodrev 11641 eulerthlemh 12245 eulerthlemth 12246 phisum 12254 1arithlem2 12376 ennnfonelemjn 12417 ennnfonelemp1 12421 ctiunctlemfo 12454 nninfdclemf 12464 nninfdclemp1 12465 ptex 12731 divsfvalg 12767 plusffvalg 12800 grpidvalg 12811 issubm 12885 grpinvfvalg 12939 grpinvval 12940 grpsubfvalg 12942 grplactfval 12998 mulgfvalg 13016 issubg 13065 subgex 13068 isnsg 13094 mgpvalg 13175 srglmhm 13245 srgrmhm 13246 opprvalg 13317 reldvdsrsrg 13340 dvdsrvald 13341 isunitd 13354 invrfvald 13370 dvrfvald 13381 issubrng 13419 issubrg 13441 aprval 13471 aprap 13475 scaffvalg 13495 lsssetm 13545 lspfval 13577 lspval 13579 sraval 13626 rlmvalg 13643 2idlvalg 13690 zlmval 13785 ntrval 13906 clsval 13907 cnpval 13994 upxp 14068 uptx 14070 txlm 14075 cnmpt11 14079 cnmpt21 14087 ispsmet 14119 mopnval 14238 bdxmet 14297 cncfmptc 14378 cncfmptid 14379 addccncf 14382 negcncf 14384 ivthdec 14418 limcmpted 14428 cnmptlimc 14439 dvrecap 14473 dveflem 14483 dvef 14484 lgsval 14701 lgsfvalg 14702 lgsdir 14732 lgsdilem2 14733 lgsdi 14734 lgsne0 14735 lgseisenlem2 14747 subctctexmid 15047 nninffeq 15066 trilpolemclim 15081 trilpolemcl 15082 trilpolemisumle 15083 trilpolemeq1 15085 trilpolemlt1 15086 iswomni0 15096 dceqnconst 15105 dcapnconst 15106 nconstwlpolemgt0 15109 |
Copyright terms: Public domain | W3C validator |