![]() |
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 2544 r19.30OLD 3125 r19.37 3248 axrep2 5250 dmcosseq 5933 fliftfun 7262 tz7.48lem 8392 ssfi 9124 ac6sfi 9238 frfi 9239 domunfican 9271 iunfi 9291 finsschain 9310 cantnfval2 9612 cantnflt 9615 cnfcom 9643 kmlem1 10093 kmlem13 10105 axpowndlem2 10541 wunfi 10664 ingru 10758 xrub 13238 hashf1lem2 14362 caubnd 15250 fsum2d 15663 fsumabs 15693 fsumrlim 15703 fsumo1 15704 fsumiun 15713 fprod2d 15871 ablfac1eulem 19858 mplcoe1 21454 mplcoe5 21457 mdetunilem9 21985 t1t0 22715 fiuncmp 22771 ptcmpfi 23180 isfil2 23223 fsumcn 24249 ovolfiniun 24881 finiunmbl 24924 volfiniun 24927 itgfsum 25207 dvmptfsum 25355 pntrsumbnd 26930 nmounbseqi 29761 nmounbseqiALT 29762 isch3 30225 dmdmd 31284 mdslmd1lem2 31310 sumdmdi 31404 dmdbr4ati 31405 dmdbr6ati 31407 gsumle 31974 gsumvsca1 32103 gsumvsca2 32104 pwsiga 32769 bnj1533 33504 bnj110 33510 bnj1523 33723 dfon2lem8 34404 meran1 34912 bj-stabpeirce 35046 bj-bi3ant 35083 bj-ssbid2ALT 35156 bj-spnfw 35163 bj-spst 35183 bj-19.23bit 35185 wl-syls2 35997 heibor1lem 36297 isltrn2N 38612 cdlemefrs32fva 38892 fiinfi 41919 con3ALT2 42886 alrim3con13v 42889 islinindfis 46604 setrec1lem4 47209 |
Copyright terms: Public domain | W3C validator |