Theorem sylcom 51

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

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 3113  funopg 3533  tz7.49 3944  abianfp 3947  elrnoprabg 4108  unblem3 4519  isfinite2 4523  nsmallpq 5055  uzwo4OLD 6158  uzwo 6387  uzwoOLD 6388  chcmh 9034  h1datom 9421  irredlem1 10225

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

Copyright terms: Public domain