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

Theorem sylan9 657
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-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:  rspc2  3218  rspc3v  3222  trintss  4566  copsexg  4741  copsexgOLD  4742  chfnrn  5999  fvcofneq  6040  ffnfv  6058  f1elima  6172  onint  6629  peano5  6722  f1oweALT  6783  smoel2  7052  pssnn  7757  fiint  7815  dffi2  7901  alephnbtwn  8469  cfcof  8671  zorn2lem7  8899  suplem1pr  9447  addsrpr  9469  mulsrpr  9470  cau3lem  13199  divalglem8  14070  efgi  16864  elfrlmbasn0  18923  locfincmp  20153  tx1stc  20277  fbunfip  20496  filuni  20512  ufileu  20546  rescncf  21527  shmodsi  26434  spanuni  26589  spansneleq  26615  mdi  27341  dmdi  27348  dmdi4  27353  funimass4f  27622  ffnafv  32459  bj-ax89  34381
  Copyright terms: Public domain W3C validator