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  con2 90  imbi1i 184  dfor2 227  pm2.67 280  pm3.41 325  pm3.42 326  jaob 422  oibabs 657  pm2.26 662  dedlem0a 765  meredith 931  19.23 1099  19.39 1118  a12study 1417  r19.37av 1807  axrep1 2768  axrep2 2769  dmcosseq 3452  tz7.48lem 4256  kmlem1 4911  kmlem13 4923  axpowndlem2 5104  axacndlem4 5116  suppsr2 5377  suppsr3 5378  xrub 6248  supxrre 6251  seqzeq 6750  cau5ii 7120  iserzshft2i 7310  clim2serz 7337  iserzmulc1 7339  isum1p 7410  isumrecl 7414  fsum0diaglem2 7462  islp2 7957  nmounbseqi 8694  chcmhi 9389  dmdmd 10508  mdslmd1lem2 10534  sumdmdi 10629  dmdbr4ati 10630  dmdbr6ati 10632  dfcon2 11501

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

Copyright terms: Public domain