Theorem sylan9 639

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
sylan9	|- ( ( ph /\ th ) -> ( ps -> ta ) )

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		sylan9.2	. . 3 |- ( th -> ( ch -> ta ) )
3	1, 2	syl9 68	. 2 |- ( ph -> ( th -> ( ps -> ta ) ) )
4	3	imp 419	1 |- ( ( ph /\ th ) -> ( ps -> ta ) )

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  sbequi  2116  sbal1  2184  rspc2  3025  rspc3v  3029  trintss  4286  copsexg  4410  onint  4742  peano5  4835  chfnrn  5808  ffnfv  5861  f1elima  5976  f1oweALT  6041  smoel2  6592  th3q  6980  pssnn  7294  fiint  7350  dffi2  7394  alephnbtwn  7916  cfcof  8118  zorn2lem7  8346  suplem1pr  8893  cau3lem  12121  divalglem8  12883  efgi  15314  tx1stc  17643  fbunfip  17862  filuni  17878  ufileu  17912  rescncf  18888  shmodsi  22852  spanuni  23007  spansneleq  23033  mdi  23759  dmdi  23766  dmdi4  23771  funimass4f  24005  locfincmp  26282  ffnafv  27910  sbequiNEW7  29294  sbal1NEW7  29328

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

This theorem depends on definitions:  df-bi 178  df-an 361