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

Theorem sylibrd 250
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 239 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3imtr4d  285  sbciegft  3661  opeldmd  5525  elreldm  5548  ordtr2  5978  ssimaex  6481  fliftfun  6783  isopolem  6816  isosolem  6818  ordsucss  7245  f1oweALT  7379  fnse  7525  brtpos  7593  issmo2  7679  seqomlem1  7778  omcl  7850  oecl  7851  oawordeulem  7868  oaass  7875  omordi  7880  omord  7882  odi  7893  oen0  7900  oeordi  7901  oeordsuc  7908  nnmcl  7926  nnecl  7927  nnmordi  7945  nnmord  7946  nnmwordri  7950  nnaordex  7952  swoord1  8007  ecopovtrn  8083  f1domg  8209  pw2f1olem  8300  domtriord  8342  mapen  8360  mapxpen  8362  mapunen  8365  nndomo  8390  inficl  8567  supmo  8594  infmo  8637  inf3lem6  8774  cantnflem1  8830  tcmin  8861  tcrank  8991  cardne  9071  cardlim  9078  cardsdomel  9080  carduni  9087  alephord  9178  cardinfima  9200  dfac5lem4  9229  infdif2  9314  cofsmo  9373  cfcoflem  9376  infpssrlem4  9410  infpssrlem5  9411  fin4en1  9413  isfin2-2  9423  enfin2i  9425  fin23lem27  9432  isf32lem12  9468  isf34lem6  9484  domtriomlem  9546  cardmin  9668  fpwwe2lem12  9745  inar1  9879  gruiun  9903  ltsonq  10073  prub  10098  reclem3pr  10153  mulcmpblnr  10174  mulgt0sr  10208  axpre-sup  10272  leltadd  10794  infm3  11264  peano5nni  11305  zextle  11712  prime  11720  uzin  11934  ublbneg  11988  zbtwnre  12001  mul2lt0bi  12146  xrre2  12215  xralrple  12250  xmulneg1  12313  supxrbnd  12372  supxrgtmnf  12373  fzrevral  12644  flge  12826  ceile  12868  modadd1  12927  modmul1  12943  modsumfzodifsn  12963  seqcl2  13038  facdiv  13290  hashss  13410  hash2exprb  13466  elfzelfzccat  13573  repswswrd  13751  cshf1  13776  cshwcsh2id  13794  rlim2lt  14447  rlim3  14448  o1lo1  14487  climshftlem  14524  o1co  14536  o1of2  14562  isercolllem2  14615  isercoll  14617  caucvgrlem2  14624  climcndslem2  14800  sqrt2irr  15195  dvds2lem  15213  dvdsle  15251  dvdsfac  15267  ltoddhalfle  15301  divalglem0  15332  ndvdsadd  15349  bitsinv1lem  15378  sadcaddlem  15394  dvdslegcd  15441  bezoutlem2  15472  bezoutlem4  15474  gcdzeq  15486  algcvga  15507  rpdvds  15588  cncongr1  15595  cncongr2  15596  prmind2  15612  isprm6  15639  rpexp  15645  eulerthlem2  15700  pclem  15756  pceulem  15763  pc2dvds  15796  fldivp1  15814  infpnlem1  15827  prmunb  15831  mrieqv2d  16500  plttr  17171  clatl  17317  issubg4  17811  gexdvds  18196  pgpssslw  18226  sylow2alem2  18230  efgs1b  18346  efgsfo  18349  lspindpi  19336  pf1ind  19923  psgnodpm  20137  psgndif  20152  obselocv  20278  mdetunilem9  20633  fiinbas  20966  bastg  20980  tgcl  20983  opnssneib  21129  clslp  21162  tgcnp  21267  iscnp4  21277  cncls2  21287  cncls  21288  cnntr  21289  cnpresti  21302  lmss  21312  lmcnp  21318  cmpsub  21413  tgcmp  21414  dfconn2  21432  t1connperf  21449  1stcfb  21458  1stcrest  21466  kgenss  21556  llycmpkgen2  21563  txdis  21645  qtoptop2  21712  kqt0lem  21749  isr0  21750  regr1lem2  21753  cmphaushmeo  21813  fbun  21853  ssfg  21885  fgtr  21903  ufildr  21944  cnpflf  22014  fclsnei  22032  flimfnfcls  22041  fclscmp  22043  ufilcmp  22045  cnpfcf  22054  alexsublem  22057  alexsubALTlem3  22062  alexsubALTlem4  22063  ptcmplem3  22067  tgphaus  22129  tgpt1  22130  tsmsres  22156  imasdsf1olem  22387  xblss2ps  22415  xblss2  22416  blsscls2  22518  metequiv2  22524  stdbdxmet  22529  nmoi  22741  reconn  22840  mulc1cncf  22917  cncfco  22919  iccpnfhmeo  22953  xrhmeo  22954  evth  22967  pi1grplem  23057  fgcfil  23277  ivthlem2  23429  ivthlem3  23430  ovolicc2lem4  23497  voliunlem1  23527  ioombl1lem4  23538  itg2gt0  23737  limcco  23867  lhop1  23987  tdeglem4  24030  plypf1  24178  coeeulem  24190  coeidlem  24203  coeid3  24206  plymul0or  24246  dvnply2  24252  plydivex  24262  vieta1lem2  24276  plyexmo  24278  aaliou3lem2  24308  ulmss  24361  ulmdvlem3  24366  iblulm  24371  sincosq2sgn  24462  sincosq3sgn  24463  sincosq4sgn  24464  logcnlem5  24602  dcubic  24783  amgm  24927  isnsqf  25071  mumullem2  25116  chtublem  25146  chtub  25147  fsumvma2  25149  vmasum  25151  dchrfi  25190  bposlem1  25219  bposlem3  25221  bposlem7  25225  lgsdir  25267  lgsquadlem2  25316  2sqlem8a  25360  2sqlem10  25363  dchrisum0flb  25409  pntpbnd1  25485  pntlemf  25504  pntlem3  25508  axeuclid  26053  uspgrushgr  26281  uspgrupgr  26282  usgruspgr  26284  usgr2pth  26884  crctcshwlkn0lem5  26931  wwlksnext  27026  wwlksnextsur  27033  clwwlkccatlem  27128  clwlkclwwlkf  27147  clwwisshclwwslemlem  27152  lnon0  27978  normpyc  28328  ocsh  28467  ocorth  28475  ococss  28477  shsel2  28506  hsupss  28525  pjhth  28577  shlub  28598  cm2j  28804  lnfncnbd  29241  riesz1  29249  rnbra  29291  leopadd  29316  leopmuli  29317  hstles  29415  stge1i  29422  stle0i  29423  dmdbr5  29492  ssmd2  29496  superpos  29538  chcv1  29539  atoml2i  29567  chirredlem2  29575  atcvat3i  29580  mdsymlem5  29591  mdsymlem6  29592  sumdmdii  29599  sumdmdlem2  29603  isarchiofld  30139  sqsscirc2  30277  cnre2csqlem  30278  xrge0iifiso  30303  sigaclci  30517  omssubadd  30684  eulerpartlemb  30752  ballotlemimin  30889  ballotlem7  30919  cvmlift2lem12  31616  dfon2lem8  32012  soseq  32072  segconeq  32435  ifscgr  32469  brofs2  32502  brifs2  32503  endofsegid  32510  dissneqlem  33501  tan2h  33711  matunitlindflem2  33716  poimirlem31  33750  poimir  33752  fzmul  33845  fdc  33849  incsequz2  33853  sstotbnd2  33881  sstotbnd3  33883  totbndbnd  33896  isexid2  33962  ispridl2  34145  mpt2bi123f  34278  riotasvd  34732  lsator0sp  34778  lssatle  34792  lshpset2N  34896  lkrlspeqN  34948  omllaw2N  35021  cmtbr3N  35031  lecmtN  35033  cvlcvr1  35116  cvrval4N  35191  cvrat3  35219  3noncolr2  35226  4noncolr3  35230  3dimlem3  35238  3dimlem3OLDN  35239  3dimlem4  35241  3dimlem4OLDN  35242  llncvrlpln  35335  lplncvrlvol  35393  snatpsubN  35527  linepsubN  35529  pmapjat1  35630  pclfinclN  35727  pl42N  35760  ltrneq2  35925  cdleme7aa  36020  cdleme18d  36073  cdleme21b  36104  trlord  36347  trlcoat  36501  dochkrshp  37164  lcfl8  37280  irrapxlem2  37886  pell14qrdich  37932  monotoddzz  38006  pw2f1ocnv  38102  iocinico  38294  sbcim2g  39243  stoweidlem62  40755  elfzelfzlble  41903
  Copyright terms: Public domain W3C validator