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  864  pm5.11dc  911  ax16i  1881  mor  2096  ceqsalg  2800  cgsexg  2807  cgsex2g  2808  cgsex4g  2809  spc2egv  2863  spc2gv  2864  spc3egv  2865  spc3gv  2866  disjne  3514  uneqdifeqim  3546  eqifdc  3607  triun  4155  sucssel  4471  ordsucg  4550  regexmidlem1  4581  relresfld  5212  relcoi1  5214  focdmex  6200  f1dmex  6201  dom2d  6864  findcard  6985  nneo  9476  zeo2  9479  uznfz  10225  difelfzle  10256  ssfzo12  10353  facndiv  10884  fisumcom2  11749  fprodssdc  11901  fprodcom2fi  11937  ndvdssub  12241  bezoutlembi  12326  eucalglt  12379  prmind2  12442  coprm  12466  prmdiveq  12558  mhmlin  13299  issubg2m  13525  nsgbi  13540  issubrng2  13972  issubrg2  14003  lmodlema  14054  rmodislmodlem  14112  rmodislmod  14113  lspsnel6  14170  inopn  14475  basis1  14519  tgss  14535  tgcl  14536  xmeteq0  14831  blssexps  14901  blssex  14902  mopni3  14956  neibl  14963  metss  14966  metcnp3  14983  logbgcd1irr  15439  gausslemma2dlem0i  15534  2lgsoddprmlem3  15588  bj-indsuc  15864  bj-nntrans  15887