Theorem imim1i 16

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent.

Hypothesis

Ref	Expression
imim1i.1	|- (ph -> ps)

Assertion

Ref	Expression
imim1i	|- ((ps -> ch) -> (ph -> ch))

Proof of Theorem imim1i

Step	Hyp	Ref	Expression
1		imim1i.1	. 2 |- (ph -> ps)
2		imim1 15	. 2 |- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))
3	1, 2	ax-mp 7	1 |- ((ps -> ch) -> (ph -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim12i 18  syl5 21  syl7 23  pm2.86 69  loolin 72  loowoz 73  peirce 82  pm2.01 88  con2 90  imbi1i 186  dfor2 229  pm2.67 282  pm3.41 327  pm3.42 328  jaob 422  oibabs 654  pm2.26 659  dedlem0a 760  meredith 924  19.23 1063  19.39 1082  a12study 1378  r19.37av 1761  axrep1 2694  axrep2 2695  dmcosseq 3365  tz7.48lem 3955  kmlem1 4765  kmlem13 4777  axpowndlem2 4950  axacndlem4 4962  suppsr2 5223  suppsr3 5224  xrub 6080  supxrre 6083  seqzeq 6555  cau5i 6917  iserzshft2 7107  clim2serzt 7134  iserzmulc1 7136  isum1p 7206  isumreclt 7210  fsum0diaglem2 7257  islp2 7747  chcmh 9113  dmdmdt 10227  mdslmd1lem2 10253  sumdmd 10347  dmdbr4at 10348  dmdbr6at 10350  fillsb 10560

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain