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

Theorem sylibrd 249
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 238 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3imtr4d  283  sbciegft  3499  eqsbc3rOLD  3526  opeldmd  5359  elreldm  5382  ordtr2  5806  ssimaex  6302  fliftfun  6602  isopolem  6635  isosolem  6637  ordsucss  7060  f1oweALT  7194  fnse  7339  brtpos  7406  issmo2  7491  seqomlem1  7590  omcl  7661  oecl  7662  oawordeulem  7679  oaass  7686  omordi  7691  omord  7693  odi  7704  oen0  7711  oeordi  7712  oeordsuc  7719  nnmcl  7737  nnecl  7738  nnmordi  7756  nnmord  7757  nnmwordri  7761  nnaordex  7763  swoord1  7818  ecopovtrn  7893  f1domg  8017  pw2f1olem  8105  domtriord  8147  mapen  8165  mapxpen  8167  mapunen  8170  nndomo  8195  inficl  8372  supmo  8399  infmo  8442  inf3lem6  8568  cantnflem1  8624  tcmin  8655  tcrank  8785  cardne  8829  cardlim  8836  cardsdomel  8838  carduni  8845  alephord  8936  cardinfima  8958  dfac5lem4  8987  infdif2  9070  cofsmo  9129  cfcoflem  9132  infpssrlem4  9166  infpssrlem5  9167  fin4en1  9169  isfin2-2  9179  enfin2i  9181  fin23lem27  9188  isf32lem12  9224  isf34lem6  9240  domtriomlem  9302  cardmin  9424  fpwwe2lem12  9501  inar1  9635  gruiun  9659  ltsonq  9829  prub  9854  reclem3pr  9909  mulcmpblnr  9930  mulgt0sr  9964  axpre-sup  10028  leltadd  10550  infm3  11020  peano5nni  11061  zextle  11488  prime  11496  uzin  11758  ublbneg  11811  zbtwnre  11824  mul2lt0bi  11974  xrre2  12039  xralrple  12074  xmulneg1  12137  supxrbnd  12196  supxrgtmnf  12197  fzrevral  12463  flge  12646  ceile  12688  modadd1  12747  modmul1  12763  modsumfzodifsn  12783  seqcl2  12859  facdiv  13114  hashss  13235  hash2exprb  13291  elfzelfzccat  13398  repswswrd  13577  cshf1  13602  cshwcsh2id  13620  rlim2lt  14272  rlim3  14273  o1lo1  14312  climshftlem  14349  o1co  14361  o1of2  14387  isercolllem2  14440  isercoll  14442  caucvgrlem2  14449  climcndslem2  14626  sqrt2irr  15023  dvds2lem  15041  dvdsle  15079  dvdsfac  15095  ltoddhalfle  15132  divalglem0  15163  ndvdsadd  15181  bitsinv1lem  15210  sadcaddlem  15226  dvdslegcd  15273  bezoutlem2  15304  bezoutlem4  15306  gcdzeq  15318  algcvga  15339  rpdvds  15421  cncongr1  15428  cncongr2  15429  prmind2  15445  isprm6  15473  rpexp  15479  eulerthlem2  15534  pclem  15590  pceulem  15597  pc2dvds  15630  fldivp1  15648  infpnlem1  15661  prmunb  15665  mrieqv2d  16346  plttr  17017  clatl  17163  issubg4  17660  gexdvds  18045  pgpssslw  18075  sylow2alem2  18079  efgs1b  18195  efgsfo  18198  lspindpi  19180  pf1ind  19767  psgnodpm  19982  psgndif  19996  obselocv  20120  mdetunilem9  20474  fiinbas  20804  bastg  20818  tgcl  20821  opnssneib  20967  clslp  21000  tgcnp  21105  iscnp4  21115  cncls2  21125  cncls  21126  cnntr  21127  cnpresti  21140  lmss  21150  lmcnp  21156  cmpsub  21251  tgcmp  21252  dfconn2  21270  t1connperf  21287  1stcfb  21296  1stcrest  21304  kgenss  21394  llycmpkgen2  21401  txdis  21483  qtoptop2  21550  kqt0lem  21587  isr0  21588  regr1lem2  21591  cmphaushmeo  21651  fbun  21691  ssfg  21723  fgtr  21741  ufildr  21782  cnpflf  21852  fclsnei  21870  flimfnfcls  21879  fclscmp  21881  ufilcmp  21883  cnpfcf  21892  alexsublem  21895  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem3  21905  tgphaus  21967  tgpt1  21968  tsmsres  21994  imasdsf1olem  22225  xblss2ps  22253  xblss2  22254  blsscls2  22356  metequiv2  22362  stdbdxmet  22367  nmoi  22579  reconn  22678  mulc1cncf  22755  cncfco  22757  iccpnfhmeo  22791  xrhmeo  22792  evth  22805  pi1grplem  22895  fgcfil  23115  ivthlem2  23267  ivthlem3  23268  ovolicc2lem4  23334  voliunlem1  23364  ioombl1lem4  23375  itg2gt0  23572  limcco  23702  lhop1  23822  tdeglem4  23865  plypf1  24013  coeeulem  24025  coeidlem  24038  coeid3  24041  plymul0or  24081  dvnply2  24087  plydivex  24097  vieta1lem2  24111  plyexmo  24113  aaliou3lem2  24143  ulmss  24196  ulmdvlem3  24201  iblulm  24206  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  logcnlem5  24437  dcubic  24618  amgm  24762  isnsqf  24906  mumullem2  24951  chtublem  24981  chtub  24982  fsumvma2  24984  vmasum  24986  dchrfi  25025  bposlem1  25054  bposlem3  25056  bposlem7  25060  lgsdir  25102  lgsquadlem2  25151  2sqlem8a  25195  2sqlem10  25198  dchrisum0flb  25244  pntpbnd1  25320  pntlemf  25339  pntlem3  25343  axeuclid  25888  uspgrushgr  26115  uspgrupgr  26116  usgruspgr  26118  usgr2pth  26716  crctcshwlkn0lem5  26762  wwlksnext  26856  wwlksnextsur  26863  clwwisshclwwslemlem  26970  clwwlkccatlem  27331  lnon0  27781  normpyc  28131  ocsh  28270  ocorth  28278  ococss  28280  shsel2  28309  hsupss  28328  pjhth  28380  shlub  28401  cm2j  28607  lnfncnbd  29044  riesz1  29052  rnbra  29094  leopadd  29119  leopmuli  29120  hstles  29218  stge1i  29225  stle0i  29226  dmdbr5  29295  ssmd2  29299  superpos  29341  chcv1  29342  atoml2i  29370  chirredlem2  29378  atcvat3i  29383  mdsymlem5  29394  mdsymlem6  29395  sumdmdii  29402  sumdmdlem2  29406  isarchiofld  29945  sqsscirc2  30083  cnre2csqlem  30084  xrge0iifiso  30109  sigaclci  30323  omssubadd  30490  eulerpartlemb  30558  ballotlemimin  30695  ballotlem7  30725  cvmlift2lem12  31422  dfon2lem8  31819  soseq  31879  segconeq  32242  ifscgr  32276  brofs2  32309  brifs2  32310  endofsegid  32317  dissneqlem  33317  tan2h  33531  matunitlindflem2  33536  poimirlem31  33570  poimir  33572  fzmul  33667  fdc  33671  incsequz2  33675  sstotbnd2  33703  sstotbnd3  33705  totbndbnd  33718  isexid2  33784  ispridl2  33967  mpt2bi123f  34101  riotasvd  34560  lsator0sp  34606  lssatle  34620  lshpset2N  34724  lkrlspeqN  34776  omllaw2N  34849  cmtbr3N  34859  lecmtN  34861  cvlcvr1  34944  cvrval4N  35018  cvrat3  35046  3noncolr2  35053  4noncolr3  35057  3dimlem3  35065  3dimlem3OLDN  35066  3dimlem4  35068  3dimlem4OLDN  35069  llncvrlpln  35162  lplncvrlvol  35220  snatpsubN  35354  linepsubN  35356  pmapjat1  35457  pclfinclN  35554  pl42N  35587  ltrneq2  35752  cdleme7aa  35847  cdleme18d  35900  cdleme21b  35931  trlord  36174  trlcoat  36328  dochkrshp  36992  lcfl8  37108  irrapxlem2  37704  pell14qrdich  37750  monotoddzz  37825  pw2f1ocnv  37921  iocinico  38114  sbcim2g  39065  stoweidlem62  40597  elfzelfzlble  41656
  Copyright terms: Public domain W3C validator