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  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