Theorem syli 65

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

Syntax hints:   -> wi 3

This theorem is referenced by:  pclem6 813  onminex 3888  elreldm 4185  tz6.12c 4697  oeordi 5262  f1domg 5455  f1dom2g 5456  ssdom2g 5468  php 5607  infenomsub 5889  cardmin 6012  carduniima 6038  suplem2pr 6314  supsr 6383  elghomlem2 10194  grpmnd 10393  negn0 13655  injrec 14461  tostos 14637  inttop4 14865  infenomsubOLD 15398  smores 16446

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

Copyright terms: Public domain