|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > imim1i | Structured version Visualization version GIF version | ||
| Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 83. Its associated inference is syl 17. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.) | 
| Ref | Expression | 
|---|---|
| imim1i.1 | ⊢ (𝜑 → 𝜓) | 
| Ref | Expression | 
|---|---|
| imim1i | ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | imim1i.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | id 22 | . 2 ⊢ (𝜒 → 𝜒) | |
| 3 | 1, 2 | imim12i 62 | 1 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 | 
| This theorem is referenced by: jarr 106 jarl 125 impt 178 pm3.41 492 pm3.42 493 pm2.67-2 891 jaob 963 3jaobOLD 1428 merco1 1712 19.21v 1938 19.39 1983 moimi 2544 r19.30OLD 3120 r19.37 3261 axrep2 5281 axprlem4 5425 dmcosseq 5986 dmcosseqOLD 5987 fliftfun 7333 tz7.48lem 8482 ssfi 9214 ac6sfi 9321 frfi 9322 domunfican 9362 iunfi 9384 finsschain 9400 cantnfval2 9710 cantnflt 9713 cnfcom 9741 kmlem1 10192 kmlem13 10204 axpowndlem2 10639 wunfi 10762 ingru 10856 xrub 13355 hashf1lem2 14496 caubnd 15398 fsum2d 15808 fsumabs 15838 fsumrlim 15848 fsumo1 15849 fsumiun 15858 fprod2d 16018 ablfac1eulem 20093 mplcoe1 22056 mplcoe5 22059 mdetunilem9 22627 t1t0 23357 fiuncmp 23413 ptcmpfi 23822 isfil2 23865 fsumcn 24895 ovolfiniun 25537 finiunmbl 25580 volfiniun 25583 itgfsum 25863 dvmptfsum 26014 pntrsumbnd 27611 mulsproplem12 28154 mulsproplem13 28155 mulsproplem14 28156 nmounbseqi 30797 nmounbseqiALT 30798 isch3 31261 dmdmd 32320 mdslmd1lem2 32346 sumdmdi 32440 dmdbr4ati 32441 dmdbr6ati 32443 gsumle 33102 gsumvsca1 33233 gsumvsca2 33234 pwsiga 34132 bnj1533 34867 bnj110 34873 bnj1523 35086 dfon2lem8 35792 meran1 36413 bj-stabpeirce 36556 bj-bi3ant 36591 bj-ssbid2ALT 36665 bj-spnfw 36672 bj-spst 36691 bj-19.23bit 36693 wl-syls2 37511 heibor1lem 37817 isltrn2N 40123 cdlemefrs32fva 40403 fiinfi 43591 con3ALT2 44555 alrim3con13v 44558 islinindfis 48371 setrec1lem4 49264 | 
| Copyright terms: Public domain | W3C validator |