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  863  pm5.11dc  910  ax16i  1880  mor  2095  ceqsalg  2799  cgsexg  2806  cgsex2g  2807  cgsex4g  2808  spc2egv  2862  spc2gv  2863  spc3egv  2864  spc3gv  2865  disjne  3513  uneqdifeqim  3545  eqifdc  3606  triun  4154  sucssel  4470  ordsucg  4549  regexmidlem1  4580  relresfld  5211  relcoi1  5213  focdmex  6199  f1dmex  6200  dom2d  6863  findcard  6984  nneo  9475  zeo2  9478  uznfz  10224  difelfzle  10255  ssfzo12  10351  facndiv  10882  fisumcom2  11720  fprodssdc  11872  fprodcom2fi  11908  ndvdssub  12212  bezoutlembi  12297  eucalglt  12350  prmind2  12413  coprm  12437  prmdiveq  12529  mhmlin  13270  issubg2m  13496  nsgbi  13511  issubrng2  13943  issubrg2  13974  lmodlema  14025  rmodislmodlem  14083  rmodislmod  14084  lspsnel6  14141  inopn  14446  basis1  14490  tgss  14506  tgcl  14507  xmeteq0  14802  blssexps  14872  blssex  14873  mopni3  14927  neibl  14934  metss  14937  metcnp3  14954  logbgcd1irr  15410  gausslemma2dlem0i  15505  2lgsoddprmlem3  15559  bj-indsuc  15826  bj-nntrans  15849