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  3564  uneqdifeqim  3597  eqifdc  3661  triun  4223  sucssel  4547  ordsucg  4626  regexmidlem1  4657  relresfld  5294  relcoi1  5296  focdmex  6310  f1dmex  6311  dom2d  7014  findcard  7147  nneo  9684  zeo2  9687  uznfz  10441  difelfzle  10472  ssfzo12  10573  facndiv  11105  swrdswrd  11401  pfxccatin12lem2  11427  pfxccatin12  11429  pfxccat3  11430  fisumcom2  12128  fprodssdc  12280  fprodcom2fi  12316  ndvdssub  12620  bezoutlembi  12705  eucalglt  12758  prmind2  12821  coprm  12845  prmdiveq  12937  mhmlin  13697  issubg2m  13923  nsgbi  13938  issubrng2  14372  issubrg2  14403  lmodlema  14457  rmodislmodlem  14515  rmodislmod  14516  lspsnel6  14573  inopn  14885  basis1  14929  tgss  14945  tgcl  14946  xmeteq0  15241  blssexps  15311  blssex  15312  mopni3  15366  neibl  15373  metss  15376  metcnp3  15393  logbgcd1irr  15849  gausslemma2dlem0i  15947  2lgsoddprmlem3  16001  clwwlkn1loopb  16432  clwwlknonex2lem2  16450  bj-indsuc  16715  bj-nntrans  16738