![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fvmptd3 | Unicode version |
Description: Deduction version of fvmpt 5452. (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 2255 |
. . 3
![]() ![]() ![]() ![]() | |
4 | nfcv 2255 |
. . 3
![]() ![]() ![]() ![]() | |
5 | fvmptd3.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | fvmptd3.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3, 4, 5, 6 | fvmptf 5467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2, 7 | syl2anc 406 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-pow 4058 ax-pr 4091 |
This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-v 2659 df-sbc 2879 df-csb 2972 df-un 3041 df-in 3043 df-ss 3050 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-br 3896 df-opab 3950 df-mpt 3951 df-id 4175 df-xp 4505 df-rel 4506 df-cnv 4507 df-co 4508 df-dm 4509 df-iota 5046 df-fun 5083 df-fv 5089 |
This theorem is referenced by: ofvalg 5945 fival 6810 inl11 6902 djuss 6907 ctmlemr 6945 ctssdclemn0 6947 ctssdc 6950 enumctlemm 6951 fodjum 6968 fodju0 6969 ismkvnex 6979 xrnegiso 10920 summodclem3 11038 fsumf1o 11048 fsum3ser 11055 fsumadd 11064 sumsnf 11067 ennnfonelemjn 11757 ennnfonelemp1 11761 ctiunctlemfo 11792 ntrval 12119 clsval 12120 cnpval 12206 upxp 12280 uptx 12282 txlm 12287 cnmpt11 12291 cnmpt21 12299 ispsmet 12309 mopnval 12428 bdxmet 12487 cncfmptc 12565 cncfmptid 12566 addccncf 12569 negcncf 12571 limcmpted 12585 cnmptlimc 12596 subctctexmid 12880 nninffeq 12900 trilpolemclim 12913 trilpolemcl 12914 trilpolemisumle 12915 trilpolemeq1 12917 trilpolemlt1 12918 |
Copyright terms: Public domain | W3C validator |