Theorem sylcom 62

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 10	. 2 |- ((ps -> ch) -> (ps -> th))
4	1, 3	syl 12	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl5com 63  syli 65  limuni3 3936  dmcosseq 4214  iss 4254  funopg 4454  elrnoprabg 5066  tz7.49 5168  abianfp 5171  unblem3 5635  isfinite2 5639  nsmallpq 6235  uzwo4OLD 7422  uzwo 7624  uzwoOLD 7625  gafo 9451  dif1en 10172  cncomp 10331  chcmhi 10746  h1datomi 11137  irredlem1 11962  fnn0ind 13611  wfrlem12 13968  npincppr 14501  compsublem 15430  compfipin0 15436

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

Copyright terms: Public domain