Theorem syl9 71

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 66	1 |- (ph -> (th -> (ps -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl9r 72  sylan9 517  sbequi 1598  hbsb4 1620  sbal1 1737  ralcom2 2244  ralcom2OLD 2245  vtoclegft 2356  reuss2 2870  reupick 2874  ordtr2 3708  ordtr2OLD 3709  suc11 3773  ssrelOLD 4076  ssrelrelOLD 4084  funimass4 4722  cbvfo 4861  onopriun 5118  tfrlem1 5119  omlimcl 5257  nneob 5312  th3qlem1 5373  infsdomnn 5625  imbi12 5838  cflim 6057  ltexpq 6232  sup3 7261  cvganz 8176  clm3i 8339  climaddlem3 8376  climmullem8 8387  reccnv 8479  gapm 9462  spwmo 9999  flimopn 10321  projlem15 10833  spansnss 11127  elres 13824  dfon2lem6 13854  uninqs 14340  supdef 14604  svs2 14829  mapdiscnlem 14870  cnvhmphb 14880  dualcat2 15133  intartar 15255  heiborlem32 15986  prtlem10 16265  pm11.71 16354

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

Copyright terms: Public domain