![]() |
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 1426 merco1 1710 19.21v 1937 19.39 1982 moimi 2543 r19.30OLD 3119 r19.37 3260 axrep2 5288 axprlem4 5432 dmcosseq 5990 dmcosseqOLD 5991 fliftfun 7332 tz7.48lem 8480 ssfi 9212 ac6sfi 9318 frfi 9319 domunfican 9359 iunfi 9381 finsschain 9397 cantnfval2 9707 cantnflt 9710 cnfcom 9738 kmlem1 10189 kmlem13 10201 axpowndlem2 10636 wunfi 10759 ingru 10853 xrub 13351 hashf1lem2 14492 caubnd 15394 fsum2d 15804 fsumabs 15834 fsumrlim 15844 fsumo1 15845 fsumiun 15854 fprod2d 16014 ablfac1eulem 20107 mplcoe1 22073 mplcoe5 22076 mdetunilem9 22642 t1t0 23372 fiuncmp 23428 ptcmpfi 23837 isfil2 23880 fsumcn 24908 ovolfiniun 25550 finiunmbl 25593 volfiniun 25596 itgfsum 25877 dvmptfsum 26028 pntrsumbnd 27625 mulsproplem12 28168 mulsproplem13 28169 mulsproplem14 28170 nmounbseqi 30806 nmounbseqiALT 30807 isch3 31270 dmdmd 32329 mdslmd1lem2 32355 sumdmdi 32449 dmdbr4ati 32450 dmdbr6ati 32452 gsumle 33084 gsumvsca1 33215 gsumvsca2 33216 pwsiga 34111 bnj1533 34845 bnj110 34851 bnj1523 35064 dfon2lem8 35772 meran1 36394 bj-stabpeirce 36537 bj-bi3ant 36572 bj-ssbid2ALT 36646 bj-spnfw 36653 bj-spst 36672 bj-19.23bit 36674 wl-syls2 37490 heibor1lem 37796 isltrn2N 40103 cdlemefrs32fva 40383 fiinfi 43563 con3ALT2 44528 alrim3con13v 44531 islinindfis 48295 setrec1lem4 48921 |
Copyright terms: Public domain | W3C validator |