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 181 pm3.41 496 pm3.42 497 pm2.67-2 892 jaob 962 3jaob 1428 merco1 1721 19.21v 1947 19.39 1993 moimi 2544 r19.30 3253 r19.37 3257 axrep2 5182 dmcosseq 5842 fliftfun 7121 tz7.48lem 8177 ssfi 8851 ac6sfi 8915 frfi 8916 domunfican 8944 iunfi 8964 finsschain 8983 cantnfval2 9284 cantnflt 9287 cnfcom 9315 kmlem1 9764 kmlem13 9776 axpowndlem2 10212 wunfi 10335 ingru 10429 xrub 12902 hashf1lem2 14022 caubnd 14922 fsum2d 15335 fsumabs 15365 fsumrlim 15375 fsumo1 15376 fsumiun 15385 fprod2d 15543 ablfac1eulem 19459 mplcoe1 20994 mplcoe5 20997 mdetunilem9 21517 t1t0 22245 fiuncmp 22301 ptcmpfi 22710 isfil2 22753 fsumcn 23767 ovolfiniun 24398 finiunmbl 24441 volfiniun 24444 itgfsum 24724 dvmptfsum 24872 pntrsumbnd 26447 nmounbseqi 28858 nmounbseqiALT 28859 isch3 29322 dmdmd 30381 mdslmd1lem2 30407 sumdmdi 30501 dmdbr4ati 30502 dmdbr6ati 30504 gsumle 31069 gsumvsca1 31198 gsumvsca2 31199 pwsiga 31810 bnj1533 32545 bnj110 32551 bnj1523 32764 dfon2lem8 33485 meran1 34337 bj-stabpeirce 34471 bj-bi3ant 34508 bj-ssbid2ALT 34581 bj-spnfw 34588 bj-spst 34608 bj-19.23bit 34610 wl-syls2 35405 heibor1lem 35704 isltrn2N 37871 cdlemefrs32fva 38151 fiinfi 40856 con3ALT2 41823 alrim3con13v 41826 islinindfis 45463 setrec1lem4 46067 |
Copyright terms: Public domain | W3C validator |