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

Theorem imim1i 60
Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 80. 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 59 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  103  impt  167  jarl  173  pm2.67-2  415  pm3.41  579  pm3.42  580  jaob  817  3jaob  1381  merco1  1628  19.21v  1853  19.39  1884  r19.37  3062  axrep2  4691  dmcosseq  5291  fliftfun  6436  tz7.48lem  7396  ac6sfi  8062  frfi  8063  domunfican  8091  iunfi  8110  finsschain  8129  cantnfval2  8422  cantnflt  8425  cnfcom  8453  kmlem1  8828  kmlem13  8840  axpowndlem2  9272  wunfi  9395  ingru  9489  xrub  11966  hashf1lem2  13045  caubnd  13888  fsum2d  14286  fsumabs  14316  fsumrlim  14326  fsumo1  14327  fsumiun  14336  fprod2d  14492  ablfac1eulem  18236  mplcoe1  19228  mplcoe5  19231  mdetunilem9  20183  t1t0  20900  fiuncmp  20955  ptcmpfi  21364  isfil2  21408  fsumcn  22408  ovolfiniun  22989  finiunmbl  23032  volfiniun  23035  itgfsum  23312  dvmptfsum  23455  pntrsumbnd  24968  nbgraf1olem1  25732  nmounbseqi  26818  nmounbseqiALT  26819  isch3  27284  dmdmd  28345  mdslmd1lem2  28371  sumdmdi  28465  dmdbr4ati  28466  dmdbr6ati  28468  gsumle  28912  gsumvsca1  28915  gsumvsca2  28916  pwsiga  29322  bnj1533  29978  bnj110  29984  bnj1523  30195  dfon2lem8  30741  meran1  31382  bj-bi3ant  31549  bj-ssbid2ALT  31637  bj-spnfw  31647  bj-spst  31668  bj-19.23bit  31670  bj-axrep2  31786  wl-syls2  32270  heibor1lem  32577  isltrn2N  34223  cdlemefrs32fva  34505  fiinfi  36696  con3ALT2  37556  alrim3con13v  37563  islinindfis  42030
  Copyright terms: Public domain W3C validator