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

Step	Hyp	Ref	Expression
1		imim1i.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 22	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	imim12i 62	1 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

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  492  pm3.42  493  pm2.67-2  891  jaob  963  3jaobOLD  1429  merco1  1713  19.21v  1939  19.39  1990  moimi  2538  r19.37  3240  axrep2  5237  axprlem4  5381  dmcosseq  5940  dmcosseqOLD  5941  fliftfun  7287  tz7.48lem  8409  ssfi  9137  ac6sfi  9231  frfi  9232  domunfican  9272  iunfi  9294  finsschain  9310  cantnfval2  9622  cantnflt  9625  cnfcom  9653  kmlem1  10104  kmlem13  10116  axpowndlem2  10551  wunfi  10674  ingru  10768  xrub  13272  hashf1lem2  14421  caubnd  15325  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  fprod2d  15947  ablfac1eulem  20004  mplcoe1  21944  mplcoe5  21947  mdetunilem9  22507  t1t0  23235  fiuncmp  23291  ptcmpfi  23700  isfil2  23743  fsumcn  24761  ovolfiniun  25402  finiunmbl  25445  volfiniun  25448  itgfsum  25728  dvmptfsum  25879  pntrsumbnd  27477  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  nmounbseqi  30706  nmounbseqiALT  30707  isch3  31170  dmdmd  32229  mdslmd1lem2  32255  sumdmdi  32349  dmdbr4ati  32350  dmdbr6ati  32352  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  pwsiga  34120  bnj1533  34842  bnj110  34848  bnj1523  35061  dfon2lem8  35778  meran1  36399  bj-stabpeirce  36542  bj-bi3ant  36577  bj-ssbid2ALT  36651  bj-spnfw  36658  bj-spst  36677  bj-19.23bit  36679  wl-syls2  37497  heibor1lem  37803  isltrn2N  40114  cdlemefrs32fva  40394  fiinfi  43562  con3ALT2  44520  alrim3con13v  44523  islinindfis  48435  setrec1lem4  49676