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  jarl  123  impt  170  pm3.41  482  pm3.42  483  pm2.67-2  907  jaob  975  3jaob  1544  merco1  1793  19.21v  2031  19.39  2079  r19.37  3274  axrep2  4967  dmcosseq  5588  fliftfun  6782  tz7.48lem  7768  ac6sfi  8439  frfi  8440  domunfican  8468  iunfi  8489  finsschain  8508  cantnfval2  8809  cantnflt  8812  cnfcom  8840  kmlem1  9253  kmlem13  9265  axpowndlem2  9701  wunfi  9824  ingru  9918  xrub  12356  hashf1lem2  13453  caubnd  14317  fsum2d  14721  fsumabs  14751  fsumrlim  14761  fsumo1  14762  fsumiun  14771  fprod2d  14928  ablfac1eulem  18669  mplcoe1  19670  mplcoe5  19673  mdetunilem9  20633  t1t0  21362  fiuncmp  21417  ptcmpfi  21826  isfil2  21869  fsumcn  22882  ovolfiniun  23478  finiunmbl  23521  volfiniun  23524  itgfsum  23803  dvmptfsum  23948  pntrsumbnd  25465  nmounbseqi  27956  nmounbseqiALT  27957  isch3  28422  dmdmd  29483  mdslmd1lem2  29509  sumdmdi  29603  dmdbr4ati  29604  dmdbr6ati  29606  gsumle  30100  gsumvsca1  30103  gsumvsca2  30104  pwsiga  30514  bnj1533  31240  bnj110  31246  bnj1523  31457  dfon2lem8  32010  meran1  32722  bj-bi3ant  32884  bj-ssbid2ALT  32956  bj-spnfw  32968  bj-spst  32989  bj-19.23bit  32991  bj-axrep2  33098  wl-syls2  33603  heibor1lem  33914  isltrn2N  35895  cdlemefrs32fva  36175  fiinfi  38372  con3ALT2  39228  alrim3con13v  39235  islinindfis  42800  setrec1lem4  42999
  Copyright terms: Public domain W3C validator