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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com12  30  syl5  32  pm2.6dc  793  pm5.11dc  849  ax16i  1780  mor  1984  ceqsalg  2628  cgsexg  2635  cgsex2g  2636  cgsex4g  2637  spc2egv  2688  spc2gv  2689  spc3egv  2690  spc3gv  2691  disjne  3304  uneqdifeqim  3335  triun  3896  sucssel  4187  ordsucg  4254  regexmidlem1  4284  relresfld  4877  relcoi1  4879  fornex  5773  f1dmex  5774  dom2d  6320  findcard  6422  nneo  8531  zeo2  8534  uznfz  9196  difelfzle  9222  ssfzo12  9310  facndiv  9763  ndvdssub  10474  bezoutlembi  10538  eucalglt  10583  prmind2  10646  coprm  10667  bj-indsuc  10881  bj-nntrans  10904