Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim1i Structured version   Visualization version   GIF version

Theorem imim1i 63
 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.)
Hypothesis
Ref Expression
imim1i.1 (𝜑𝜓)
Assertion
Ref Expression
imim1i ((𝜓𝜒) → (𝜑𝜒))

Proof of Theorem imim1i
StepHypRef Expression
1 imim1i.1 . 2 (𝜑𝜓)
2 id 22 . 2 (𝜒𝜒)
31, 2imim12i 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  889  jaob  959  3jaob  1423  merco1  1715  19.21v  1940  19.39  1991  moimi  2603  r19.30  3293  r19.37  3297  axrep2  5157  dmcosseq  5809  fliftfun  7044  tz7.48lem  8062  ac6sfi  8748  frfi  8749  domunfican  8777  iunfi  8798  finsschain  8817  cantnfval2  9118  cantnflt  9121  cnfcom  9149  kmlem1  9563  kmlem13  9575  axpowndlem2  10011  wunfi  10134  ingru  10228  xrub  12695  hashf1lem2  13812  caubnd  14712  fsum2d  15120  fsumabs  15150  fsumrlim  15160  fsumo1  15161  fsumiun  15170  fprod2d  15329  ablfac1eulem  19190  mplcoe1  20709  mplcoe5  20712  mdetunilem9  21232  t1t0  21960  fiuncmp  22016  ptcmpfi  22425  isfil2  22468  fsumcn  23482  ovolfiniun  24112  finiunmbl  24155  volfiniun  24158  itgfsum  24437  dvmptfsum  24585  pntrsumbnd  26157  nmounbseqi  28567  nmounbseqiALT  28568  isch3  29031  dmdmd  30090  mdslmd1lem2  30116  sumdmdi  30210  dmdbr4ati  30211  dmdbr6ati  30213  gsumle  30782  gsumvsca1  30911  gsumvsca2  30912  pwsiga  31511  bnj1533  32246  bnj110  32252  bnj1523  32465  dfon2lem8  33160  meran1  33884  bj-stabpeirce  34018  bj-bi3ant  34052  bj-ssbid2ALT  34125  bj-spnfw  34132  bj-spst  34152  bj-19.23bit  34154  wl-syls2  34930  heibor1lem  35263  isltrn2N  37432  cdlemefrs32fva  37712  fiinfi  40287  con3ALT2  41251  alrim3con13v  41254  islinindfis  44872  setrec1lem4  45234
 Copyright terms: Public domain W3C validator