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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com12  30  syl5  32  pm2.6dc  874  pm5.11dc  921  ax16i  1911  mor  2129  ceqsalg  2850  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  disjne  3578  uneqdifeqim  3613  eqifdc  3677  triun  4244  sucssel  4571  ordsucg  4651  regexmidlem1  4682  relresfld  5320  relcoi1  5322  focdmex  6348  f1dmex  6349  dom2d  7065  findcard  7198  nneo  9759  zeo2  9762  uznfz  10526  difelfzle  10557  ssfzo12  10658  facndiv  11198  swrdswrd  11498  pfxccatin12lem2  11524  pfxccatin12  11526  pfxccat3  11527  fisumcom2  12229  fprodssdc  12381  fprodcom2fi  12417  ndvdssub  12721  bezoutlembi  12806  eucalglt  12859  prmind2  12922  coprm  12947  prmdiveq  13042  mhmlin  13832  issubg2m  14050  nsgbi  14065  issubrng2  14626  issubrg2  14657  lmodlema  14736  rmodislmodlem  14795  rmodislmod  14796  ellspsn6  14853  inopn  15246  basis1  15290  tgss  15306  tgcl  15307  xmeteq0  15602  blssexps  15672  blssex  15673  mopni3  15727  neibl  15734  metss  15737  metcnp3  15754  logbgcd1irr  16220  gausslemma2dlem0i  16398  2lgsoddprmlem3  16452  clwwlkn1loopb  16883  clwwlknonex2lem2  16901  bj-indsuc  17176  bj-nntrans  17199