Theorem syli 54

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

Syntax hints:   -> wi 3

This theorem is referenced by:  pclem6 741  onminex 3020  elreldm 3338  tz6.12c 3740  oeordi 4214  f1domg 4396  f1dom2g 4397  ssdom2g 4409  php 4513  cardmin 4860  carduniima 4890  suplem2pr 5162  supsr 5231  elghomlem2 10383

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain