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  9749  zeo2  9752  uznfz  10510  difelfzle  10541  ssfzo12  10642  facndiv  11177  swrdswrd  11477  pfxccatin12lem2  11503  pfxccatin12  11505  pfxccat3  11506  fisumcom2  12205  fprodssdc  12357  fprodcom2fi  12393  ndvdssub  12697  bezoutlembi  12782  eucalglt  12835  prmind2  12898  coprm  12922  prmdiveq  13014  mhmlin  13774  issubg2m  13992  nsgbi  14007  issubrng2  14518  issubrg2  14549  lmodlema  14628  rmodislmodlem  14687  rmodislmod  14688  ellspsn6  14745  inopn  15104  basis1  15148  tgss  15164  tgcl  15165  xmeteq0  15460  blssexps  15530  blssex  15531  mopni3  15585  neibl  15592  metss  15595  metcnp3  15612  logbgcd1irr  16069  gausslemma2dlem0i  16176  2lgsoddprmlem3  16230  clwwlkn1loopb  16661  clwwlknonex2lem2  16679  bj-indsuc  16954  bj-nntrans  16977