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

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
StepHypRef Expression
1 sylan9.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylan9.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
31, 2syl9 68 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 419 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator