![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4i | Unicode version |
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3imtr4.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
3imtr4.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3imtr4.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3imtr4i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imtr4.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3imtr4.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylbi 114 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3imtr4.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | sylibr 137 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: dcn 745 dcan 841 xordc1 1281 hbxfrbi 1358 nfalt 1467 19.29r 1509 19.31r 1568 sbimi 1644 spsbbi 1722 sbi2v 1769 euan 1953 2exeu 1989 ralimi2 2375 reximi2 2409 r19.28av 2443 r19.29r 2445 elex 2560 rmoan 2733 rmoimi2 2736 sseq2 2961 rabss2 3017 unssdif 3166 inssdif 3167 unssin 3170 inssun 3171 rabn0r 3238 undif4 3278 ssdif0im 3280 inssdif0im 3285 ssundifim 3300 ralf0 3318 prmg 3480 difprsnss 3493 snsspw 3526 pwprss 3567 pwtpss 3568 uniin 3591 intss 3627 iuniin 3658 iuneq1 3661 iuneq2 3664 iundif2ss 3713 iinuniss 3728 iunpwss 3734 intexrabim 3898 exss 3954 pwunss 4011 soeq2 4044 ordunisuc2r 4205 peano5 4264 reliin 4402 coeq1 4436 coeq2 4437 cnveq 4452 dmeq 4478 dmin 4486 dmcoss 4544 rncoeq 4548 resiexg 4596 dminss 4681 imainss 4682 dfco2a 4764 euiotaex 4826 fununi 4910 fof 5049 f1ocnv 5082 rexrnmpt 5253 isocnv 5394 isotr 5399 oprabid 5480 dmtpos 5812 tposfn 5829 smores 5848 eqer 6074 enssdom 6178 fiprc 6228 ltexprlemlol 6576 ltexprlemupu 6578 recexgt0 7364 peano2uz2 8121 eluzp1p1 8274 peano2uz 8302 zq 8337 elfzmlbmOLD 8759 ubmelfzo 8826 frecuzrdgfn 8879 expclzaplem 8933 bj-indint 9390 peano5setOLD 9400 |
Copyright terms: Public domain | W3C validator |