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

Theorem sylibrd 225
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylibrd.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylibrd.2  |-  ( ph  ->  ( th  <->  ch )
)
Assertion
Ref Expression
sylibrd  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylibrd
StepHypRef Expression
1 sylibrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylibrd.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
32biimprd 214 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 40 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr4d  259  sbciegft  3021  eqsbc3r  3048  ordtr2  4436  ordsucss  4609  elreldm  4903  ssimaex  5584  fconstfv  5734  fliftfun  5811  isopolem  5842  isosolem  5844  f1oweALT  5851  fnse  6232  brtpos  6243  riotasvd  6347  issmo2  6366  seqomlem1  6462  omcl  6535  oecl  6536  oawordeulem  6552  oaass  6559  omordi  6564  omord  6566  odi  6577  oen0  6584  oeordi  6585  oeordsuc  6592  nnmcl  6610  nnecl  6611  nnmordi  6629  nnmord  6630  nnmwordri  6634  nnaordex  6636  swoord1  6689  ecopovtrn  6761  f1domg  6881  pw2f1olem  6966  domtriord  7007  mapen  7025  mapxpen  7027  mapunen  7030  nndomo  7054  inficl  7178  supmo  7203  inf3lem6  7334  cantnflem1  7391  tcmin  7426  tcrank  7554  cardne  7598  cardlim  7605  cardsdomel  7607  carduni  7614  alephord  7702  cardinfima  7724  dfac5lem4  7753  infdif2  7836  cofsmo  7895  cfcoflem  7898  infpssrlem4  7932  infpssrlem5  7933  fin4en1  7935  isfin2-2  7945  enfin2i  7947  fin23lem27  7954  isf32lem12  7990  isf34lem6  8006  domtriomlem  8068  cardmin  8186  fpwwe2lem12  8263  inar1  8397  gruiun  8421  ltsonq  8593  prub  8618  reclem3pr  8673  mulcmpblnr  8696  mulgt0sr  8727  axpre-sup  8791  leltadd  9258  infm3  9713  peano5nni  9749  zextle  10085  prime  10092  uzindOLD  10106  uzin  10260  ublbneg  10302  zbtwnre  10314  xrre2  10499  xralrple  10532  xmulneg1  10589  supxrbnd  10647  supxrgtmnf  10648  fzrevral  10866  flge  10937  ceile  10958  modadd1  11001  modmul1  11002  seqcl2  11064  facdiv  11300  rlim2lt  11971  rlim3  11972  o1lo1  12011  climshftlem  12048  o1co  12060  o1of2  12086  isercolllem2  12139  isercoll  12141  caucvgrlem2  12147  climcndslem2  12309  sqr2irr  12527  dvds2lem  12541  dvdsle  12574  dvdsfac  12583  divalglem0  12592  ndvdsadd  12607  bitsinv1lem  12632  sadcaddlem  12648  dvdslegcd  12695  bezoutlem2  12718  bezoutlem4  12720  gcdeq  12731  algcvga  12749  prmind2  12769  isprm6  12788  rpexp  12799  rpdvds  12803  eulerthlem2  12850  pclem  12891  pceulem  12898  pc2dvds  12931  fldivp1  12945  infpnlem1  12957  prmunb  12961  mrieqv2d  13541  plttr  14104  joinlem  14124  meetlem  14131  issubg4  14638  gexdvds  14895  pgpssslw  14925  sylow2alem2  14929  efgs1b  15045  efgsfo  15048  lspindpi  15885  obselocv  16628  fiinbas  16690  bastg  16704  tgcl  16707  opnssneib  16852  clslp  16879  tgcnp  16983  cncls2  17002  cncls  17003  cnntr  17004  cnpresti  17016  lmss  17026  lmcnp  17032  cmpsub  17127  tgcmp  17128  dfcon2  17145  t1conperf  17162  1stcfb  17171  1stcrest  17179  kgenss  17238  llycmpkgen2  17245  txdis  17326  qtoptop2  17390  kqt0lem  17427  isr0  17428  regr1lem2  17431  cmphaushmeo  17491  fbun  17535  ssfg  17567  fgtr  17585  ufildr  17626  cnpflf  17696  fclsnei  17714  flimfnfcls  17723  fclscmp  17725  ufilcmp  17727  cnpfcf  17736  alexsublem  17738  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem3  17748  tgphaus  17799  tgpt1  17800  tsmsres  17826  imasdsf1olem  17937  xblss2  17958  blsscls2  18050  metequiv2  18056  stdbdxmet  18061  nmoi  18237  reconn  18333  mulc1cncf  18409  cncfco  18411  iccpnfhmeo  18443  xrhmeo  18444  evth  18457  pi1grplem  18547  fgcfil  18697  ivthlem2  18812  ivthlem3  18813  ovolicc2lem4  18879  voliunlem1  18907  ioombl1lem4  18918  itg2gt0  19115  limcco  19243  lhop1  19361  pf1ind  19438  tdeglem4  19446  plypf1  19594  coeeulem  19606  coeidlem  19619  coeid3  19622  plymul0or  19661  dvnply2  19667  plydivex  19677  vieta1lem2  19691  plyexmo  19693  aaliou3lem2  19723  ulmss  19774  ulmdvlem3  19779  iblulm  19783  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  logcnlem5  19993  dcubic  20142  amgm  20285  isnsqf  20373  mumullem2  20418  chtublem  20450  chtub  20451  fsumvma2  20453  vmasum  20455  dchrfi  20494  bposlem1  20523  bposlem3  20525  bposlem7  20529  lgsdir  20569  lgsquadlem2  20594  2sqlem8a  20610  2sqlem10  20613  dchrisum0flb  20659  pntpbnd1  20735  pntlemf  20754  pntlem3  20758  gxcl  20932  isexid2  20992  lnon0  21376  normpyc  21725  ocsh  21862  ocorth  21870  ococss  21872  shsel2  21901  hsupss  21920  pjhth  21972  shlub  21993  cm2j  22199  lnfncnbd  22637  riesz1  22645  rnbra  22687  leopadd  22712  leopmuli  22713  hstles  22811  stge1i  22818  stle0i  22819  dmdbr5  22888  ssmd2  22892  superpos  22934  chcv1  22935  atoml2i  22963  chirredlem2  22971  atcvat3i  22976  mdsymlem5  22987  mdsymlem6  22988  sumdmdii  22995  sumdmdlem2  22999  ballotlemimin  23064  ballotlem7  23094  sqsscirc2  23293  cnre2csqlem  23294  xrge0iifiso  23317  sigaclci  23493  cvmlift2lem12  23845  dfon2lem8  24146  soseq  24254  axeuclid  24591  segconeq  24633  ifscgr  24667  brofs2  24700  brifs2  24701  endofsegid  24708  mapmapmap  25148  grpodlcan  25376  nsn  25530  iscnp4  25563  homgrf  25802  cmpmon  25815  partarelt2  25897  fzmul  26443  fdc  26455  incsequz2  26459  sstotbnd2  26498  sstotbnd3  26500  totbndbnd  26513  ispridl2  26663  irrapxlem2  26908  pell14qrdich  26954  monotoddzz  27028  pw2f1ocnv  27130  stoweidlem62  27811  uslisumgra  28112  usisuslgra  28113  sbcim2g  28302  lsator0sp  29191  lssatle  29205  lshpset2N  29309  lkrlspeqN  29361  omllaw2N  29434  cmtbr3N  29444  lecmtN  29446  cvlcvr1  29529  cvrval4N  29603  cvrat3  29631  3noncolr2  29638  4noncolr3  29642  3dimlem3  29650  3dimlem3OLDN  29651  3dimlem4  29653  3dimlem4OLDN  29654  llncvrlpln  29747  lplncvrlvol  29805  snatpsubN  29939  linepsubN  29941  pmapjat1  30042  pclfinclN  30139  pl42N  30172  ltrneq2  30337  cdleme7aa  30431  cdleme18d  30484  cdleme21b  30515  trlord  30758  trlcoat  30912  dochkrshp  31576  lcfl8  31692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator