Theorem syl9r 73

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 72	. 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  670  ax12v2  1952  ax12vOLD  1953  ax12vOLDOLD  1954  19.23tOLD  2012  nfimd  2020  fununi  5659  dfimafn  5928  funimass3  6013  isomin  6246  oneqmin  6651  tz7.48lem  7176  fisupg  7837  fiinfg  8033  trcl  8230  coflim  8709  coftr  8721  axdc3lem2  8899  konigthlem  9011  indpi  9350  nnsub  10670  2ndc1stc  20543  kgencn2  20649  tx1stc  20742  filuni  20978  fclscf  21118  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALT  21144  lpni  25990  dfimafnf  28309  dfon2lem6  30505  nodenselem8  30648  finixpnum  31994  heiborlem4  32210  lncvrelatN  33417  imbi13  36947  dfaimafn  38812