![]() |
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 120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3imtr4.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | sylibr 133 |
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 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: dcn 810 stdcn 815 dcan 899 xordc1 1352 hbxfrbi 1429 nfalt 1538 19.29r 1581 19.31r 1640 sbimi 1718 spsbbi 1796 sbi2v 1844 euan 2029 2exeu 2065 ralimi2 2464 reximi2 2500 r19.28av 2540 r19.29r 2542 elex 2666 rmoan 2851 rmoimi2 2854 sseq2 3085 rabss2 3144 unssdif 3275 inssdif 3276 unssin 3279 inssun 3280 rabn0r 3353 undif4 3389 ssdif0im 3391 inssdif0im 3394 ssundifim 3410 ralf0 3430 prmg 3608 difprsnss 3622 snsspw 3655 pwprss 3696 pwtpss 3697 uniin 3720 intss 3756 iuniin 3787 iuneq1 3790 iuneq2 3793 iundif2ss 3842 iinuniss 3859 iunpwss 3868 intexrabim 4036 exmidundif 4087 exmidundifim 4088 exss 4107 pwunss 4163 soeq2 4196 ordunisuc2r 4388 peano5 4470 reliin 4619 coeq1 4654 coeq2 4655 cnveq 4671 dmeq 4697 dmin 4705 dmcoss 4764 rncoeq 4768 resiexg 4820 dminss 4909 imainss 4910 dfco2a 4995 euiotaex 5060 fununi 5147 fof 5301 f1ocnv 5334 rexrnmpt 5515 isocnv 5664 isotr 5669 oprabid 5755 dmtpos 6105 tposfn 6122 smores 6141 eqer 6413 ixpeq2 6558 enssdom 6608 fiprc 6661 fiintim 6768 ltexprlemlol 7352 ltexprlemupu 7354 recexgt0 8254 peano2uz2 9056 eluzp1p1 9247 peano2uz 9274 zq 9314 ubmelfzo 9864 frecuzrdgtcl 10072 frecuzrdgfunlem 10079 expclzaplem 10204 hashfiv01gt1 10415 fsum2dlemstep 11089 sin02gt0 11315 qredeu 11618 bj-stim 12637 bj-stan 12638 bj-stal 12640 bj-nfalt 12655 bj-indint 12812 |
Copyright terms: Public domain | W3C validator |