![]() |
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 746 dcan 842 xordc1 1284 hbxfrbi 1361 nfalt 1470 19.29r 1512 19.31r 1571 sbimi 1647 spsbbi 1725 sbi2v 1772 euan 1956 2exeu 1992 ralimi2 2381 reximi2 2415 r19.28av 2449 r19.29r 2451 elex 2566 rmoan 2739 rmoimi2 2742 sseq2 2967 rabss2 3023 unssdif 3172 inssdif 3173 unssin 3176 inssun 3177 rabn0r 3244 undif4 3284 ssdif0im 3286 inssdif0im 3291 ssundifim 3306 ralf0 3324 prmg 3489 difprsnss 3502 snsspw 3535 pwprss 3576 pwtpss 3577 uniin 3600 intss 3636 iuniin 3667 iuneq1 3670 iuneq2 3673 iundif2ss 3722 iinuniss 3737 iunpwss 3743 intexrabim 3907 exss 3963 pwunss 4020 soeq2 4053 ordunisuc2r 4240 peano5 4321 reliin 4459 coeq1 4493 coeq2 4494 cnveq 4509 dmeq 4535 dmin 4543 dmcoss 4601 rncoeq 4605 resiexg 4653 dminss 4738 imainss 4739 dfco2a 4821 euiotaex 4883 fununi 4967 fof 5106 f1ocnv 5139 rexrnmpt 5310 isocnv 5451 isotr 5456 oprabid 5537 dmtpos 5871 tposfn 5888 smores 5907 eqer 6138 enssdom 6242 fiprc 6292 ltexprlemlol 6700 ltexprlemupu 6702 recexgt0 7571 peano2uz2 8345 eluzp1p1 8498 peano2uz 8526 zq 8561 elfzmlbmOLD 8989 ubmelfzo 9056 frecuzrdgfn 9198 expclzaplem 9279 bj-indint 10055 peano5setOLD 10065 |
Copyright terms: Public domain | W3C validator |