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

Theorem syld3an3 1273
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an3.1
syld3an3.2
Assertion
Ref Expression
syld3an3

Proof of Theorem syld3an3
StepHypRef Expression
1 simp1 996 . 2
2 simp2 997 . 2
3 syld3an3.1 . 2
4 syld3an3.2 . 2
51, 2, 3, 4syl3anc 1228 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  syld3an1  1274  syld3an2  1275  brelrng  5237  resin  5842  moriotass  6286  omwordri  7240  oewordri  7260  gchaleph2  9071  gruf  9210  nnncan1  9878  lediv1  10432  lemuldiv  10449  suprfinzcl  11003  supxrbnd  11549  bcval4  12385  ccatval3  12597  ccatfv0  12601  ccatval1lsw  12602  lswccatn0lsw  12607  2swrd1eqwrdeq  12679  2swrd2eqwrdeq  12891  znnenlem  13945  dvdsmultr1  14019  dvdssub2  14023  ndvdsadd  14066  mrcsscl  15017  latnle  15715  latabs1  15717  latabs2  15718  latj4rot  15732  grpsubf  16117  grpinvsub  16120  grpnpcan  16130  subgsubcl  16212  qussub  16261  ghmsub  16275  odhash3  16596  dvrcl  17335  unitdvcl  17336  abvsubtri  17484  lspsntrim  17744  lply1binomsc  18349  frlmsslss2  18805  frlmsslss2OLD  18806  lindsmm  18863  smadiadetglem2  19174  m2cpm  19242  m2cpminvid  19254  pmatcollpwscmat  19292  mp2pm2mp  19312  cpmidgsum  19369  cpmadugsumfi  19378  basgen2  19491  opnneiss  19619  restlp  19684  nmtri  21145  sincosq1lem  22890  logrec  23151  1pthon2v  24595  grpodivinv  25246  grpoinvdiv  25247  grpodivf  25248  gxsuc  25274  vcnegsubdi2  25468  vcsub4  25469  nvmval2  25538  nvsubadd  25550  nvaddsub4  25556  nvnncan  25558  nvpi  25569  nvmtri  25574  nvabs  25576  4ipval2  25618  ipval3  25619  isblo2  25698  blof  25700  nmblore  25701  nmlnoubi  25711  nmlnogt0  25712  shsubcl  26138  unopadj  26838  atexch  27300  atcvatlem  27304  ogrpsublt  27712  ind1  28032  inelsiga  28135  mrsubcv  28870  mrsubvr  28871  ghomf1olem  29034  btwnconn2  29752  ismtybnd  30303  mzprename  30682  pell14qrdivcl  30801  pwssplit4  31035  iocmbl  31180  dvconstbi  31239  dvbdfbdioolem1  31725  ibliccsinexp  31749  stoweidlem22  31804  fourierdlem42  31931  lkrlsp2  34828  opcon2b  34922  opltcon2b  34931  oldmm3N  34944  oldmm4  34945  oldmj3  34948  oldmj4  34949  cmt2N  34975  cmt4N  34977  atleneN  35158  lplnri2N  35278  cdlema2N  35516  pmapojoinN  35692  ltrncnvatb  35862  trlval2  35888  trljat1  35891  cdleme18c  36018  cdleme19c  36031  cdlemeiota  36311  trlcocnv  36446  tendoplco2  36505  cdlemk6  36563  cdlemk7u  36596  cdlemk22  36619  cdlemk24-3  36629  cdlemkid2  36650  cdlemk11ta  36655  cdlemk11tc  36671  cdlemk47  36675  cdlemk52  36680  tendocnv  36748  dibelval1st1  36877  dibelval1st2N  36878  dihord2pre2  36953
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  df-3an 975
  Copyright terms: Public domain W3C validator