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  867  pm5.11dc  914  ax16i  1904  mor  2120  ceqsalg  2828  cgsexg  2835  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  spc3egv  2895  spc3gv  2896  disjne  3545  uneqdifeqim  3577  eqifdc  3639  triun  4195  sucssel  4515  ordsucg  4594  regexmidlem1  4625  relresfld  5258  relcoi1  5260  focdmex  6266  f1dmex  6267  dom2d  6932  findcard  7058  nneo  9561  zeo2  9564  uznfz  10311  difelfzle  10342  ssfzo12  10442  facndiv  10973  swrdswrd  11252  pfxccatin12lem2  11278  pfxccatin12  11280  pfxccat3  11281  fisumcom2  11964  fprodssdc  12116  fprodcom2fi  12152  ndvdssub  12456  bezoutlembi  12541  eucalglt  12594  prmind2  12657  coprm  12681  prmdiveq  12773  mhmlin  13515  issubg2m  13741  nsgbi  13756  issubrng2  14189  issubrg2  14220  lmodlema  14271  rmodislmodlem  14329  rmodislmod  14330  lspsnel6  14387  inopn  14692  basis1  14736  tgss  14752  tgcl  14753  xmeteq0  15048  blssexps  15118  blssex  15119  mopni3  15173  neibl  15180  metss  15183  metcnp3  15200  logbgcd1irr  15656  gausslemma2dlem0i  15751  2lgsoddprmlem3  15805  bj-indsuc  16346  bj-nntrans  16369