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

Theorem sylbird 235
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbird.1
sylbird.2
Assertion
Ref Expression
sylbird

Proof of Theorem sylbird
StepHypRef Expression
1 sylbird.1 . . 3
21biimprd 223 . 2
3 sylbird.2 . 2
42, 3syld 44 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr3d  267  ceqex  3230  eqreu  3291  sotr2  4834  ordtr3  4928  ordintdif  4932  sossfld  5459  tz6.12i  5891  suppssrOLD  6021  soisoi  6224  ov3  6439  tfindsg  6695  tfindsg2  6696  nnsuc  6717  findsg  6727  suppssr  6950  tfrlem9  7073  oe0lem  7182  oa00  7227  omwordi  7239  om00  7243  omass  7248  oelim2  7263  oeoa  7265  oeoe  7267  nnmwordi  7303  swoso  7361  dom2lem  7575  onsdominel  7686  f1finf1o  7766  cantnfp1lem3  8120  cantnfp1  8121  cantnflem1  8129  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  cantnflem1OLD  8152  rankr1ai  8237  rankval3b  8265  harcard  8380  infxpenlem  8412  alephnbtwn  8473  alephinit  8497  infxp  8616  cofsmo  8670  infpssALT  8714  fin23lem24  8723  fin56  8794  ttukeylem6  8915  ficard  8961  alephval2  8968  fpwwe2lem8  9036  fpwwe2  9042  gchcda1  9055  pwfseqlem3  9059  pwfseqlem4a  9060  pwfseqlem4  9061  gchpwdom  9069  tskss  9157  inar1  9174  gruss  9195  gruurn  9197  ltsonq  9368  distrlem4pr  9425  sqgt0sr  9504  map2psrpr  9508  letric  9706  renegcli  9903  mulge0b  10437  nnge1  10587  0mnnnnn0  10853  nn0lt2  10952  zneo  10970  uzind2  10980  fzind  10987  nn0ind-raph  10989  uzwo  11173  uzwoOLD  11174  nn01to3  11204  zbtwnre  11209  rpnnen1lem5  11241  xrletri  11386  qsqueeze  11429  difreicc  11681  elfzmlbp  11815  difelfznle  11818  elfzodifsumelfzo  11882  ssfzo12  11905  elfzonelfzo  11912  flflp1  11944  fleqceilz  11981  om2uzf1oi  12064  facdiv  12365  facwordi  12367  bcpasc  12399  hashdom  12447  hashle00  12465  lswcl  12589  ccatsymb  12600  ccatval1lsw  12602  swrdspsleq  12673  swrdlsw  12677  swrdswrdlem  12684  swrdccatin1  12708  swrdccatin12lem3  12715  repswswrd  12756  cshwidx0  12776  cshwcsh2id  12796  limsupbnd1  13305  lo1bdd2  13347  addcn2  13416  mulcn2  13418  o1rlimmul  13441  lo1add  13449  lo1mul  13450  rlimno1  13476  znnenlem  13945  ruclem3  13966  odd2np1  14046  bitsfzo  14085  prmn2uzge3  14237  pcdvdsb  14392  pcaddlem  14407  infpnlem1  14428  prmunb  14432  vdwlem9  14507  vdwnnlem3  14515  ramcl  14547  cshwshash  14589  setcmon  15414  setcepi  15415  setciso  15418  ghmf1  16295  sylow2alem2  16638  sylow2blem3  16642  qusabl  16871  lt6abl  16897  cyggexb  16901  gsumcom2  17003  imasring  17268  f1rhm0to0  17389  drnginvrcl  17413  drnginvrl  17415  drnginvrr  17416  subrgdvds  17443  lsmelval2  17731  quscrng  17888  mplsubrglem  18100  mplsubrglemOLD  18101  gsummoncoe1  18346  xrsdsreclblem  18464  obs2ss  18760  obslbs  18761  mp2pm2mplem4  19310  chfacfisf  19355  chfacfisfcpmat  19356  cayleyhamilton1  19393  cmpsublem  19899  cmpsub  19900  1stccnp  19963  locfincf  20032  txhaus  20148  xkohaus  20154  ufilss  20406  cfinufil  20429  fmfnfmlem1  20455  hausflim  20482  fclscf  20526  alexsubb  20546  qustgplem  20619  prdsbl  20994  metss2lem  21014  nghmcn  21252  cfil3i  21708  cmetcaulem  21727  minveclem4  21847  ovolgelb  21891  ovolunnul  21911  ovoliun  21916  ovoliunnul  21918  ovolicc2lem2  21929  iundisj2  21959  voliunlem3  21962  rolle  22391  dvlip  22394  lhop1lem  22414  lhop2  22416  dvfsumrlim  22432  deg1ge  22499  coeeulem  22621  dgrco  22672  radcnvlt1  22813  psercnlem1  22820  logcnlem2  23024  logcnlem3  23025  cxpeq  23131  angpined  23161  efrlim  23299  basellem2  23355  ppieq0  23450  mumullem2  23454  chpeq0  23483  chteq0  23484  chtub  23487  fsumvma  23488  dchrptlem1  23539  bposlem6  23564  lgseisenlem2  23625  2sqlem6  23644  dchrisum0lem1  23701  pntrsumbnd2  23752  pntlem3  23794  colinearalg  24213  eengtrkg  24288  wlkv0  24760  0clwlk  24765  clwwlkgt0  24771  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem1  24787  nbhashuvtx1  24915  dvrunz  25435  blocni  25720  ubthlem1  25786  minvecolem4  25796  shmodsi  26307  atcvati  27305  atcvat2i  27306  chirredlem4  27312  atmd2  27319  sumdmdlem  27337  addltmulALT  27365  iundisj2f  27449  iundisj2fi  27602  rngurd  27778  dmgmaddn0  28565  lgamucov  28580  erdszelem9  28643  rdgprc  29227  soseq  29334  cgrsub  29695  btwnxfr  29706  lineext  29726  linecgr  29731  btwnconn1lem4  29740  btwnconn1lem5  29741  btwnconn1lem6  29742  btwnconn1lem8  29744  btwnconn1lem11  29747  ltflcei  30043  ftc1anclem5  30094  heiborlem6  30312  grpokerinj  30347  isdmn3  30471  dmncan1  30473  pellexlem1  30765  pellexlem6  30770  imasgim  31048  radcnvrat  31195  nzss  31222  zm1nn  32325  lesubnn0  32326  2ffzoeq  32341  usgra2pthspth  32351  lmod0rng  32674  0ring1eq0  32678  lidldomn1  32727  rngciso  32790  rngcisoOLD  32802  ringciso  32841  ringcisoOLD  32865  ztprmneprm  32936  lincresunit3  33082  aacllem  33216  l1cvpat  34779  atnle  35042  cvlexch3  35057  cvlexch4N  35058  cvlatexchb1  35059  cvrat2  35153  atlelt  35162  3dimlem4a  35187  3dimlem4OLDN  35189  ps-1  35201  ps-2  35202  4atlem10  35330  4atlem11  35333  4atlem12  35336  cdleme11c  35986  cdleme21c  36053  cdlemg6d  36347  trlcoat  36449  tendoid0  36551  cdleml3N  36704  dia2dimlem7  36797
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
  Copyright terms: Public domain W3C validator