Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3imtr4i | GIF 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: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: dcn 812 stdcn 817 dcan 903 xordc1 1356 hbxfrbi 1433 nfalt 1542 19.29r 1585 19.31r 1644 sbimi 1722 spsbbi 1800 sbi2v 1848 euan 2033 2exeu 2069 ralimi2 2469 reximi2 2505 r19.28av 2545 r19.29r 2547 elex 2671 rmoan 2857 rmoimi2 2860 sseq2 3091 rabss2 3150 unssdif 3281 inssdif 3282 unssin 3285 inssun 3286 rabn0r 3359 undif4 3395 ssdif0im 3397 inssdif0im 3400 ssundifim 3416 ralf0 3436 prmg 3614 difprsnss 3628 snsspw 3661 pwprss 3702 pwtpss 3703 uniin 3726 intss 3762 iuniin 3793 iuneq1 3796 iuneq2 3799 iundif2ss 3848 iinuniss 3865 iunpwss 3874 intexrabim 4048 exmidundif 4099 exmidundifim 4100 exss 4119 pwunss 4175 soeq2 4208 ordunisuc2r 4400 peano5 4482 reliin 4631 coeq1 4666 coeq2 4667 cnveq 4683 dmeq 4709 dmin 4717 dmcoss 4778 rncoeq 4782 resiexg 4834 dminss 4923 imainss 4924 dfco2a 5009 euiotaex 5074 fununi 5161 fof 5315 f1ocnv 5348 rexrnmpt 5531 isocnv 5680 isotr 5685 oprabid 5771 dmtpos 6121 tposfn 6138 smores 6157 eqer 6429 ixpeq2 6574 enssdom 6624 fiprc 6677 fiintim 6785 ltexprlemlol 7378 ltexprlemupu 7380 recexgt0 8310 peano2uz2 9126 eluzp1p1 9319 peano2uz 9346 zq 9386 ubmelfzo 9945 frecuzrdgtcl 10153 frecuzrdgfunlem 10160 expclzaplem 10285 hashfiv01gt1 10496 fsum2dlemstep 11171 sin02gt0 11397 qredeu 11705 bj-stim 12881 bj-stan 12882 bj-stal 12884 bj-nfalt 12898 bj-indint 13056 |
Copyright terms: Public domain | W3C validator |