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

Theorem sylan9r 687
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 75 . 2 (𝜃 → (𝜑 → (𝜓𝜏)))
43imp 443 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  spimt  2240  limsssuc  6919  tfindsg  6929  findsg  6962  f1oweALT  7020  oaordi  7490  pssnn  8040  inf3lem2  8386  cardlim  8658  ac10ct  8717  cardaleph  8772  cfub  8931  cfcoflem  8954  hsmexlem2  9109  zorn2lem7  9184  pwcfsdom  9261  grur1a  9497  genpcd  9684  supadd  10838  supmul  10842  zeo  11295  uzwo  11583  xrub  11970  iccsupr  12093  reuccats1lem  13277  climuni  14077  efgi2  17907  opnnei  20676  tgcn  20808  locfincf  21086  uffix  21477  alexsubALTlem2  21604  alexsubALT  21607  metrest  22080  causs  22822  ocin  27345  spanuni  27593  superpos  28403  bnj518  30016  3orel13  30659  trpredmintr  30781  frmin  30789  nndivsub  31432  bj-spimtv  31711  cover2  32474  metf1o  32517  intabssd  36731  stoweidlem62  38752  reuccatpfxs1lem  40094
  Copyright terms: Public domain W3C validator