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  6276  f1dmex  6277  dom2d  6945  findcard  7076  nneo  9582  zeo2  9585  uznfz  10337  difelfzle  10368  ssfzo12  10468  facndiv  11000  swrdswrd  11285  pfxccatin12lem2  11311  pfxccatin12  11313  pfxccat3  11314  fisumcom2  11998  fprodssdc  12150  fprodcom2fi  12186  ndvdssub  12490  bezoutlembi  12575  eucalglt  12628  prmind2  12691  coprm  12715  prmdiveq  12807  mhmlin  13549  issubg2m  13775  nsgbi  13790  issubrng2  14223  issubrg2  14254  lmodlema  14305  rmodislmodlem  14363  rmodislmod  14364  lspsnel6  14421  inopn  14726  basis1  14770  tgss  14786  tgcl  14787  xmeteq0  15082  blssexps  15152  blssex  15153  mopni3  15207  neibl  15214  metss  15217  metcnp3  15234  logbgcd1irr  15690  gausslemma2dlem0i  15785  2lgsoddprmlem3  15839  clwwlkn1loopb  16270  clwwlknonex2lem2  16288  bj-indsuc  16523  bj-nntrans  16546