Theorem syl5com 29

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 28	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  30  syl5  32  pm2.6dc  848  pm5.11dc  895  ax16i  1831  mor  2042  ceqsalg  2717  cgsexg  2724  cgsex2g  2725  cgsex4g  2726  spc2egv  2779  spc2gv  2780  spc3egv  2781  spc3gv  2782  disjne  3421  uneqdifeqim  3453  eqifdc  3511  triun  4047  sucssel  4354  ordsucg  4426  regexmidlem1  4456  relresfld  5076  relcoi1  5078  fornex  6021  f1dmex  6022  dom2d  6675  findcard  6790  nneo  9178  zeo2  9181  uznfz  9914  difelfzle  9942  ssfzo12  10032  facndiv  10517  fisumcom2  11239  ndvdssub  11663  bezoutlembi  11729  eucalglt  11774  prmind2  11837  coprm  11858  inopn  12209  basis1  12253  tgss  12271  tgcl  12272  xmeteq0  12567  blssexps  12637  blssex  12638  mopni3  12692  neibl  12699  metss  12702  metcnp3  12719  logbgcd1irr  13092  bj-indsuc  13297  bj-nntrans  13320