Theorem syl9 55

Description: A nested syllogism inference with different antecedents. (The proof was shortened by Josh Purinton, 29-Dec-00.)

Hypotheses

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

Assertion

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

Proof of Theorem syl9

Step	Hyp	Ref	Expression
1		syl9.2	. . 3 |- (th -> (ch -> ta ))
2	1	a1i 7	. 2 |- (ph -> (th -> (ch -> ta )))
3		syl9.1	. 2 |- (ph -> (ps -> ch))
4	2, 3	syl5d 53	1 |- (ph -> (th -> (ps -> ta )))

Syntax hints:   -> wi 2

This theorem is referenced by:  syl9r 56  sbequi 876  hbsb4 905  sbal1 996  ralcom2 1314  reuss 1577  reupick 1578  ordtr2 2257  suc11 2341  relss 2480  cbvfo 2923  tfrlem1 2949  th3qlem1 3250  infsdomnn 3426  cflim 3704  ltexpq 3874  sup3 4511  projlem15 5207  spansnsst 5476

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

metamath.org