Theorem syl5com 26

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)

Hypotheses

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

Assertion

Ref	Expression
syl5com	|- (ph -> (ch -> th))

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 |- (ph -> ps)
2	1	a1d 22	. 2 |- (ph -> (ch -> ps))
3		syl5com.2	. 2 |- (ch -> (ps -> th))
4	2, 3	sylcom 25	1 |- (ph -> (ch -> th))

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com12  27  syl5  28  ax16i  2046  ceqsalg  2884  cgsexg  2891  cgsex2g  2892  cgsex4g  2893  spc2egv  2942  spc3egv  2944  disjne  3597  uneqdifeq  3639  ncfinraise  4482  nnpweq  4524  fvimacnv  5404