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  1872  mor  2087  ceqsalg  2791  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  disjne  3505  uneqdifeqim  3537  eqifdc  3597  triun  4145  sucssel  4460  ordsucg  4539  regexmidlem1  4570  relresfld  5200  relcoi1  5202  focdmex  6181  f1dmex  6182  dom2d  6841  findcard  6958  nneo  9446  zeo2  9449  uznfz  10195  difelfzle  10226  ssfzo12  10317  facndiv  10848  fisumcom2  11620  fprodssdc  11772  fprodcom2fi  11808  ndvdssub  12112  bezoutlembi  12197  eucalglt  12250  prmind2  12313  coprm  12337  prmdiveq  12429  mhmlin  13169  issubg2m  13395  nsgbi  13410  issubrng2  13842  issubrg2  13873  lmodlema  13924  rmodislmodlem  13982  rmodislmod  13983  lspsnel6  14040  inopn  14323  basis1  14367  tgss  14383  tgcl  14384  xmeteq0  14679  blssexps  14749  blssex  14750  mopni3  14804  neibl  14811  metss  14814  metcnp3  14831  logbgcd1irr  15287  gausslemma2dlem0i  15382  2lgsoddprmlem3  15436  bj-indsuc  15658  bj-nntrans  15681