Theorem imim1 18

Description: A closed form of syllogism (see syl 12). Theorem *2.06 of [WhiteheadRussell] p. 100.

Assertion

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

Proof of Theorem imim1

Step	Hyp	Ref	Expression
1		imim2 17	. 2 |- ((ps -> ch) -> ((ph -> ps) -> (ph -> ch)))
2	1	com12 14	1 |- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim1i 19  imim1d 33  pm2.83 35  looinv 99  pm3.33 384  immo 1813  sstr2OLD 2624  intss 3239  suppsr2 6375  ivthlem3 8545  usinuniop 10341  tb-ax1 14128  tbw-ax1 14167  heiborlem13 15967  3ax5VD 16686  syl5impVD 16687

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

Copyright terms: Public domain