Theorem sylani 464

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 457	1 |- (ph -> ((ta /\ ch) -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  syl2ani 466  inf3lem2 4594  zorn2lem5 4772  distrlem4pr 5110  supxrun 6040  uzwo4OLD 6166  uzwo 6395  uzwoOLD 6396  metelcls 7916  bcthlem33 7981  projlem1 9125  projlem25 9149  spanunsn 9442  csmdsym 10198

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