![]() |
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 494 pm3.42 495 pm2.67-2 891 jaob 961 3jaob 1427 merco1 1716 19.21v 1943 19.39 1989 moimi 2540 r19.30OLD 3122 r19.37 3260 axrep2 5284 dmcosseq 5967 fliftfun 7296 tz7.48lem 8428 ssfi 9161 ac6sfi 9275 frfi 9276 domunfican 9308 iunfi 9328 finsschain 9347 cantnfval2 9651 cantnflt 9654 cnfcom 9682 kmlem1 10132 kmlem13 10144 axpowndlem2 10580 wunfi 10703 ingru 10797 xrub 13278 hashf1lem2 14404 caubnd 15292 fsum2d 15704 fsumabs 15734 fsumrlim 15744 fsumo1 15745 fsumiun 15754 fprod2d 15912 ablfac1eulem 19925 mplcoe1 21560 mplcoe5 21563 mdetunilem9 22091 t1t0 22821 fiuncmp 22877 ptcmpfi 23286 isfil2 23329 fsumcn 24355 ovolfiniun 24987 finiunmbl 25030 volfiniun 25033 itgfsum 25313 dvmptfsum 25461 pntrsumbnd 27036 mulsproplem12 27550 mulsproplem13 27551 mulsproplem14 27552 nmounbseqi 29995 nmounbseqiALT 29996 isch3 30459 dmdmd 31518 mdslmd1lem2 31544 sumdmdi 31638 dmdbr4ati 31639 dmdbr6ati 31641 gsumle 32213 gsumvsca1 32342 gsumvsca2 32343 pwsiga 33059 bnj1533 33794 bnj110 33800 bnj1523 34013 dfon2lem8 34693 meran1 35201 bj-stabpeirce 35335 bj-bi3ant 35372 bj-ssbid2ALT 35445 bj-spnfw 35452 bj-spst 35472 bj-19.23bit 35474 wl-syls2 36283 heibor1lem 36583 isltrn2N 38897 cdlemefrs32fva 39177 fiinfi 42195 con3ALT2 43162 alrim3con13v 43165 islinindfis 46970 setrec1lem4 47575 |
Copyright terms: Public domain | W3C validator |