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  852  pm5.11dc  899  ax16i  1846  mor  2056  ceqsalg  2754  cgsexg  2761  cgsex2g  2762  cgsex4g  2763  spc2egv  2816  spc2gv  2817  spc3egv  2818  spc3gv  2819  disjne  3462  uneqdifeqim  3494  eqifdc  3554  triun  4093  sucssel  4402  ordsucg  4479  regexmidlem1  4510  relresfld  5133  relcoi1  5135  fornex  6083  f1dmex  6084  dom2d  6739  findcard  6854  nneo  9294  zeo2  9297  uznfz  10038  difelfzle  10069  ssfzo12  10159  facndiv  10652  fisumcom2  11379  fprodssdc  11531  fprodcom2fi  11567  ndvdssub  11867  bezoutlembi  11938  eucalglt  11989  prmind2  12052  coprm  12076  prmdiveq  12168  inopn  12641  basis1  12685  tgss  12703  tgcl  12704  xmeteq0  12999  blssexps  13069  blssex  13070  mopni3  13124  neibl  13131  metss  13134  metcnp3  13151  logbgcd1irr  13525  bj-indsuc  13810  bj-nntrans  13833