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

Theorem sylan9r 504
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 395 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  spimt  2359  limsssuc  7252  tfindsg  7262  findsg  7295  f1oweALT  7354  oaordi  7835  pssnn  8389  inf3lem2  8745  updjudhf  9012  cardlim  9053  ac10ct  9112  cardaleph  9167  cfub  9328  cfcoflem  9351  hsmexlem2  9506  zorn2lem7  9581  pwcfsdom  9662  grur1a  9898  genpcd  10085  supadd  11249  supmul  11253  zeo  11715  uzwo  11957  xrub  12349  iccsupr  12474  reuccats1lemOLD  13739  reuccatpfxs1lem  13774  climuni  14582  efgi2  18416  opnnei  21218  tgcn  21350  locfincf  21628  uffix  22018  alexsubALTlem2  22145  alexsubALT  22148  metrest  22622  causs  23389  ocin  28632  spanuni  28880  superpos  29690  bnj518  31425  3orel13  32065  trpredmintr  32195  frmin  32207  nndivsub  32916  bj-spimtv  33174  bj-snmoore  33517  cover2  33952  metf1o  33994  intabssd  38615  stoweidlem62  40940
  Copyright terms: Public domain W3C validator