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  4114  sucssel  4424  ordsucg  4501  regexmidlem1  4532  relresfld  5158  relcoi1  5160  focdmex  6115  f1dmex  6116  dom2d  6772  findcard  6887  nneo  9354  zeo2  9357  uznfz  10100  difelfzle  10131  ssfzo12  10221  facndiv  10714  fisumcom2  11441  fprodssdc  11593  fprodcom2fi  11629  ndvdssub  11929  bezoutlembi  12000  eucalglt  12051  prmind2  12114  coprm  12138  prmdiveq  12230  mhmlin  12812  issubg2m  13002  nsgbi  13017  issubrg2  13322  inopn  13394  basis1  13438  tgss  13456  tgcl  13457  xmeteq0  13752  blssexps  13822  blssex  13823  mopni3  13877  neibl  13884  metss  13887  metcnp3  13904  logbgcd1irr  14278  bj-indsuc  14562  bj-nntrans  14585