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  2829  cgsexg  2836  cgsex2g  2837  cgsex4g  2838  spc2egv  2894  spc2gv  2895  spc3egv  2896  spc3gv  2897  disjne  3546  uneqdifeqim  3578  eqifdc  3640  triun  4198  sucssel  4519  ordsucg  4598  regexmidlem1  4629  relresfld  5264  relcoi1  5266  focdmex  6272  f1dmex  6273  dom2d  6941  findcard  7070  nneo  9573  zeo2  9576  uznfz  10328  difelfzle  10359  ssfzo12  10459  facndiv  10991  swrdswrd  11276  pfxccatin12lem2  11302  pfxccatin12  11304  pfxccat3  11305  fisumcom2  11989  fprodssdc  12141  fprodcom2fi  12177  ndvdssub  12481  bezoutlembi  12566  eucalglt  12619  prmind2  12682  coprm  12706  prmdiveq  12798  mhmlin  13540  issubg2m  13766  nsgbi  13781  issubrng2  14214  issubrg2  14245  lmodlema  14296  rmodislmodlem  14354  rmodislmod  14355  lspsnel6  14412  inopn  14717  basis1  14761  tgss  14777  tgcl  14778  xmeteq0  15073  blssexps  15143  blssex  15144  mopni3  15198  neibl  15205  metss  15208  metcnp3  15225  logbgcd1irr  15681  gausslemma2dlem0i  15776  2lgsoddprmlem3  15830  clwwlkn1loopb  16215  clwwlknonex2lem2  16233  bj-indsuc  16459  bj-nntrans  16482