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  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  3577  uneqdifeqim  3610  eqifdc  3674  triun  4237  sucssel  4564  ordsucg  4644  regexmidlem1  4675  relresfld  5312  relcoi1  5314  focdmex  6334  f1dmex  6335  dom2d  7049  findcard  7182  nneo  9728  zeo2  9731  uznfz  10488  difelfzle  10519  ssfzo12  10620  facndiv  11155  swrdswrd  11455  pfxccatin12lem2  11481  pfxccatin12  11483  pfxccat3  11484  fisumcom2  12183  fprodssdc  12335  fprodcom2fi  12371  ndvdssub  12675  bezoutlembi  12760  eucalglt  12813  prmind2  12876  coprm  12900  prmdiveq  12992  mhmlin  13751  issubg2m  13969  nsgbi  13984  issubrng2  14491  issubrg2  14522  lmodlema  14601  rmodislmodlem  14659  rmodislmod  14660  lspsnel6  14717  inopn  15027  basis1  15071  tgss  15087  tgcl  15088  xmeteq0  15383  blssexps  15453  blssex  15454  mopni3  15508  neibl  15515  metss  15518  metcnp3  15535  logbgcd1irr  15992  gausslemma2dlem0i  16090  2lgsoddprmlem3  16144  clwwlkn1loopb  16575  clwwlknonex2lem2  16593  bj-indsuc  16868  bj-nntrans  16891