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 424  oibabs 656  pm2.26 661  dedlem0a 762  meredith 926  19.23 1065  19.39 1084  a12study 1380  r19.37av 1764  axrep1 2699  axrep2 2700  dmcosseq 3371  tz7.48lem 3961  kmlem1 4775  kmlem13 4787  axpowndlem2 4962  axacndlem4 4974  suppsr2 5235  suppsr3 5236  xrub 6082  supxrre 6085  seqzeq 6556  cau5i 6917  iserzshft2 7107  clim2serzt 7134  iserzmulc1 7136  isum1p 7206  isumreclt 7210  fsum0diaglem2 7257  islp2 7744  chcmh 9108  dmdmdt 10222  mdslmd1lem2 10248  sumdmd 10342  dmdbr4at 10343  dmdbr6at 10345

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

Copyright terms: Public domain