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  848  pm5.11dc  895  ax16i  1835  mor  2045  ceqsalg  2737  cgsexg  2744  cgsex2g  2745  cgsex4g  2746  spc2egv  2799  spc2gv  2800  spc3egv  2801  spc3gv  2802  disjne  3443  uneqdifeqim  3475  eqifdc  3535  triun  4071  sucssel  4379  ordsucg  4455  regexmidlem1  4486  relresfld  5108  relcoi1  5110  fornex  6053  f1dmex  6054  dom2d  6707  findcard  6822  nneo  9246  zeo2  9249  uznfz  9983  difelfzle  10011  ssfzo12  10101  facndiv  10590  fisumcom2  11312  fprodssdc  11464  fprodcom2fi  11500  ndvdssub  11794  bezoutlembi  11860  eucalglt  11905  prmind2  11968  coprm  11989  inopn  12340  basis1  12384  tgss  12402  tgcl  12403  xmeteq0  12698  blssexps  12768  blssex  12769  mopni3  12823  neibl  12830  metss  12833  metcnp3  12850  logbgcd1irr  13223  bj-indsuc  13441  bj-nntrans  13464