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

Theorem sylan9 640
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 69 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 420 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  sbequiOLD  2118  sbal1  2209  rspc2  3063  rspc3v  3067  trintss  4343  copsexg  4471  onint  4804  peano5  4897  chfnrn  5870  ffnfv  5923  f1elima  6038  f1oweALT  6103  smoel2  6654  th3q  7042  pssnn  7356  fiint  7412  dffi2  7457  alephnbtwn  7983  cfcof  8185  zorn2lem7  8413  suplem1pr  8960  cau3lem  12189  divalglem8  12951  efgi  15382  tx1stc  17713  fbunfip  17932  filuni  17948  ufileu  17982  rescncf  18958  shmodsi  22922  spanuni  23077  spansneleq  23103  mdi  23829  dmdi  23836  dmdi4  23841  funimass4f  24075  locfincmp  26422  ffnafv  28049  sbequiNEW7  29677  sbal1NEW7  29713
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 179  df-an 362
  Copyright terms: Public domain W3C validator