Theorem imim1i 19

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 18	. 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:  syl5 20  imim12iOLD 22  syl7 26  pm2.86 84  loolin 87  loowoz 88  peirce 97  con2 105  imbi1i 202  dfor2 245  pm2.67 302  pm3.41 352  pm3.42 353  jaob 465  oibabs 713  pm2.26 718  dedlem0aOLD 832  3jaob 1006  meredithOLD 1048  19.23 1249  19.39 1271  a12study 1607  r19.37av 2067  axrep1 3244  axrep2 3245  dmcosseq 4025  dmcosseqOLD 4026  tz7.48lem 4975  19.21a3con13v 5637  kmlem1 5723  kmlem13 5735  axpowndlem2 5898  axacndlem4 5910  suppsr2 6171  suppsr3 6172  xrub 7084  supxrre 7087  seqzeq 7593  cau5ii 7964  iserzshft2i 8162  clim2serz 8189  iserzmulc1 8191  isum1p 8262  isumrecl 8266  fsum0diaglem2 8314  islp2 8818  nmounbseqi 9574  chcmhi 10538  dmdmd 11664  mdslmd1lem2 11690  sumdmdi 11784  dmdbr4ati 11785  dmdbr6ati 11787  bnj49 12213  bnj1532 12973  bnj1533 12974  dfon2lem8 13647  merco1 13910  merco2 13933  meran1 13965  dfcon2 15124

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

Copyright terms: Public domain