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  19.23t  1842  nfimd  1850  fununi  5484  dfimafn  5740  funimass3  5819  isomin  6028  oneqmin  6416  tz7.48lem  6896  fisupg  7560  trcl  7948  coflim  8430  coftr  8442  axdc3lem2  8620  konigthlem  8732  indpi  9076  nnsub  10360  2ndc1stc  19055  kgencn2  19130  tx1stc  19223  filuni  19458  fclscf  19598  alexsubALTlem2  19620  alexsubALTlem3  19621  alexsubALT  19623  lpni  23666  dfimafnf  25950  dfon2lem6  27601  nodenselem8  27829  finixpnum  28414  heiborlem4  28713  dfaimafn  30071  imbi13  31225  lncvrelatN  33425