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

Theorem syl2and 483
Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
syl2and.1
syl2and.2
syl2and.3
Assertion
Ref Expression
syl2and

Proof of Theorem syl2and
StepHypRef Expression
1 syl2and.1 . 2
2 syl2and.2 . . 3
3 syl2and.3 . . 3
42, 3sylan2d 482 . 2
51, 4syland 481 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  anim12d  563  dffi3  7911  cflim2  8664  axpre-sup  9567  xle2add  11480  fzen  11732  rpmulgcd2  14246  pcqmul  14377  plttr  15600  pospo  15603  lublecllem  15618  latjlej12  15697  latmlem12  15713  cygabl  16893  hausnei2  19854  uncmp  19903  itgsubst  22450  dvdsmulf1o  23470  2sqlem8a  23646  axcontlem9  24275  usg2wotspth  24884  numclwlk1lem2f1  25094  shintcli  26247  cvntr  27211  cdj3i  27360  heicant  30049  itg2addnc  30069  initoeu1  32617  termoeu1  32624  bj-bary1  34681  dihmeetlem1N  37017
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 185  df-an 371
  Copyright terms: Public domain W3C validator