Theorem syl9 57

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

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 8	. 2 |- (ph -> (th -> (ch -> ta)))
3		syl9.1	. 2 |- (ph -> (ps -> ch))
4	2, 3	syl5d 55	1 |- (ph -> (th -> (ps -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl9r 58  sbequi 1230  hbsb4 1250  sbal1 1348  ralcom2 1779  reuss2 2278  reupick 2282  ordtr2 3008  suc11 3099  ssrel 3253  funimass4 3769  cbvfo 3891  tfrlem1 3917  omlimcl 4215  nneob 4261  th3qlem1 4320  infsdomnn 4541  cflim 4921  ltexpq 5092  sup3 6054  cvganz 6924  clm3 7079  climaddlem3 7116  climmullem8 7127  reccnv 7218  spwmo 8652  projlem15 9195  spansnsst 9489  uninqs 10436  mapdiscn 10497  cnvhmphb 10512

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

Copyright terms: Public domain