Theorem sylani 466

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylani.1	|- (ph -> ((ps /\ ch) -> th))
sylani.2	|- (ta -> ps)

Assertion

Ref	Expression
sylani	|- (ph -> ((ta /\ ch) -> th))

Proof of Theorem sylani

Step	Hyp	Ref	Expression
1		sylani.1	. 2 |- (ph -> ((ps /\ ch) -> th))
2		sylani.2	. . 3 |- (ta -> ps)
3	2	a1i 8	. 2 |- (ph -> (ta -> ps))
4	1, 3	syland 459	1 |- (ph -> ((ta /\ ch) -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  syl2ani 468  inf3lem2 4623  zorn2lem5 4802  distrlem4pr 5142  supxrun 6087  uzwo4OLD 6212  uzwo 6456  uzwoOLD 6457  metelcls 7962  bcthlem33 8028  projlem1 9181  projlem25 9205  spanunsn 9497  csmdsym 10256

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain