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

Theorem sylan9r 510
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 408 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  3orel13  1488  spimt  2385  euim  2614  axprlem3  5384  limsssuc  7790  tfindsg  7801  findsg  7840  f1oweALT  7909  oaordi  8497  pssnn  9118  pssnnOLD  9215  inf3lem2  9573  updjudhf  9875  cardlim  9916  ac10ct  9978  cardaleph  10033  cfub  10193  cfcoflem  10216  hsmexlem2  10371  zorn2lem7  10446  pwcfsdom  10527  grur1a  10763  genpcd  10950  supadd  12131  supmul  12135  zeo  12597  uzwo  12844  xrub  13240  iccsupr  13368  reuccatpfxs1lem  14643  climuni  15443  efgi2  19515  opnnei  22494  tgcn  22626  locfincf  22905  uffix  23295  alexsubALTlem2  23422  alexsubALT  23425  metrest  23903  causs  24685  ocin  30287  spanuni  30535  superpos  31345  bnj518  33562  nndivsub  34982  bj-spimtv  35312  bj-snmoore  35634  cover2  36223  metf1o  36264  sn-axprlem3  40689  intabssd  41883  stoweidlem62  44393  pgindnf  47251
  Copyright terms: Public domain W3C validator