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  870  pm5.11dc  917  ax16i  1906  mor  2122  ceqsalg  2832  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  spc2egv  2897  spc2gv  2898  spc3egv  2899  spc3gv  2900  disjne  3550  uneqdifeqim  3582  eqifdc  3646  triun  4205  sucssel  4527  ordsucg  4606  regexmidlem1  4637  relresfld  5273  relcoi1  5275  focdmex  6286  f1dmex  6287  dom2d  6989  findcard  7120  nneo  9627  zeo2  9630  uznfz  10383  difelfzle  10414  ssfzo12  10515  facndiv  11047  swrdswrd  11335  pfxccatin12lem2  11361  pfxccatin12  11363  pfxccat3  11364  fisumcom2  12062  fprodssdc  12214  fprodcom2fi  12250  ndvdssub  12554  bezoutlembi  12639  eucalglt  12692  prmind2  12755  coprm  12779  prmdiveq  12871  mhmlin  13613  issubg2m  13839  nsgbi  13854  issubrng2  14288  issubrg2  14319  lmodlema  14371  rmodislmodlem  14429  rmodislmod  14430  lspsnel6  14487  inopn  14797  basis1  14841  tgss  14857  tgcl  14858  xmeteq0  15153  blssexps  15223  blssex  15224  mopni3  15278  neibl  15285  metss  15288  metcnp3  15305  logbgcd1irr  15761  gausslemma2dlem0i  15859  2lgsoddprmlem3  15913  clwwlkn1loopb  16344  clwwlknonex2lem2  16362  bj-indsuc  16627  bj-nntrans  16650