![]() |
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 121 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3imtr4.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | sylibr 134 |
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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: dcn 843 stdcn 848 xordc1 1404 hbxfrbi 1483 nfalt 1589 19.29r 1632 19.31r 1692 sbimi 1775 spsbbi 1855 sbi2v 1904 euan 2098 2exeu 2134 ralimi2 2554 reximi2 2590 r19.28av 2630 r19.29r 2632 elex 2771 rmoan 2961 rmoimi2 2964 sseq2 3204 rabss2 3263 unssdif 3395 inssdif 3396 unssin 3399 inssun 3400 rabn0r 3474 undif4 3510 ssdif0im 3512 inssdif0im 3515 ssundifim 3531 ralf0 3550 prmg 3740 difprsnss 3757 snsspw 3791 pwprss 3832 pwtpss 3833 uniin 3856 intss 3892 iuniin 3923 iuneq1 3926 iuneq2 3929 iundif2ss 3979 iinuniss 3996 iunpwss 4005 intexrabim 4183 exmidundif 4236 exmidundifim 4237 exss 4257 pwunss 4315 soeq2 4348 ordunisuc2r 4547 peano5 4631 reliin 4782 coeq1 4820 coeq2 4821 cnveq 4837 dmeq 4863 dmin 4871 dmcoss 4932 rncoeq 4936 resiexg 4988 dminss 5081 imainss 5082 dfco2a 5167 euiotaex 5232 eliotaeu 5244 fununi 5323 fof 5477 f1ocnv 5514 rexrnmpt 5702 isocnv 5855 isotr 5860 oprabid 5951 dmtpos 6311 tposfn 6328 smores 6347 eqer 6621 ixpeq2 6768 enssdom 6818 fiprc 6871 fiintim 6987 ltexprlemlol 7664 ltexprlemupu 7666 recexgt0 8601 peano2uz2 9427 eluzp1p1 9621 peano2uz 9651 zq 9694 ubmelfzo 10270 frecuzrdgtcl 10486 frecuzrdgfunlem 10493 expclzaplem 10637 hashfiv01gt1 10856 wrdeq 10939 fsum2dlemstep 11580 fprod2dlemstep 11768 sin02gt0 11910 qredeu 12238 prmdc 12271 subrngrng 13701 lgslem3 15159 bj-stim 15308 bj-stan 15309 bj-stal 15311 bj-nfalt 15326 bj-indint 15493 tridceq 15616 |
Copyright terms: Public domain | W3C validator |