Theorem syl9 77

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof 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.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl9.2	. . 3 |- ( th -> ( ch -> ta ) )
3	2	a1i 11	. 2 |- ( ph -> ( th -> ( ch -> ta ) ) )
4	1, 3	syl5d 73	1 |- ( ph -> ( th -> ( ps -> ta ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl9r  78  com23  86  sylan9  689  nfimt  1821  19.21tOLDOLD  2074  19.21t-1OLD  2212  ax13lem1  2248  ax13lem2  2296  axc11n  2307  axc11nOLD  2308  axc11nOLDOLD  2309  axc11nALT  2310  sbequi  2375  reuss2  3907  reupick  3911  elres  5435  ordtr2  5768  suc11  5831  funimass4  6247  fliftfun  6562  omlimcl  7658  nneob  7732  rankwflemb  8656  cflm  9072  domtriomlem  9264  grothomex  9651  sup3  10980  caubnd  14098  fbflim2  21781  ellimc3  23643  usgruspgrb  26076  usgredgsscusgredg  26355  3cyclfrgrrn1  27149  dfon2lem6  31693  opnrebl2  32316  axc11n11r  32673  stdpc5t  32814  wl-ax13lem1  33287  diaintclN  36347  dibintclN  36456  dihintcl  36633  pm11.71  38597  axc11next  38607