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  869  pm5.11dc  916  ax16i  1906  mor  2122  ceqsalg  2831  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  spc2egv  2896  spc2gv  2897  spc3egv  2898  spc3gv  2899  disjne  3548  uneqdifeqim  3580  eqifdc  3642  triun  4200  sucssel  4521  ordsucg  4600  regexmidlem1  4631  relresfld  5266  relcoi1  5268  focdmex  6277  f1dmex  6278  dom2d  6946  findcard  7077  nneo  9583  zeo2  9586  uznfz  10338  difelfzle  10369  ssfzo12  10470  facndiv  11002  swrdswrd  11290  pfxccatin12lem2  11316  pfxccatin12  11318  pfxccat3  11319  fisumcom2  12017  fprodssdc  12169  fprodcom2fi  12205  ndvdssub  12509  bezoutlembi  12594  eucalglt  12647  prmind2  12710  coprm  12734  prmdiveq  12826  mhmlin  13568  issubg2m  13794  nsgbi  13809  issubrng2  14243  issubrg2  14274  lmodlema  14325  rmodislmodlem  14383  rmodislmod  14384  lspsnel6  14441  inopn  14746  basis1  14790  tgss  14806  tgcl  14807  xmeteq0  15102  blssexps  15172  blssex  15173  mopni3  15227  neibl  15234  metss  15237  metcnp3  15254  logbgcd1irr  15710  gausslemma2dlem0i  15805  2lgsoddprmlem3  15859  clwwlkn1loopb  16290  clwwlknonex2lem2  16308  bj-indsuc  16574  bj-nntrans  16597