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

Theorem sylibrd 260
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 249 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3imtr4d  295  sbciegft  3807  opeldmd  5769  elreldm  5799  ordtr2  6229  ssimaex  6742  fliftfun  7054  isopolem  7087  isosolem  7089  ordsucss  7521  f1oweALT  7664  fnse  7818  brtpos  7892  issmo2  7977  seqomlem1  8077  omcl  8152  oecl  8153  oawordeulem  8170  oaass  8177  omordi  8182  omord  8184  odi  8195  oen0  8202  oeordi  8203  oeordsuc  8210  nnmcl  8228  nnecl  8229  nnmordi  8247  nnmord  8248  nnmwordri  8252  nnaordex  8254  swoord1  8310  ecopovtrn  8390  f1domg  8518  pw2f1olem  8610  domtriord  8652  mapen  8670  mapxpen  8672  mapunen  8675  nndomo  8701  inficl  8878  supmo  8905  infmo  8948  inf3lem6  9085  cantnflem1  9141  tcmin  9172  tcrank  9302  cardne  9383  cardlim  9390  cardsdomel  9392  carduni  9399  alephord  9490  cardinfima  9512  dfac5lem4  9541  infdif2  9621  cofsmo  9680  cfcoflem  9683  infpssrlem4  9717  infpssrlem5  9718  fin4en1  9720  isfin2-2  9730  enfin2i  9732  fin23lem27  9739  isf32lem12  9775  isf34lem6  9791  domtriomlem  9853  cardmin  9975  fpwwe2lem12  10052  inar1  10186  gruiun  10210  ltsonq  10380  prub  10405  reclem3pr  10460  mulcmpblnr  10482  mulgt0sr  10516  axpre-sup  10580  leltadd  11113  infm3  11589  peano5nni  11630  zextle  12044  prime  12052  uzin  12267  ublbneg  12322  zbtwnre  12335  mul2lt0bi  12485  xrre2  12553  xralrple  12588  xmulneg1  12652  supxrbnd  12711  supxrgtmnf  12712  fzrevral  12982  flge  13165  ceile  13207  modadd1  13266  modmul1  13282  modsumfzodifsn  13302  seqcl2  13378  facdiv  13637  hashss  13760  hash2exprb  13819  elfzelfzccat  13924  repswswrd  14136  cshf1  14162  cshwcsh2id  14180  rlim2lt  14844  rlim3  14845  o1lo1  14884  climshftlem  14921  o1co  14933  o1of2  14959  isercolllem2  15012  isercoll  15014  caucvgrlem2  15021  climcndslem2  15195  sqrt2irr  15592  dvds2lem  15612  dvdsle  15650  dvdsfac  15666  ltoddhalfle  15700  divalglem0  15734  ndvdsadd  15751  bitsinv1lem  15780  sadcaddlem  15796  dvdslegcd  15843  bezoutlem2  15878  bezoutlem4  15880  gcdzeq  15892  algcvga  15913  rpdvds  15994  cncongr1  16001  cncongr2  16002  prmind2  16019  isprm6  16048  rpexp  16054  eulerthlem2  16109  pclem  16165  pceulem  16172  pc2dvds  16205  fldivp1  16223  infpnlem1  16236  prmunb  16240  mrieqv2d  16900  plttr  17570  clatl  17716  issubg4  18238  gexdvds  18640  pgpssslw  18670  sylow2alem2  18674  efgs1b  18793  efgsfo  18796  lspindpi  19835  pf1ind  20448  psgnodpm  20662  psgndif  20676  obselocv  20802  mdetunilem9  21159  fiinbas  21490  bastg  21504  tgcl  21507  opnssneib  21653  clslp  21686  tgcnp  21791  iscnp4  21801  cncls2  21811  cncls  21812  cnntr  21813  cnpresti  21826  lmss  21836  lmcnp  21842  cmpsub  21938  tgcmp  21939  dfconn2  21957  t1connperf  21974  1stcfb  21983  1stcrest  21991  kgenss  22081  llycmpkgen2  22088  txdis  22170  qtoptop2  22237  kqt0lem  22274  isr0  22275  regr1lem2  22278  cmphaushmeo  22338  fbun  22378  ssfg  22410  fgtr  22428  ufildr  22469  cnpflf  22539  fclsnei  22557  flimfnfcls  22566  fclscmp  22568  ufilcmp  22570  cnpfcf  22579  alexsublem  22582  alexsubALTlem3  22587  alexsubALTlem4  22588  ptcmplem3  22592  tgphaus  22654  tgpt1  22655  tsmsres  22681  imasdsf1olem  22912  xblss2ps  22940  xblss2  22941  blsscls2  23043  metequiv2  23049  stdbdxmet  23054  nmoi  23266  reconn  23365  mulc1cncf  23442  cncfco  23444  iccpnfhmeo  23478  xrhmeo  23479  evth  23492  pi1grplem  23582  fgcfil  23803  ivthlem2  23982  ivthlem3  23983  ovolicc2lem4  24050  voliunlem1  24080  ioombl1lem4  24091  itg2gt0  24290  limcco  24420  lhop1  24540  tdeglem4  24583  plypf1  24731  coeeulem  24743  coeidlem  24756  coeid3  24759  plymul0or  24799  dvnply2  24805  plydivex  24815  vieta1lem2  24829  plyexmo  24831  aaliou3lem2  24861  ulmss  24914  ulmdvlem3  24919  iblulm  24924  sincosq2sgn  25014  sincosq3sgn  25015  sincosq4sgn  25016  logcnlem5  25156  dcubic  25351  amgm  25496  isnsqf  25640  mumullem2  25685  chtublem  25715  chtub  25716  fsumvma2  25718  vmasum  25720  dchrfi  25759  bposlem1  25788  bposlem3  25790  bposlem7  25794  lgsdir  25836  lgsquadlem2  25885  2sqlem8a  25929  2sqlem10  25932  dchrisum0flb  26014  pntpbnd1  26090  pntlemf  26109  pntlem3  26113  axeuclid  26677  uspgrushgr  26888  uspgrupgr  26889  usgruspgr  26891  usgr2pth  27473  crctcshwlkn0lem5  27520  wwlksnext  27599  wwlksnextsurj  27606  clwwlkccatlem  27695  clwlkclwwlkf  27714  clwwisshclwwslemlem  27719  lnon0  28503  normpyc  28851  ocsh  28988  ocorth  28996  ococss  28998  shsel2  29027  hsupss  29046  pjhth  29098  shlub  29119  cm2j  29325  lnfncnbd  29762  riesz1  29770  rnbra  29812  leopadd  29837  leopmuli  29838  hstles  29936  stge1i  29943  stle0i  29944  dmdbr5  30013  ssmd2  30017  superpos  30059  chcv1  30060  atoml2i  30088  chirredlem2  30096  atcvat3i  30101  mdsymlem5  30112  mdsymlem6  30113  sumdmdii  30120  sumdmdlem2  30124  isarchiofld  30818  sqsscirc2  31052  cnre2csqlem  31053  xrge0iifiso  31078  sigaclci  31291  omssubadd  31458  eulerpartlemb  31526  ballotlemimin  31663  ballotlem7  31693  subgrwlk  32277  cusgracyclt3v  32301  cvmlift2lem12  32459  fmlasucdisj  32544  dfon2lem8  32933  soseq  32994  segconeq  33369  ifscgr  33403  brofs2  33436  brifs2  33437  endofsegid  33444  dissneqlem  34504  rdgellim  34540  fvineqsneq  34576  tan2h  34766  matunitlindflem2  34771  poimirlem31  34805  poimir  34807  fzmul  34899  fdc  34903  incsequz2  34907  sstotbnd2  34935  sstotbnd3  34937  totbndbnd  34950  isexid2  35016  ispridl2  35199  mpobi123f  35323  riotasvd  35974  lsator0sp  36019  lssatle  36033  lshpset2N  36137  lkrlspeqN  36189  omllaw2N  36262  cmtbr3N  36272  lecmtN  36274  cvlcvr1  36357  cvrval4N  36432  cvrat3  36460  3noncolr2  36467  4noncolr3  36471  3dimlem3  36479  3dimlem3OLDN  36480  3dimlem4  36482  3dimlem4OLDN  36483  llncvrlpln  36576  lplncvrlvol  36634  snatpsubN  36768  linepsubN  36770  pmapjat1  36871  pclfinclN  36968  pl42N  37001  ltrneq2  37166  cdleme7aa  37260  cdleme18d  37313  cdleme21b  37344  trlord  37587  trlcoat  37741  dochkrshp  38404  lcfl8  38520  irrapxlem2  39300  pell14qrdich  39346  monotoddzz  39420  pw2f1ocnv  39514  iocinico  39698  nndomog  39777  harval3  39784  sbcim2g  40752  stoweidlem62  42228  elfzelfzlble  43402  eenglngeehlnmlem2  44623
  Copyright terms: Public domain W3C validator