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:  sbal1OLD  2189  rspc2  3217  rspc3v  3221  trintss  4551  copsexg  4727  copsexgOLD  4728  chfnrn  5985  fvcofneq  6022  ffnfv  6040  f1elima  6152  onint  6603  peano5  6696  f1oweALT  6760  smoel2  7026  pssnn  7730  fiint  7788  dffi2  7874  alephnbtwn  8443  cfcof  8645  zorn2lem7  8873  suplem1pr  9421  addsrpr  9443  mulsrpr  9444  cau3lem  13138  divalglem8  13908  efgi  16528  elfrlmbasn0  18558  tx1stc  19881  fbunfip  20100  filuni  20116  ufileu  20150  rescncf  21131  shmodsi  25971  spanuni  26126  spansneleq  26152  mdi  26878  dmdi  26885  dmdi4  26890  funimass4f  27135  locfincmp  29765  ffnafv  31680  bj-ax89  33197
  Copyright terms: Public domain W3C validator