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 1228  hbsb4 1248  sbal1 1346  ralcom2 1776  reuss2 2275  reupick 2279  ordtr2 3002  suc11 3093  ssrel 3247  funimass4 3763  cbvfo 3885  tfrlem1 3911  omlimcl 4209  nneob 4255  th3qlem1 4314  infsdomnn 4532  cflim 4909  ltexpq 5080  sup3 6052  cvganz 6924  clm3 7079  climaddlem3 7116  climmullem8 7127  reccnv 7218  spwmo 8656  projlem15 9200  spansnsst 9494  uninqs 10441  mapdiscn 10511  cnvhmphb 10526

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

Copyright terms: Public domain