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  3805  opeldmd  5768  elreldm  5798  ordtr2  6228  ssimaex  6741  fliftfun  7054  isopolem  7087  isosolem  7089  ordsucss  7522  f1oweALT  7662  fnse  7816  brtpos  7890  issmo2  7975  seqomlem1  8075  omcl  8150  oecl  8151  oawordeulem  8169  oaass  8176  omordi  8181  omord  8183  odi  8194  oen0  8201  oeordi  8202  oeordsuc  8209  nnmcl  8227  nnecl  8228  nnmordi  8246  nnmord  8247  nnmwordri  8251  nnaordex  8253  swoord1  8309  ecopovtrn  8389  f1domg  8517  pw2f1olem  8609  domtriord  8651  mapen  8669  mapxpen  8671  mapunen  8674  nndomo  8700  inficl  8877  supmo  8904  infmo  8947  inf3lem6  9084  cantnflem1  9140  tcmin  9171  tcrank  9301  cardne  9382  cardlim  9389  cardsdomel  9391  carduni  9398  alephord  9489  cardinfima  9511  dfac5lem4  9540  infdif2  9620  cofsmo  9679  cfcoflem  9682  infpssrlem4  9716  infpssrlem5  9717  fin4en1  9719  isfin2-2  9729  enfin2i  9731  fin23lem27  9738  isf32lem12  9774  isf34lem6  9790  domtriomlem  9852  cardmin  9974  fpwwe2lem12  10051  inar1  10185  gruiun  10209  ltsonq  10379  prub  10404  reclem3pr  10459  mulcmpblnr  10481  mulgt0sr  10515  axpre-sup  10579  leltadd  11112  infm3  11588  peano5nni  11629  zextle  12043  prime  12051  uzin  12266  ublbneg  12321  zbtwnre  12334  mul2lt0bi  12483  xrre2  12551  xralrple  12586  xmulneg1  12650  supxrbnd  12709  supxrgtmnf  12710  fzrevral  12980  flge  13163  ceile  13205  modadd1  13264  modmul1  13280  modsumfzodifsn  13300  seqcl2  13376  facdiv  13635  hashss  13758  hash2exprb  13817  elfzelfzccat  13922  repswswrd  14134  cshf1  14160  cshwcsh2id  14178  rlim2lt  14842  rlim3  14843  o1lo1  14882  climshftlem  14919  o1co  14931  o1of2  14957  isercolllem2  15010  isercoll  15012  caucvgrlem2  15019  climcndslem2  15193  sqrt2irr  15590  dvds2lem  15610  dvdsle  15648  dvdsfac  15664  ltoddhalfle  15698  divalglem0  15732  ndvdsadd  15749  bitsinv1lem  15778  sadcaddlem  15794  dvdslegcd  15841  bezoutlem2  15876  bezoutlem4  15878  gcdzeq  15890  algcvga  15911  rpdvds  15992  cncongr1  15999  cncongr2  16000  prmind2  16017  isprm6  16046  rpexp  16052  eulerthlem2  16107  pclem  16163  pceulem  16170  pc2dvds  16203  fldivp1  16221  infpnlem1  16234  prmunb  16238  mrieqv2d  16898  plttr  17568  clatl  17714  issubg4  18236  gexdvds  18638  pgpssslw  18668  sylow2alem2  18672  efgs1b  18791  efgsfo  18794  lspindpi  19833  pf1ind  20446  psgnodpm  20660  psgndif  20674  obselocv  20800  mdetunilem9  21157  fiinbas  21488  bastg  21502  tgcl  21505  opnssneib  21651  clslp  21684  tgcnp  21789  iscnp4  21799  cncls2  21809  cncls  21810  cnntr  21811  cnpresti  21824  lmss  21834  lmcnp  21840  cmpsub  21936  tgcmp  21937  dfconn2  21955  t1connperf  21972  1stcfb  21981  1stcrest  21989  kgenss  22079  llycmpkgen2  22086  txdis  22168  qtoptop2  22235  kqt0lem  22272  isr0  22273  regr1lem2  22276  cmphaushmeo  22336  fbun  22376  ssfg  22408  fgtr  22426  ufildr  22467  cnpflf  22537  fclsnei  22555  flimfnfcls  22564  fclscmp  22566  ufilcmp  22568  cnpfcf  22577  alexsublem  22580  alexsubALTlem3  22585  alexsubALTlem4  22586  ptcmplem3  22590  tgphaus  22652  tgpt1  22653  tsmsres  22679  imasdsf1olem  22910  xblss2ps  22938  xblss2  22939  blsscls2  23041  metequiv2  23047  stdbdxmet  23052  nmoi  23264  reconn  23363  mulc1cncf  23440  cncfco  23442  iccpnfhmeo  23476  xrhmeo  23477  evth  23490  pi1grplem  23580  fgcfil  23801  ivthlem2  23980  ivthlem3  23981  ovolicc2lem4  24048  voliunlem1  24078  ioombl1lem4  24089  itg2gt0  24288  limcco  24418  lhop1  24538  tdeglem4  24581  plypf1  24729  coeeulem  24741  coeidlem  24754  coeid3  24757  plymul0or  24797  dvnply2  24803  plydivex  24813  vieta1lem2  24827  plyexmo  24829  aaliou3lem2  24859  ulmss  24912  ulmdvlem3  24917  iblulm  24922  sincosq2sgn  25012  sincosq3sgn  25013  sincosq4sgn  25014  logcnlem5  25156  dcubic  25351  amgm  25495  isnsqf  25639  mumullem2  25684  chtublem  25714  chtub  25715  fsumvma2  25717  vmasum  25719  dchrfi  25758  bposlem1  25787  bposlem3  25789  bposlem7  25793  lgsdir  25835  lgsquadlem2  25884  2sqlem8a  25928  2sqlem10  25931  dchrisum0flb  26013  pntpbnd1  26089  pntlemf  26108  pntlem3  26112  axeuclid  26676  uspgrushgr  26887  uspgrupgr  26888  usgruspgr  26890  usgr2pth  27472  crctcshwlkn0lem5  27519  wwlksnext  27598  wwlksnextsurj  27605  clwwlkccatlem  27694  clwlkclwwlkf  27713  clwwisshclwwslemlem  27718  lnon0  28502  normpyc  28850  ocsh  28987  ocorth  28995  ococss  28997  shsel2  29026  hsupss  29045  pjhth  29097  shlub  29118  cm2j  29324  lnfncnbd  29761  riesz1  29769  rnbra  29811  leopadd  29836  leopmuli  29837  hstles  29935  stge1i  29942  stle0i  29943  dmdbr5  30012  ssmd2  30016  superpos  30058  chcv1  30059  atoml2i  30087  chirredlem2  30095  atcvat3i  30100  mdsymlem5  30111  mdsymlem6  30112  sumdmdii  30119  sumdmdlem2  30123  isarchiofld  30817  sqsscirc2  31051  cnre2csqlem  31052  xrge0iifiso  31077  sigaclci  31290  omssubadd  31457  eulerpartlemb  31525  ballotlemimin  31662  ballotlem7  31692  subgrwlk  32276  cusgracyclt3v  32300  cvmlift2lem12  32458  fmlasucdisj  32543  dfon2lem8  32932  soseq  32993  segconeq  33368  ifscgr  33402  brofs2  33435  brifs2  33436  endofsegid  33443  dissneqlem  34503  rdgellim  34539  fvineqsneq  34575  tan2h  34765  matunitlindflem2  34770  poimirlem31  34804  poimir  34806  fzmul  34897  fdc  34901  incsequz2  34905  sstotbnd2  34933  sstotbnd3  34935  totbndbnd  34948  isexid2  35014  ispridl2  35197  mpobi123f  35321  riotasvd  35972  lsator0sp  36017  lssatle  36031  lshpset2N  36135  lkrlspeqN  36187  omllaw2N  36260  cmtbr3N  36270  lecmtN  36272  cvlcvr1  36355  cvrval4N  36430  cvrat3  36458  3noncolr2  36465  4noncolr3  36469  3dimlem3  36477  3dimlem3OLDN  36478  3dimlem4  36480  3dimlem4OLDN  36481  llncvrlpln  36574  lplncvrlvol  36632  snatpsubN  36766  linepsubN  36768  pmapjat1  36869  pclfinclN  36966  pl42N  36999  ltrneq2  37164  cdleme7aa  37258  cdleme18d  37311  cdleme21b  37342  trlord  37585  trlcoat  37739  dochkrshp  38402  lcfl8  38518  irrapxlem2  39298  pell14qrdich  39344  monotoddzz  39418  pw2f1ocnv  39512  iocinico  39696  nndomog  39775  harval3  39782  sbcim2g  40749  stoweidlem62  42224  elfzelfzlble  43398  eenglngeehlnmlem2  44653
  Copyright terms: Public domain W3C validator