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  1882  mor  2098  ceqsalg  2806  cgsexg  2813  cgsex2g  2814  cgsex4g  2815  spc2egv  2871  spc2gv  2872  spc3egv  2873  spc3gv  2874  disjne  3523  uneqdifeqim  3555  eqifdc  3617  triun  4172  sucssel  4490  ordsucg  4569  regexmidlem1  4600  relresfld  5232  relcoi1  5234  focdmex  6225  f1dmex  6226  dom2d  6889  findcard  7013  nneo  9513  zeo2  9516  uznfz  10262  difelfzle  10293  ssfzo12  10392  facndiv  10923  swrdswrd  11198  pfxccatin12lem2  11224  pfxccatin12  11226  pfxccat3  11227  fisumcom2  11910  fprodssdc  12062  fprodcom2fi  12098  ndvdssub  12402  bezoutlembi  12487  eucalglt  12540  prmind2  12603  coprm  12627  prmdiveq  12719  mhmlin  13460  issubg2m  13686  nsgbi  13701  issubrng2  14133  issubrg2  14164  lmodlema  14215  rmodislmodlem  14273  rmodislmod  14274  lspsnel6  14331  inopn  14636  basis1  14680  tgss  14696  tgcl  14697  xmeteq0  14992  blssexps  15062  blssex  15063  mopni3  15117  neibl  15124  metss  15127  metcnp3  15144  logbgcd1irr  15600  gausslemma2dlem0i  15695  2lgsoddprmlem3  15749  bj-indsuc  16171  bj-nntrans  16194