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  864  pm5.11dc  911  ax16i  1882  mor  2098  ceqsalg  2805  cgsexg  2812  cgsex2g  2813  cgsex4g  2814  spc2egv  2870  spc2gv  2871  spc3egv  2872  spc3gv  2873  disjne  3522  uneqdifeqim  3554  eqifdc  3616  triun  4171  sucssel  4489  ordsucg  4568  regexmidlem1  4599  relresfld  5231  relcoi1  5233  focdmex  6223  f1dmex  6224  dom2d  6887  findcard  7011  nneo  9511  zeo2  9514  uznfz  10260  difelfzle  10291  ssfzo12  10390  facndiv  10921  swrdswrd  11196  pfxccatin12lem2  11222  pfxccatin12  11224  pfxccat3  11225  fisumcom2  11864  fprodssdc  12016  fprodcom2fi  12052  ndvdssub  12356  bezoutlembi  12441  eucalglt  12494  prmind2  12557  coprm  12581  prmdiveq  12673  mhmlin  13414  issubg2m  13640  nsgbi  13655  issubrng2  14087  issubrg2  14118  lmodlema  14169  rmodislmodlem  14227  rmodislmod  14228  lspsnel6  14285  inopn  14590  basis1  14634  tgss  14650  tgcl  14651  xmeteq0  14946  blssexps  15016  blssex  15017  mopni3  15071  neibl  15078  metss  15081  metcnp3  15098  logbgcd1irr  15554  gausslemma2dlem0i  15649  2lgsoddprmlem3  15703  bj-indsuc  16063  bj-nntrans  16086