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  862  pm5.11dc  909  ax16i  1858  mor  2068  ceqsalg  2765  cgsexg  2772  cgsex2g  2773  cgsex4g  2774  spc2egv  2827  spc2gv  2828  spc3egv  2829  spc3gv  2830  disjne  3476  uneqdifeqim  3508  eqifdc  3569  triun  4112  sucssel  4422  ordsucg  4499  regexmidlem1  4530  relresfld  5155  relcoi1  5157  focdmex  6111  f1dmex  6112  dom2d  6768  findcard  6883  nneo  9350  zeo2  9353  uznfz  10096  difelfzle  10127  ssfzo12  10217  facndiv  10710  fisumcom2  11437  fprodssdc  11589  fprodcom2fi  11625  ndvdssub  11925  bezoutlembi  11996  eucalglt  12047  prmind2  12110  coprm  12134  prmdiveq  12226  mhmlin  12786  issubg2m  12975  inopn  13283  basis1  13327  tgss  13345  tgcl  13346  xmeteq0  13641  blssexps  13711  blssex  13712  mopni3  13766  neibl  13773  metss  13776  metcnp3  13793  logbgcd1irr  14167  bj-indsuc  14451  bj-nntrans  14474