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 3120  funopg 3544  tz7.49 3956  abianfp 3959  elrnoprabg 4121  unblem3 4532  isfinite2 4536  nsmallpq 5070  uzwo4OLD 6172  uzwo 6405  uzwoOLD 6406  chcmh 9101  h1datom 9494  irredlem1 10308

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

Copyright terms: Public domain