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  870  pm5.11dc  917  ax16i  1907  mor  2123  ceqsalg  2842  cgsexg  2849  cgsex2g  2850  cgsex4g  2851  spc2egv  2907  spc2gv  2908  spc3egv  2909  spc3gv  2910  disjne  3562  uneqdifeqim  3595  eqifdc  3659  triun  4221  sucssel  4545  ordsucg  4624  regexmidlem1  4655  relresfld  5292  relcoi1  5294  focdmex  6308  f1dmex  6309  dom2d  7012  findcard  7145  nneo  9681  zeo2  9684  uznfz  10437  difelfzle  10468  ssfzo12  10569  facndiv  11101  swrdswrd  11397  pfxccatin12lem2  11423  pfxccatin12  11425  pfxccat3  11426  fisumcom2  12124  fprodssdc  12276  fprodcom2fi  12312  ndvdssub  12616  bezoutlembi  12701  eucalglt  12754  prmind2  12817  coprm  12841  prmdiveq  12933  mhmlin  13680  issubg2m  13906  nsgbi  13921  issubrng2  14355  issubrg2  14386  lmodlema  14440  rmodislmodlem  14498  rmodislmod  14499  lspsnel6  14556  inopn  14868  basis1  14912  tgss  14928  tgcl  14929  xmeteq0  15224  blssexps  15294  blssex  15295  mopni3  15349  neibl  15356  metss  15359  metcnp3  15376  logbgcd1irr  15832  gausslemma2dlem0i  15930  2lgsoddprmlem3  15984  clwwlkn1loopb  16415  clwwlknonex2lem2  16433  bj-indsuc  16698  bj-nntrans  16721