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

Theorem sylibrd 262
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 251 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  3imtr4d  297  sbciegft  3756  opeldmd  5739  elreldm  5769  ordtr2  6203  ssimaex  6723  fliftfun  7044  isopolem  7077  isosolem  7079  ordsucss  7513  f1oweALT  7655  fnse  7810  brtpos  7884  issmo2  7969  seqomlem1  8069  omcl  8144  oecl  8145  oawordeulem  8163  oaass  8170  omordi  8175  omord  8177  odi  8188  oen0  8195  oeordi  8196  oeordsuc  8203  nnmcl  8221  nnecl  8222  nnmordi  8240  nnmord  8241  nnmwordri  8245  nnaordex  8247  swoord1  8303  ecopovtrn  8383  f1domg  8512  pw2f1olem  8604  domtriord  8647  mapen  8665  mapxpen  8667  mapunen  8670  nndomog  8692  inficl  8873  supmo  8900  infmo  8943  inf3lem6  9080  cantnflem1  9136  tcmin  9167  tcrank  9297  cardne  9378  cardlim  9385  cardsdomel  9387  carduni  9394  alephord  9486  cardinfima  9508  dfac5lem4  9537  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  11587  peano5nni  11628  zextle  12043  prime  12051  uzin  12266  ublbneg  12321  zbtwnre  12334  mul2lt0bi  12483  xrre2  12551  xralrple  12586  xmulneg1  12650  supxrbnd  12709  supxrgtmnf  12710  fzrevral  12987  flge  13170  ceile  13212  modadd1  13271  modmul1  13287  modsumfzodifsn  13307  seqcl2  13384  facdiv  13643  hashss  13766  hash2exprb  13825  elfzelfzccat  13925  repswswrd  14137  cshf1  14163  cshwcsh2id  14181  rlim2lt  14846  rlim3  14847  o1lo1  14886  climshftlem  14923  o1co  14935  o1of2  14961  isercolllem2  15014  isercoll  15016  caucvgrlem2  15023  climcndslem2  15197  sqrt2irr  15594  dvds2lem  15614  dvdsle  15652  dvdsfac  15668  ltoddhalfle  15702  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  16902  plttr  17572  clatl  17718  issubg4  18290  gexdvds  18701  pgpssslw  18731  sylow2alem2  18735  efgs1b  18854  efgsfo  18857  lspindpi  19897  psgnodpm  20277  psgndif  20291  obselocv  20417  pf1ind  20979  mdetunilem9  21225  fiinbas  21557  bastg  21571  tgcl  21574  opnssneib  21720  clslp  21753  tgcnp  21858  iscnp4  21868  cncls2  21878  cncls  21879  cnntr  21880  cnpresti  21893  lmss  21903  lmcnp  21909  cmpsub  22005  tgcmp  22006  dfconn2  22024  t1connperf  22041  1stcfb  22050  1stcrest  22058  kgenss  22148  llycmpkgen2  22155  txdis  22237  qtoptop2  22304  kqt0lem  22341  isr0  22342  regr1lem2  22345  cmphaushmeo  22405  fbun  22445  ssfg  22477  fgtr  22495  ufildr  22536  cnpflf  22606  fclsnei  22624  flimfnfcls  22633  fclscmp  22635  ufilcmp  22637  cnpfcf  22646  alexsublem  22649  alexsubALTlem3  22654  alexsubALTlem4  22655  ptcmplem3  22659  tgphaus  22722  tgpt1  22723  tsmsres  22749  imasdsf1olem  22980  xblss2ps  23008  xblss2  23009  blsscls2  23111  metequiv2  23117  stdbdxmet  23122  nmoi  23334  reconn  23433  mulc1cncf  23510  cncfco  23512  iccpnfhmeo  23550  xrhmeo  23551  evth  23564  pi1grplem  23654  fgcfil  23875  ivthlem2  24056  ivthlem3  24057  ovolicc2lem4  24124  voliunlem1  24154  ioombl1lem4  24165  itg2gt0  24364  limcco  24496  lhop1  24617  tdeglem4  24661  plypf1  24809  coeeulem  24821  coeidlem  24834  coeid3  24837  plymul0or  24877  dvnply2  24883  plydivex  24893  vieta1lem2  24907  plyexmo  24909  aaliou3lem2  24939  ulmss  24992  ulmdvlem3  24997  iblulm  25002  sincosq2sgn  25092  sincosq3sgn  25093  sincosq4sgn  25094  logcnlem5  25237  dcubic  25432  amgm  25576  isnsqf  25720  mumullem2  25765  chtublem  25795  chtub  25796  fsumvma2  25798  vmasum  25800  dchrfi  25839  bposlem1  25868  bposlem3  25870  bposlem7  25874  lgsdir  25916  lgsquadlem2  25965  2sqlem8a  26009  2sqlem10  26012  dchrisum0flb  26094  pntpbnd1  26170  pntlemf  26189  pntlem3  26193  axeuclid  26757  uspgrushgr  26968  uspgrupgr  26969  usgruspgr  26971  usgr2pth  27553  crctcshwlkn0lem5  27600  wwlksnext  27679  wwlksnextsurj  27686  clwwlkccatlem  27774  clwlkclwwlkf  27793  clwwisshclwwslemlem  27798  lnon0  28581  normpyc  28929  ocsh  29066  ocorth  29074  ococss  29076  shsel2  29105  hsupss  29124  pjhth  29176  shlub  29197  cm2j  29403  lnfncnbd  29840  riesz1  29848  rnbra  29890  leopadd  29915  leopmuli  29916  hstles  30014  stge1i  30021  stle0i  30022  dmdbr5  30091  ssmd2  30095  superpos  30137  chcv1  30138  atoml2i  30166  chirredlem2  30174  atcvat3i  30179  mdsymlem5  30190  mdsymlem6  30191  sumdmdii  30198  sumdmdlem2  30202  isarchiofld  30941  sqsscirc2  31262  cnre2csqlem  31263  xrge0iifiso  31288  sigaclci  31501  omssubadd  31668  eulerpartlemb  31736  ballotlemimin  31873  ballotlem7  31903  subgrwlk  32492  cusgracyclt3v  32516  cvmlift2lem12  32674  fmlasucdisj  32759  dfon2lem8  33148  soseq  33209  segconeq  33584  ifscgr  33618  brofs2  33651  brifs2  33652  endofsegid  33659  dissneqlem  34757  rdgellim  34793  fvineqsneq  34829  tan2h  35049  matunitlindflem2  35054  poimirlem31  35088  poimir  35090  fzmul  35179  fdc  35183  incsequz2  35187  sstotbnd2  35212  sstotbnd3  35214  totbndbnd  35227  isexid2  35293  ispridl2  35476  mpobi123f  35600  riotasvd  36252  lsator0sp  36297  lssatle  36311  lshpset2N  36415  lkrlspeqN  36467  omllaw2N  36540  cmtbr3N  36550  lecmtN  36552  cvlcvr1  36635  cvrval4N  36710  cvrat3  36738  3noncolr2  36745  4noncolr3  36749  3dimlem3  36757  3dimlem3OLDN  36758  3dimlem4  36760  3dimlem4OLDN  36761  llncvrlpln  36854  lplncvrlvol  36912  snatpsubN  37046  linepsubN  37048  pmapjat1  37149  pclfinclN  37246  pl42N  37279  ltrneq2  37444  cdleme7aa  37538  cdleme18d  37591  cdleme21b  37622  trlord  37865  trlcoat  38019  dochkrshp  38682  lcfl8  38798  mulgt0con1dlem  39580  irrapxlem2  39762  pell14qrdich  39808  monotoddzz  39882  pw2f1ocnv  39976  iocinico  40160  harval3  40242  sbcim2g  41242  stoweidlem62  42702  elfzelfzlble  43876  1arymaptf1  45054  2arymaptf1  45065  eenglngeehlnmlem2  45150
  Copyright terms: Public domain W3C validator