Theorem syli 52

Description: Syllogism inference with common nested antecedent.

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 13	. 2 |- (ph -> (ch -> th))
4	1, 3	sylcom 51	1 |- (ps -> (ph -> th))

Syntax hints:   -> wi 2

This theorem is referenced by:  pclem6 555  onminex 2275  limsuclem 2360  elreldm 2554  f1dmex 2819  tz6.12c 2846  f1oeng 3298  f1domg 3299  f1dom2g 3300  ssdom2g 3312  php 3409  cardmin 3666  carduniima 3695  suplem2pr 3956  supsr 4025

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org