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  4194  sucssel  4514  ordsucg  4593  regexmidlem1  4624  relresfld  5257  relcoi1  5259  focdmex  6258  f1dmex  6259  dom2d  6922  findcard  7046  nneo  9546  zeo2  9549  uznfz  10295  difelfzle  10326  ssfzo12  10425  facndiv  10956  swrdswrd  11232  pfxccatin12lem2  11258  pfxccatin12  11260  pfxccat3  11261  fisumcom2  11944  fprodssdc  12096  fprodcom2fi  12132  ndvdssub  12436  bezoutlembi  12521  eucalglt  12574  prmind2  12637  coprm  12661  prmdiveq  12753  mhmlin  13495  issubg2m  13721  nsgbi  13736  issubrng2  14168  issubrg2  14199  lmodlema  14250  rmodislmodlem  14308  rmodislmod  14309  lspsnel6  14366  inopn  14671  basis1  14715  tgss  14731  tgcl  14732  xmeteq0  15027  blssexps  15097  blssex  15098  mopni3  15152  neibl  15159  metss  15162  metcnp3  15179  logbgcd1irr  15635  gausslemma2dlem0i  15730  2lgsoddprmlem3  15784  bj-indsuc  16249  bj-nntrans  16272