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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com12  30  syl5  32  pm2.6dc  874  pm5.11dc  921  ax16i  1911  mor  2129  ceqsalg  2850  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  disjne  3578  uneqdifeqim  3613  eqifdc  3677  triun  4242  sucssel  4569  ordsucg  4649  regexmidlem1  4680  relresfld  5317  relcoi1  5319  focdmex  6344  f1dmex  6345  dom2d  7059  findcard  7192  nneo  9753  zeo2  9756  uznfz  10520  difelfzle  10551  ssfzo12  10652  facndiv  11191  swrdswrd  11491  pfxccatin12lem2  11517  pfxccatin12  11519  pfxccat3  11520  fisumcom2  12221  fprodssdc  12373  fprodcom2fi  12409  ndvdssub  12713  bezoutlembi  12798  eucalglt  12851  prmind2  12914  coprm  12939  prmdiveq  13034  mhmlin  13823  issubg2m  14041  nsgbi  14056  issubrng2  14567  issubrg2  14598  lmodlema  14677  rmodislmodlem  14736  rmodislmod  14737  ellspsn6  14794  inopn  15153  basis1  15197  tgss  15213  tgcl  15214  xmeteq0  15509  blssexps  15579  blssex  15580  mopni3  15634  neibl  15641  metss  15644  metcnp3  15661  logbgcd1irr  16122  gausslemma2dlem0i  16274  2lgsoddprmlem3  16328  clwwlkn1loopb  16759  clwwlknonex2lem2  16777  bj-indsuc  17052  bj-nntrans  17075