Theorem syl9r 78

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 77	. 2 |- ( ph -> ( th -> ( ps -> ta ) ) )
4	3	com12 32	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  690  ax12v2  2049  ax12vOLD  2050  ax12vOLDOLD  2051  nfimdOLD  2226  fununi  5964  dfimafn  6245  funimass3  6333  isomin  6587  oneqmin  7005  tz7.48lem  7536  fisupg  8208  fiinfg  8405  trcl  8604  coflim  9083  coftr  9095  axdc3lem2  9273  konigthlem  9390  indpi  9729  nnsub  11059  2ndc1stc  21254  kgencn2  21360  tx1stc  21453  filuni  21689  fclscf  21829  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALT  21855  lpni  27332  dfimafnf  29436  dfon2lem6  31693  nodenselem8  31841  finixpnum  33394  heiborlem4  33613  lncvrelatN  35067  imbi13  38726  dfaimafn  41245  sgoldbeven3prm  41671