Theorem syl9r 56

Description: A nested syllogism inference with different antecedents.

Hypotheses

Ref	Expression
syl9r.1	|- (ph -> (ps -> ch))
syl9r.2	|- (th -> (ch -> ta ))

Assertion

Ref	Expression
syl9r	|- (th -> (ph -> (ps -> ta )))

Proof of Theorem syl9r

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3 |- (ph -> (ps -> ch))
2		syl9r.2	. . 3 |- (th -> (ch -> ta ))
3	1, 2	syl9 55	. 2 |- (ph -> (th -> (ps -> ta )))
4	3	com12 13	1 |- (th -> (ph -> (ps -> ta )))

Syntax hints:   -> wi 2

This theorem is referenced by:  sylan9r 360  hbsb4 905  a16g 933  oneqmin 2273  fununi 2705  isomin 2937  tz7.48lem 2993  sdomen2 3380  trcl 3489  indpi 3828  infxpidmlem7 4939  hlimcaui 5141  spansn 5462

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

metamath.org