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  797  pm5.11dc  853  ax16i  1786  mor  1990  ceqsalg  2647  cgsexg  2654  cgsex2g  2655  cgsex4g  2656  spc2egv  2708  spc2gv  2709  spc3egv  2710  spc3gv  2711  disjne  3336  uneqdifeqim  3368  eqifdc  3425  triun  3949  sucssel  4251  ordsucg  4319  regexmidlem1  4349  relresfld  4960  relcoi1  4962  fornex  5886  f1dmex  5887  dom2d  6488  findcard  6602  nneo  8847  zeo2  8850  uznfz  9513  difelfzle  9541  ssfzo12  9631  facndiv  10143  fisumcom2  10828  ndvdssub  11204  bezoutlembi  11268  eucalglt  11313  prmind2  11376  coprm  11397  inopn  11555  bj-indsuc  11778  bj-nntrans  11801