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  4244  sucssel  4571  ordsucg  4651  regexmidlem1  4682  relresfld  5320  relcoi1  5322  focdmex  6348  f1dmex  6349  dom2d  7063  findcard  7196  nneo  9760  zeo2  9763  uznfz  10527  difelfzle  10558  ssfzo12  10659  facndiv  11199  swrdswrd  11499  pfxccatin12lem2  11525  pfxccatin12  11527  pfxccat3  11528  fisumcom2  12230  fprodssdc  12382  fprodcom2fi  12418  ndvdssub  12722  bezoutlembi  12807  eucalglt  12860  prmind2  12923  coprm  12948  prmdiveq  13043  mhmlin  13833  issubg2m  14051  nsgbi  14066  issubrng2  14627  issubrg2  14658  lmodlema  14737  rmodislmodlem  14796  rmodislmod  14797  ellspsn6  14854  inopn  15229  basis1  15273  tgss  15289  tgcl  15290  xmeteq0  15585  blssexps  15655  blssex  15656  mopni3  15710  neibl  15717  metss  15720  metcnp3  15737  logbgcd1irr  16203  gausslemma2dlem0i  16381  2lgsoddprmlem3  16435  clwwlkn1loopb  16866  clwwlknonex2lem2  16884  bj-indsuc  17159  bj-nntrans  17182