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

Theorem sylan9r 509
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
sylan9r.1 (𝜑 → (𝜓𝜒))
sylan9r.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
sylan9r ((𝜃𝜑) → (𝜓𝜏))

Proof of Theorem sylan9r
StepHypRef Expression
1 sylan9r.1 . . 3 (𝜑 → (𝜓𝜒))
2 sylan9r.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2syl9r 78 . 2 (𝜃 → (𝜑 → (𝜓𝜏)))
43imp 407 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  spimt  2399  spimtOLD  2400  euim  2700  axprlem3  5322  limsssuc  7553  tfindsg  7563  findsg  7597  f1oweALT  7664  oaordi  8162  pssnn  8725  inf3lem2  9081  updjudhf  9349  cardlim  9390  ac10ct  9449  cardaleph  9504  cfub  9660  cfcoflem  9683  hsmexlem2  9838  zorn2lem7  9913  pwcfsdom  9994  grur1a  10230  genpcd  10417  supadd  11598  supmul  11602  zeo  12057  uzwo  12300  xrub  12695  iccsupr  12820  reuccatpfxs1lem  14098  climuni  14899  efgi2  18771  opnnei  21644  tgcn  21776  locfincf  22055  uffix  22445  alexsubALTlem2  22572  alexsubALT  22575  metrest  23049  causs  23816  ocin  28987  spanuni  29235  superpos  30045  bnj518  32044  3orel13  32831  trpredmintr  32954  frmin  32968  nndivsub  33689  bj-spimtv  34000  bj-snmoore  34286  cover2  34857  metf1o  34898  sn-axprlem3  38974  intabssd  39750  stoweidlem62  42213
  Copyright terms: Public domain W3C validator