Theorem sylani 513

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  syl2ani 515  ordtypelem7 5690  inf3lem2 5720  zorn2lem5 5954  distrlem4pr 6282  supxrun 7294  uzwo4OLD 7422  uzwo 7624  uzwoOLD 7625  metelcls 9243  bcthlem33 9309  gapmlem 9461  subtopmet 10256  projlem1 10819  projlem25 10843  spanunsni 11135  csmdsymi 11906  ordtypelem7OLD 15381  cnsubsp2 15427  fnejoin2 15531  heiborlem35 15989  pmapjoin 17313

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 164  df-an 242

Copyright terms: Public domain