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  870  pm5.11dc  917  ax16i  1907  mor  2125  ceqsalg  2844  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  spc2egv  2909  spc2gv  2910  spc3egv  2911  spc3gv  2912  disjne  3566  uneqdifeqim  3599  eqifdc  3663  triun  4226  sucssel  4550  ordsucg  4629  regexmidlem1  4660  relresfld  5297  relcoi1  5299  focdmex  6317  f1dmex  6318  dom2d  7025  findcard  7158  nneo  9699  zeo2  9702  uznfz  10459  difelfzle  10490  ssfzo12  10591  facndiv  11126  swrdswrd  11422  pfxccatin12lem2  11448  pfxccatin12  11450  pfxccat3  11451  fisumcom2  12149  fprodssdc  12301  fprodcom2fi  12337  ndvdssub  12641  bezoutlembi  12726  eucalglt  12779  prmind2  12842  coprm  12866  prmdiveq  12958  mhmlin  13722  issubg2m  13942  nsgbi  13957  issubrng2  14456  issubrg2  14487  lmodlema  14566  rmodislmodlem  14624  rmodislmod  14625  lspsnel6  14682  inopn  14994  basis1  15038  tgss  15054  tgcl  15055  xmeteq0  15350  blssexps  15420  blssex  15421  mopni3  15475  neibl  15482  metss  15485  metcnp3  15502  logbgcd1irr  15958  gausslemma2dlem0i  16056  2lgsoddprmlem3  16110  clwwlkn1loopb  16541  clwwlknonex2lem2  16559  bj-indsuc  16824  bj-nntrans  16847