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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com12  27  syl5  28  pm2.6dc  758  pm5.11dc  814  ax16i  1735  mor  1939  ceqsalg  2576  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  spc2egv  2636  spc2gv  2637  spc3egv  2638  spc3gv  2639  disjne  3267  uneqdifeqim  3302  triun  3858  sucssel  4127  ordsucg  4194  regexmidlem1  4218  relresfld  4790  relcoi1  4792  fornex  5684  f1dmex  5685  rdgon  5913  dom2d  6189  nneo  8117  zeo2  8120  uznfz  8735  difelfzle  8762  ssfzo12  8850  bj-indsuc  9387  bj-nntrans  9411