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

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

Proof of Theorem sylibrd
StepHypRef Expression
1 sylibrd.1 . 2
2 sylibrd.2 . . 3
32biimprd 223 . 2
41, 3syld 44 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr4d  268  sbciegft  3358  eqsbc3r  3389  ordtr2  4927  elreldm  5232  ssimaex  5938  fconstfvOLD  6134  fliftfun  6210  isopolem  6241  isosolem  6243  ordsucss  6653  f1oweALT  6784  fnse  6917  brtpos  6983  issmo2  7039  seqomlem1  7134  omcl  7205  oecl  7206  oawordeulem  7222  oaass  7229  omordi  7234  omord  7236  odi  7247  oen0  7254  oeordi  7255  oeordsuc  7262  nnmcl  7280  nnecl  7281  nnmordi  7299  nnmord  7300  nnmwordri  7304  nnaordex  7306  swoord1  7359  ecopovtrn  7433  f1domg  7555  pw2f1olem  7641  domtriord  7683  mapen  7701  mapxpen  7703  mapunen  7706  nndomo  7731  inficl  7905  supmo  7932  inf3lem6  8071  cantnflem1  8129  cantnflem1OLD  8152  tcmin  8193  tcrank  8323  cardne  8367  cardlim  8374  cardsdomel  8376  carduni  8383  alephord  8477  cardinfima  8499  dfac5lem4  8528  infdif2  8611  cofsmo  8670  cfcoflem  8673  infpssrlem4  8707  infpssrlem5  8708  fin4en1  8710  isfin2-2  8720  enfin2i  8722  fin23lem27  8729  isf32lem12  8765  isf34lem6  8781  domtriomlem  8843  cardmin  8960  fpwwe2lem12  9040  inar1  9174  gruiun  9198  ltsonq  9368  prub  9393  reclem3pr  9448  mulcmpblnr  9469  mulgt0sr  9503  axpre-sup  9567  leltadd  10061  infm3  10527  peano5nni  10564  zextle  10961  prime  10968  uzindOLD  10982  uzin  11142  ublbneg  11195  zbtwnre  11209  xrre2  11400  xralrple  11433  xmulneg1  11490  supxrbnd  11549  supxrgtmnf  11550  fzrevral  11792  flge  11942  ceile  11976  modadd1  12033  modmul1  12040  seqcl2  12125  facdiv  12365  hashss  12474  hash2prb  12517  elfzelfzccat  12598  repswswrd  12756  cshwcsh2id  12796  rlim2lt  13320  rlim3  13321  o1lo1  13360  climshftlem  13397  o1co  13409  o1of2  13435  isercolllem2  13488  isercoll  13490  caucvgrlem2  13497  climcndslem2  13662  sqrt2irr  13982  dvds2lem  13996  dvdsle  14031  dvdsfac  14041  divalglem0  14051  ndvdsadd  14066  bitsinv1lem  14091  sadcaddlem  14107  dvdslegcd  14154  bezoutlem2  14177  bezoutlem4  14179  gcdeq  14190  algcvga  14208  prmind2  14228  isprm6  14250  rpexp  14261  rpdvds  14265  eulerthlem2  14312  pclem  14362  pceulem  14369  pc2dvds  14402  fldivp1  14416  infpnlem1  14428  prmunb  14432  mrieqv2d  15036  plttr  15600  clatl  15746  issubg4  16220  gexdvds  16604  pgpssslw  16634  sylow2alem2  16638  efgs1b  16754  efgsfo  16757  lspindpi  17778  pf1ind  18391  psgnodpm  18624  psgndif  18638  obselocv  18759  mdetunilem9  19122  fiinbas  19453  bastg  19467  tgcl  19471  opnssneib  19616  clslp  19649  tgcnp  19754  iscnp4  19764  cncls2  19774  cncls  19775  cnntr  19776  cnpresti  19789  lmss  19799  lmcnp  19805  cmpsub  19900  tgcmp  19901  dfcon2  19920  t1conperf  19937  1stcfb  19946  1stcrest  19954  kgenss  20044  llycmpkgen2  20051  txdis  20133  qtoptop2  20200  kqt0lem  20237  isr0  20238  regr1lem2  20241  cmphaushmeo  20301  fbun  20341  ssfg  20373  fgtr  20391  ufildr  20432  cnpflf  20502  fclsnei  20520  flimfnfcls  20529  fclscmp  20531  ufilcmp  20533  cnpfcf  20542  alexsublem  20544  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem3  20554  tgphaus  20615  tgpt1  20616  tsmsresOLD  20645  tsmsres  20646  imasdsf1olem  20876  xblss2ps  20904  xblss2  20905  blsscls2  21007  metequiv2  21013  stdbdxmet  21018  nmoi  21235  reconn  21333  mulc1cncf  21409  cncfco  21411  iccpnfhmeo  21445  xrhmeo  21446  evth  21459  pi1grplem  21549  fgcfil  21710  ivthlem2  21864  ivthlem3  21865  ovolicc2lem4  21931  voliunlem1  21960  ioombl1lem4  21971  itg2gt0  22167  limcco  22297  lhop1  22415  tdeglem4  22458  plypf1  22609  coeeulem  22621  coeidlem  22634  coeid3  22637  plymul0or  22677  dvnply2  22683  plydivex  22693  vieta1lem2  22707  plyexmo  22709  aaliou3lem2  22739  ulmss  22792  ulmdvlem3  22797  iblulm  22802  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  logcnlem5  23027  dcubic  23177  amgm  23320  isnsqf  23409  mumullem2  23454  chtublem  23486  chtub  23487  fsumvma2  23489  vmasum  23491  dchrfi  23530  bposlem1  23559  bposlem3  23561  bposlem7  23565  lgsdir  23605  lgsquadlem2  23630  2sqlem8a  23646  2sqlem10  23649  dchrisum0flb  23695  pntpbnd1  23771  pntlemf  23790  pntlem3  23794  axeuclid  24266  umisuhgra  24327  uslisushgra  24363  uslisumgra  24364  usisuslgra  24365  constr3trl  24659  constr3pth  24660  wwlknext  24724  wwlkextsur  24731  clwwisshclwwlem1  24805  vdusgraval  24907  gxcl  25267  isexid2  25327  lnon0  25713  normpyc  26063  ocsh  26201  ocorth  26209  ococss  26211  shsel2  26240  hsupss  26259  pjhth  26311  shlub  26332  cm2j  26538  lnfncnbd  26976  riesz1  26984  rnbra  27026  leopadd  27051  leopmuli  27052  hstles  27150  stge1i  27157  stle0i  27158  dmdbr5  27227  ssmd2  27231  superpos  27273  chcv1  27274  atoml2i  27302  chirredlem2  27310  atcvat3i  27315  mdsymlem5  27326  mdsymlem6  27327  sumdmdii  27334  sumdmdlem2  27338  mul2lt0bi  27569  isarchiofld  27807  sqsscirc2  27891  cnre2csqlem  27892  xrge0iifiso  27917  sigaclci  28132  eulerpartlemb  28307  ballotlemimin  28444  ballotlem7  28474  cvmlift2lem12  28759  dfon2lem8  29222  soseq  29334  segconeq  29660  ifscgr  29694  brofs2  29727  brifs2  29728  endofsegid  29735  tan2h  30047  fzmul  30233  fdc  30238  incsequz2  30242  sstotbnd2  30270  sstotbnd3  30272  totbndbnd  30285  ispridl2  30435  mpt2bi123f  30571  irrapxlem2  30759  pell14qrdich  30805  monotoddzz  30879  pw2f1ocnv  30979  iocinico  31179  stoweidlem62  31844  elfzelfzlble  32337  sbcim2g  33309  riotasvd  34687  lsator0sp  34726  lssatle  34740  lshpset2N  34844  lkrlspeqN  34896  omllaw2N  34969  cmtbr3N  34979  lecmtN  34981  cvlcvr1  35064  cvrval4N  35138  cvrat3  35166  3noncolr2  35173  4noncolr3  35177  3dimlem3  35185  3dimlem3OLDN  35186  3dimlem4  35188  3dimlem4OLDN  35189  llncvrlpln  35282  lplncvrlvol  35340  snatpsubN  35474  linepsubN  35476  pmapjat1  35577  pclfinclN  35674  pl42N  35707  ltrneq2  35872  cdleme7aa  35967  cdleme18d  36020  cdleme21b  36052  trlord  36295  trlcoat  36449  dochkrshp  37113  lcfl8  37229
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