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 740  onminex 3015  elreldm 3333  tz6.12c 3731  oeordi 4204  f1domg 4383  f1dom2g 4384  ssdom2g 4396  php 4499  cardmin 4840  carduniima 4870  suplem2pr 5142  supsr 5211  elghomlem2 10317

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

Copyright terms: Public domain