![]() |
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 209 | . 2 ⊢ (𝜒 → 𝜓) |
4 | 3imtr4.3 | . 2 ⊢ (𝜃 ↔ 𝜓) | |
5 | 3, 4 | sylibr 226 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: hbxfrbi 1868 sbimi 2017 nexmo 2552 moimi 2557 eu6im 2593 ralimi2 3131 reximi2 3191 r19.28v 3257 r19.29r 3259 r19.30 3268 elex 3414 rmoan 3620 rmoimi2 3623 sseq2 3846 rabss2 3906 n0rex 4163 undif4 4259 r19.2zb 4284 difprsnss 4563 snsspw 4606 uniin 4695 iuniin 4766 iuneq1 4769 iuneq2 4772 iunpwss 4854 eunex 5103 eunexOLD 5104 rmorabex 5162 exss 5165 pwunss 5258 soeq2 5297 elopaelxp 5441 reliin 5490 coeq1 5527 coeq2 5528 cnveq 5543 dmeq 5571 dmin 5579 dmcoss 5633 rncoeq 5637 dminss 5803 imainss 5804 dfco2a 5891 iotaex 6118 fundif 6185 fununi 6211 fof 6368 f1ocnv 6405 foco2 6645 isocnv 6854 isotr 6860 oprabid 6955 zfrep6 7415 ovmptss 7541 dmtpos 7648 tposfn 7665 smores 7734 omopthlem1 8021 eqer 8063 ixpeq2 8210 enssdom 8268 fiprc 8329 sbthlem9 8368 infensuc 8428 fipwuni 8622 dfom3 8843 r1elss 8968 scott0 9048 fin56 9552 dominf 9604 ac6n 9644 brdom4 9689 dominfac 9732 inawina 9849 eltsk2g 9910 ltsosr 10253 ssxr 10448 recgt0ii 11285 sup2 11337 dfnn2 11393 peano2uz2 11821 eluzp1p1 12022 peano2uz 12051 zqOLD 12106 ubmelfzo 12856 elfzlmr 12905 expclzlem 13206 wrdeq 13628 wwlktovf 14112 fsum2dlem 14910 fprod2dlem 15117 sin02gt0 15328 divalglem6 15532 qredeu 15781 isfunc 16913 xpcbas 17208 drsdirfi 17328 clatl 17506 tsrss 17613 gimcnv 18097 gsum2dlem1 18759 gsum2dlem2 18760 lmimcnv 19466 xrge0subm 20187 fctop 21220 cctop 21222 alexsubALTlem4 22266 lpbl 22720 xrge0gsumle 23048 xrge0tsms 23049 iirev 23140 iihalf1 23142 iihalf2 23144 iimulcl 23148 vitalilem1 23816 ply1idom 24325 aacjcl 24523 aannenlem2 24525 ang180lem4 24994 lgslem3 25480 tgjustf 25828 axlowdim 26314 axcontlem2 26318 usgrexmplef 26610 cusgrop 26790 rusgrpropedg 26936 spthispth 27082 cycliscrct 27155 wwlksn0 27216 clwwlkccat 27374 clwwlkn 27419 clwwlknonccat 27502 numclwwlk1 27788 nmobndseqi 28210 axhcompl-zf 28431 hhcmpl 28633 shunssi 28803 spansni 28992 pjoml3i 29021 cmcmlem 29026 nonbooli 29086 lnopco0i 29439 pjnmopi 29583 pjnormssi 29603 hatomistici 29797 cvexchi 29804 cmdmdi 29852 mddmdin0i 29866 cdj3lem3b 29875 disjin 29966 disjin2 29967 xrge0tsmsd 30351 issgon 30788 sxbrsigalem0 30935 eulerpartlemgs2 31044 ballotlem2 31153 ballotth 31202 bnj945 31447 bnj556 31573 bnj557 31574 bnj607 31589 bnj864 31595 bnj969 31619 bnj999 31630 bnj1398 31705 elpotr 32278 dfon2lem8 32287 sltval2 32402 txpss3v 32578 meran1 32997 arg-ax 33002 bj-nfalt 33294 bj-eunex 33379 wl-cbvmotv 33894 poimirlem25 34065 poimirlem30 34070 bndss 34214 fldcrng 34432 flddmn 34486 xrnss3v 34767 redss3 35002 redpim3 35004 prter1 35038 mzpclall 38260 setindtrs 38561 dgraalem 38684 ifpimim 38822 inintabss 38851 refimssco 38880 cotrintab 38888 intimass 38913 psshepw 39048 nzin 39483 axc11next 39572 iotaexeu 39584 hbexgVD 40085 reuan 42148 aovpcov0 42241 aov0ov0 42244 spr0el 42431 sprsymrelf 42444 enege 42593 onego 42594 gbogbow 42679 mhmismgmhm 42831 sgrpplusgaopALT 42856 rhmisrnghm 42945 srhmsubclem1 43098 rhmsubcALTVlem3 43131 eluz2cnn0n1 43326 regt1loggt0 43355 rege1logbrege0 43377 rege1logbzge0 43378 relogbmulbexp 43380 |
Copyright terms: Public domain | W3C validator |