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 653  pm2.26 658  dedlem0a 759  meredith 922  19.23 1061  19.39 1080  a12study 1376  r19.37av 1758  axrep1 2689  axrep2 2690  dmcosseq 3357  tz7.48lem 3946  kmlem1 4745  kmlem13 4757  axpowndlem2 4930  axacndlem4 4942  suppsr2 5203  suppsr3 5204  xrub 6035  supxrre 6038  seqzeq 6495  cau5i 6862  iserzshft2 7052  clim2serzt 7078  iserzmulc1 7080  isum1p 7149  isumreclt 7153  fsum0diaglem2 7200  islp2 7697  chcmh 9052  dmdmdt 10165  mdslmd1lem2 10190  sumdmd 10283  dmdbr6at 10285  fillsb 10471

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

Copyright terms: Public domain