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

Theorem sylan9 663
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 73 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 431 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  rspc2  3158  rspc3v  3162  trintss  4513  copsexg  4687  chfnrn  5993  fvcofneq  6030  ffnfv  6049  f1elima  6164  onint  6622  peano5  6716  f1oweALT  6777  smoel2  7082  pssnn  7790  fiint  7848  dffi2  7937  alephnbtwn  8502  cfcof  8704  zorn2lem7  8932  suplem1pr  9477  addsrpr  9499  mulsrpr  9500  cau3lem  13417  divalglem8  14380  efgi  17369  elfrlmbasn0  19325  locfincmp  20541  tx1stc  20665  fbunfip  20884  filuni  20900  ufileu  20934  rescncf  21929  shmodsi  27042  spanuni  27197  spansneleq  27223  mdi  27948  dmdi  27955  dmdi4  27960  funimass4f  28234  bj-ax89  31276  poimirlem32  31972  ffnafv  38673
  Copyright terms: Public domain W3C validator