Theorem syli 39

Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)

Hypotheses

Ref	Expression
syli.1	|- ( ps -> ( ph -> ch ) )
syli.2	|- ( ch -> ( ph -> th ) )

Assertion

Ref	Expression
syli	|- ( ps -> ( ph -> th ) )

Proof of Theorem syli

Step	Hyp	Ref	Expression
1		syli.1	. 2 |- ( ps -> ( ph -> ch ) )
2		syli.2	. . 3 |- ( ch -> ( ph -> th ) )
3	2	com12 32	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	sylcom 30	1 |- ( ps -> ( ph -> 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:  ibd  258  bija  370  equvini  2346  equvel  2347  2eu6  2558  rgen2a  2977  rexraleqim  3328  elreldm  5350  tz6.12c  6213  onminex  7007  rntpos  7365  smores  7449  seqomlem2  7546  f1domg  7975  php  8144  fodomnum  8880  carduniima  8919  cardmin  9386  negn0  10459  sqrmo  13992  isch3  28098  cgrtriv  32109  wl-lem-moexsb  33350  grpomndo  33674  elghomlem2OLD  33685