Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3imtr4i | Structured version Visualization version GIF version |
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-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 206 | . 2 ⊢ (𝜒 → 𝜓) |
4 | 3imtr4.3 | . 2 ⊢ (𝜃 ↔ 𝜓) | |
5 | 3, 4 | sylibr 223 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: hbxfrbi 1742 nfnt 1767 sbimi 1873 ralimi2 2933 reximi2 2993 r19.28v 3053 r19.29r 3055 r19.30 3063 elex 3185 rmoan 3373 rmoimi2 3376 sseq2 3590 rabss2 3648 undif4 3987 r19.2zb 4013 ralf0OLD 4031 difprsnss 4270 snsspw 4315 uniin 4393 iuniin 4467 iuneq1 4470 iuneq2 4473 iunpwss 4551 eunex 4785 rmorabex 4855 exss 4858 pwunss 4943 soeq2 4979 elopaelxp 5114 reliin 5163 coeq1 5201 coeq2 5202 cnveq 5218 dmeq 5246 dmin 5254 dmcoss 5306 rncoeq 5310 dminss 5466 imainss 5467 dfco2a 5552 iotaex 5785 fundif 5849 fununi 5878 fof 6028 f1ocnv 6062 foco2 6287 isocnv 6480 isotr 6486 oprabid 6576 resiexg 6994 zfrep6 7027 ovmptss 7145 dmtpos 7251 tposfn 7268 smores 7336 omopthlem1 7622 eqer 7664 eqerOLD 7665 ixpeq2 7808 enssdom 7866 fiprc 7924 sbthlem9 7963 infensuc 8023 fipwuni 8215 zfregOLD 8385 zfreg2OLD 8386 dfom3 8427 r1elss 8552 scott0 8632 fin56 9098 dominf 9150 ac6n 9190 brdom4 9233 dominfac 9274 inawina 9391 eltsk2g 9452 ltsosr 9794 ssxr 9986 recgt0ii 10808 sup2 10858 dfnn2 10910 peano2uz2 11341 eluzp1p1 11589 peano2uz 11617 zq 11670 ubmelfzo 12400 expclzlem 12746 wrdeq 13182 wwlktovf 13547 fsum2dlem 14343 fprod2dlem 14549 sin02gt0 14761 divalglem6 14959 qredeu 15210 isfunc 16347 xpcbas 16641 drsdirfi 16761 clatl 16939 tsrss 17046 gimcnv 17532 gsum2dlem1 18192 gsum2dlem2 18193 lmimcnv 18888 xrge0subm 19606 fctop 20618 cctop 20620 alexsubALTlem4 21664 lpbl 22118 xrge0gsumle 22444 xrge0tsms 22445 iirev 22536 iihalf1 22538 iihalf2 22540 iimulcl 22544 vitalilem1 23182 vitalilem1OLD 23183 ply1idom 23688 aacjcl 23886 aannenlem2 23888 ang180lem4 24342 lgslem3 24824 axlowdim 25641 axcontlem2 25645 usgraexmplef 25929 nmobndseqi 27018 axhcompl-zf 27239 hhcmpl 27441 shunssi 27611 spansni 27800 pjoml3i 27829 cmcmlem 27834 nonbooli 27894 lnopco0i 28247 pjnmopi 28391 pjnormssi 28411 hatomistici 28605 cvexchi 28612 cmdmdi 28660 mddmdin0i 28674 cdj3lem3b 28683 disjin 28781 disjin2 28782 xrge0tsmsd 29116 issgon 29513 sxbrsigalem0 29660 eulerpartlemgs2 29769 ballotlem2 29877 ballotth 29926 bnj945 30098 bnj556 30224 bnj557 30225 bnj607 30240 bnj864 30246 bnj969 30270 bnj999 30281 bnj1398 30356 elpotr 30930 dfon2lem8 30939 sltval2 31053 txpss3v 31155 meran1 31580 arg-ax 31585 bj-nfalt 31889 bj-eunex 31987 poimirlem25 32604 poimirlem30 32609 bndss 32755 fldcrng 32973 flddmn 33027 prter1 33182 mzpclall 36308 setindtrs 36610 dgraalem 36734 ifpimim 36873 inintabss 36903 refimssco 36932 cotrintab 36940 intimass 36965 psshepw 37102 nzin 37539 axc11next 37629 iotaexeu 37641 hbexgVD 38164 reuan 39829 aovpcov0 39919 aov0ov0 39922 enege 40096 onego 40097 gboagbo 40178 n0rex 40310 elfzlmr 40366 cusgrop 40660 rusgrpropedg 40784 wwlksn0 41059 mhmismgmhm 41596 sgrpplusgaopALT 41621 rhmisrnghm 41710 srhmsubclem1 41865 srhmsubcALTVlem1 41884 rhmsubcALTVlem3 41899 eluz2cnn0n1 42095 regt1loggt0 42128 rege1logbrege0 42150 rege1logbzge0 42151 relogbmulbexp 42153 |
Copyright terms: Public domain | W3C validator |