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  9754  zeo2  9757  uznfz  10521  difelfzle  10552  ssfzo12  10653  facndiv  11193  swrdswrd  11493  pfxccatin12lem2  11519  pfxccatin12  11521  pfxccat3  11522  fisumcom2  12224  fprodssdc  12376  fprodcom2fi  12412  ndvdssub  12716  bezoutlembi  12801  eucalglt  12854  prmind2  12917  coprm  12942  prmdiveq  13037  mhmlin  13827  issubg2m  14045  nsgbi  14060  issubrng2  14602  issubrg2  14633  lmodlema  14712  rmodislmodlem  14771  rmodislmod  14772  ellspsn6  14829  inopn  15195  basis1  15239  tgss  15255  tgcl  15256  xmeteq0  15551  blssexps  15621  blssex  15622  mopni3  15676  neibl  15683  metss  15686  metcnp3  15703  logbgcd1irr  16164  gausslemma2dlem0i  16342  2lgsoddprmlem3  16396  clwwlkn1loopb  16827  clwwlknonex2lem2  16845  bj-indsuc  17120  bj-nntrans  17143