MPE Home 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  impt  169  jarl  175  pm2.67-2  417  pm3.41  581  pm3.42  582  jaob  821  3jaob  1387  merco1  1635  19.21v  1865  19.39  1896  r19.37  3080  axrep2  4743  dmcosseq  5357  fliftfun  6527  tz7.48lem  7496  ac6sfi  8164  frfi  8165  domunfican  8193  iunfi  8214  finsschain  8233  cantnfval2  8526  cantnflt  8529  cnfcom  8557  kmlem1  8932  kmlem13  8944  axpowndlem2  9380  wunfi  9503  ingru  9597  xrub  12101  hashf1lem2  13194  caubnd  14048  fsum2d  14449  fsumabs  14479  fsumrlim  14489  fsumo1  14490  fsumiun  14499  fprod2d  14655  ablfac1eulem  18411  mplcoe1  19405  mplcoe5  19408  mdetunilem9  20366  t1t0  21092  fiuncmp  21147  ptcmpfi  21556  isfil2  21600  fsumcn  22613  ovolfiniun  23209  finiunmbl  23252  volfiniun  23255  itgfsum  23533  dvmptfsum  23676  pntrsumbnd  25189  nmounbseqi  27520  nmounbseqiALT  27521  isch3  27986  dmdmd  29047  mdslmd1lem2  29073  sumdmdi  29167  dmdbr4ati  29168  dmdbr6ati  29170  gsumle  29606  gsumvsca1  29609  gsumvsca2  29610  pwsiga  30016  bnj1533  30683  bnj110  30689  bnj1523  30900  dfon2lem8  31449  meran1  32105  bj-bi3ant  32269  bj-ssbid2ALT  32341  bj-spnfw  32353  bj-spst  32374  bj-19.23bit  32376  bj-axrep2  32485  wl-syls2  32963  heibor1lem  33279  isltrn2N  34925  cdlemefrs32fva  35207  fiinfi  37398  con3ALT2  38257  alrim3con13v  38264  islinindfis  41556  setrec1lem4  41760
  Copyright terms: Public domain W3C validator