MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9 Structured version   Unicode version

Theorem sylan9 650
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
StepHypRef Expression
1 sylan9.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylan9.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
31, 2syl9 71 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 429 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  sbal1OLD  2174  rspc2  3067  rspc3v  3071  trintss  4389  copsexg  4564  copsexgOLD  4565  chfnrn  5802  fvcofneq  5839  ffnfv  5856  f1elima  5963  onint  6395  peano5  6488  f1oweALT  6550  smoel2  6810  th3q  7197  pssnn  7519  fiint  7576  dffi2  7661  alephnbtwn  8229  cfcof  8431  zorn2lem7  8659  suplem1pr  9208  cau3lem  12825  divalglem8  13586  efgi  16195  elfrlmbasn0  18031  tx1stc  19064  fbunfip  19283  filuni  19299  ufileu  19333  rescncf  20314  shmodsi  24614  spanuni  24769  spansneleq  24795  mdi  25521  dmdi  25528  dmdi4  25533  funimass4f  25774  locfincmp  28417  ffnafv  29920
  Copyright terms: Public domain W3C validator