Theorem sylcom 51

Description: Syllogism inference with commutation of antecedents. (The proof was shortened by O'Cat, 2-Feb-2006 and shortened further by Stefan Allan, 23-Feb-2006.)

Hypotheses

Ref	Expression
sylcom.1	|- (ph -> (ps -> ch))
sylcom.2	|- (ps -> (ch -> th))

Assertion

Ref	Expression
sylcom	|- (ph -> (ps -> th))

Proof of Theorem sylcom

Step	Hyp	Ref	Expression
1		sylcom.1	. 2 |- (ph -> (ps -> ch))
2		sylcom.2	. . 3 |- (ps -> (ch -> th))
3	2	a2i 9	. 2 |- ((ps -> ch) -> (ps -> th))
4	1, 3	syl 10	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl5com 52  syli 54  limuni3 3118  funopg 3539  tz7.49 3950  abianfp 3953  elrnoprabg 4114  unblem3 4525  isfinite2 4529  nsmallpq 5063  uzwo4OLD 6166  uzwo 6395  uzwoOLD 6396  chcmh 9052  h1datom 9444  irredlem1 10254

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

Copyright terms: Public domain