Theorem syl9r 72

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl9r

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		syl9r.2	. . 3 |- ( th -> ( ch -> ta ) )
3	1, 2	syl9 71	. 2 |- ( ph -> ( th -> ( ps -> ta ) ) )
4	3	com12 31	1 |- ( th -> ( ph -> ( 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:  sylan9r  658  ax12v  1804  19.23t  1856  nfimd  1864  fununi  5653  dfimafn  5915  funimass3  5996  isomin  6220  oneqmin  6619  tz7.48lem  7106  fisupg  7767  trcl  8158  coflim  8640  coftr  8652  axdc3lem2  8830  konigthlem  8942  indpi  9284  nnsub  10573  2ndc1stc  19734  kgencn2  19809  tx1stc  19902  filuni  20137  fclscf  20277  alexsubALTlem2  20299  alexsubALTlem3  20300  alexsubALT  20302  lpni  24873  dfimafnf  27162  dfon2lem6  28813  nodenselem8  29041  finixpnum  29631  heiborlem4  29929  dfaimafn  31733  imbi13  32378  lncvrelatN  34586