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  863  pm5.11dc  910  ax16i  1869  mor  2084  ceqsalg  2788  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  spc2egv  2850  spc2gv  2851  spc3egv  2852  spc3gv  2853  disjne  3500  uneqdifeqim  3532  eqifdc  3592  triun  4140  sucssel  4455  ordsucg  4534  regexmidlem1  4565  relresfld  5195  relcoi1  5197  focdmex  6167  f1dmex  6168  dom2d  6827  findcard  6944  nneo  9420  zeo2  9423  uznfz  10169  difelfzle  10200  ssfzo12  10291  facndiv  10810  fisumcom2  11581  fprodssdc  11733  fprodcom2fi  11769  ndvdssub  12071  bezoutlembi  12142  eucalglt  12195  prmind2  12258  coprm  12282  prmdiveq  12374  mhmlin  13039  issubg2m  13259  nsgbi  13274  issubrng2  13706  issubrg2  13737  lmodlema  13788  rmodislmodlem  13846  rmodislmod  13847  lspsnel6  13904  inopn  14171  basis1  14215  tgss  14231  tgcl  14232  xmeteq0  14527  blssexps  14597  blssex  14598  mopni3  14652  neibl  14659  metss  14662  metcnp3  14679  logbgcd1irr  15099  gausslemma2dlem0i  15173  2lgsoddprmlem3  15199  bj-indsuc  15420  bj-nntrans  15443