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

Theorem sylibrd 226
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 215 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 42 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr4d  260  sbciegft  3159  eqsbc3r  3186  ordtr2  4593  ordsucss  4765  elreldm  5061  ssimaex  5755  fconstfv  5921  fliftfun  6001  isopolem  6032  isosolem  6034  f1oweALT  6041  fnse  6430  brtpos  6455  riotasvd  6559  issmo2  6578  seqomlem1  6674  omcl  6747  oecl  6748  oawordeulem  6764  oaass  6771  omordi  6776  omord  6778  odi  6789  oen0  6796  oeordi  6797  oeordsuc  6804  nnmcl  6822  nnecl  6823  nnmordi  6841  nnmord  6842  nnmwordri  6846  nnaordex  6848  swoord1  6901  ecopovtrn  6974  f1domg  7094  pw2f1olem  7179  domtriord  7220  mapen  7238  mapxpen  7240  mapunen  7243  nndomo  7267  inficl  7396  supmo  7421  inf3lem6  7552  cantnflem1  7609  tcmin  7644  tcrank  7772  cardne  7816  cardlim  7823  cardsdomel  7825  carduni  7832  alephord  7920  cardinfima  7942  dfac5lem4  7971  infdif2  8054  cofsmo  8113  cfcoflem  8116  infpssrlem4  8150  infpssrlem5  8151  fin4en1  8153  isfin2-2  8163  enfin2i  8165  fin23lem27  8172  isf32lem12  8208  isf34lem6  8224  domtriomlem  8286  cardmin  8403  fpwwe2lem12  8480  inar1  8614  gruiun  8638  ltsonq  8810  prub  8835  reclem3pr  8890  mulcmpblnr  8913  mulgt0sr  8944  axpre-sup  9008  leltadd  9476  infm3  9931  peano5nni  9967  zextle  10307  prime  10314  uzindOLD  10328  uzin  10482  ublbneg  10524  zbtwnre  10536  xrre2  10722  xralrple  10755  xmulneg1  10812  supxrbnd  10871  supxrgtmnf  10872  fzrevral  11094  flge  11177  ceile  11198  modadd1  11241  modmul1  11242  seqcl2  11304  facdiv  11541  hash2prb  11652  rlim2lt  12254  rlim3  12255  o1lo1  12294  climshftlem  12331  o1co  12343  o1of2  12369  isercolllem2  12422  isercoll  12424  caucvgrlem2  12431  climcndslem2  12593  sqr2irr  12811  dvds2lem  12825  dvdsle  12858  dvdsfac  12867  divalglem0  12876  ndvdsadd  12891  bitsinv1lem  12916  sadcaddlem  12932  dvdslegcd  12979  bezoutlem2  13002  bezoutlem4  13004  gcdeq  13015  algcvga  13033  prmind2  13053  isprm6  13072  rpexp  13083  rpdvds  13087  eulerthlem2  13134  pclem  13175  pceulem  13182  pc2dvds  13215  fldivp1  13229  infpnlem1  13241  prmunb  13245  mrieqv2d  13827  plttr  14390  joinlem  14410  meetlem  14417  issubg4  14924  gexdvds  15181  pgpssslw  15211  sylow2alem2  15215  efgs1b  15331  efgsfo  15334  lspindpi  16167  obselocv  16918  fiinbas  16980  bastg  16994  tgcl  16997  opnssneib  17142  clslp  17174  tgcnp  17279  iscnp4  17289  cncls2  17299  cncls  17300  cnntr  17301  cnpresti  17314  lmss  17324  lmcnp  17330  cmpsub  17425  tgcmp  17426  dfcon2  17443  t1conperf  17460  1stcfb  17469  1stcrest  17477  kgenss  17536  llycmpkgen2  17543  txdis  17625  qtoptop2  17692  kqt0lem  17729  isr0  17730  regr1lem2  17733  cmphaushmeo  17793  fbun  17833  ssfg  17865  fgtr  17883  ufildr  17924  cnpflf  17994  fclsnei  18012  flimfnfcls  18021  fclscmp  18023  ufilcmp  18025  cnpfcf  18034  alexsublem  18036  alexsubALTlem3  18041  alexsubALTlem4  18042  ptcmplem3  18046  tgphaus  18107  tgpt1  18108  tsmsres  18134  imasdsf1olem  18364  xblss2ps  18392  xblss2  18393  blsscls2  18495  metequiv2  18501  stdbdxmet  18506  nmoi  18723  reconn  18820  mulc1cncf  18896  cncfco  18898  iccpnfhmeo  18931  xrhmeo  18932  evth  18945  pi1grplem  19035  fgcfil  19185  ivthlem2  19310  ivthlem3  19311  ovolicc2lem4  19377  voliunlem1  19405  ioombl1lem4  19416  itg2gt0  19613  limcco  19741  lhop1  19859  pf1ind  19936  tdeglem4  19944  plypf1  20092  coeeulem  20104  coeidlem  20117  coeid3  20120  plymul0or  20159  dvnply2  20165  plydivex  20175  vieta1lem2  20189  plyexmo  20191  aaliou3lem2  20221  ulmss  20274  ulmdvlem3  20279  iblulm  20284  sincosq2sgn  20368  sincosq3sgn  20369  sincosq4sgn  20370  logcnlem5  20498  dcubic  20647  amgm  20790  isnsqf  20879  mumullem2  20924  chtublem  20956  chtub  20957  fsumvma2  20959  vmasum  20961  dchrfi  21000  bposlem1  21029  bposlem3  21031  bposlem7  21035  lgsdir  21075  lgsquadlem2  21100  2sqlem8a  21116  2sqlem10  21119  dchrisum0flb  21165  pntpbnd1  21241  pntlemf  21260  pntlem3  21264  umisuhgra  21323  uslisumgra  21347  usisuslgra  21348  constr3trl  21607  constr3pth  21608  vdusgraval  21639  gxcl  21814  isexid2  21874  lnon0  22260  normpyc  22609  ocsh  22746  ocorth  22754  ococss  22756  shsel2  22785  hsupss  22804  pjhth  22856  shlub  22877  cm2j  23083  lnfncnbd  23521  riesz1  23529  rnbra  23571  leopadd  23596  leopmuli  23597  hstles  23695  stge1i  23702  stle0i  23703  dmdbr5  23772  ssmd2  23776  superpos  23818  chcv1  23819  atoml2i  23847  chirredlem2  23855  atcvat3i  23860  mdsymlem5  23871  mdsymlem6  23872  sumdmdii  23879  sumdmdlem2  23883  sqsscirc2  24268  cnre2csqlem  24269  xrge0iifiso  24282  sigaclci  24476  ballotlemimin  24724  ballotlem7  24754  cvmlift2lem12  24962  dfon2lem8  25368  soseq  25476  axeuclid  25814  segconeq  25856  ifscgr  25890  brofs2  25923  brifs2  25924  endofsegid  25931  fzmul  26342  fdc  26347  incsequz2  26351  sstotbnd2  26381  sstotbnd3  26383  totbndbnd  26396  ispridl2  26546  irrapxlem2  26784  pell14qrdich  26830  monotoddzz  26904  pw2f1ocnv  27006  stoweidlem62  27686  elfzelfzccat  28014  swrdccatin12lem3  28032  swrdccatin12b  28035  swrdccat3b  28039  sbcim2g  28342  lsator0sp  29496  lssatle  29510  lshpset2N  29614  lkrlspeqN  29666  omllaw2N  29739  cmtbr3N  29749  lecmtN  29751  cvlcvr1  29834  cvrval4N  29908  cvrat3  29936  3noncolr2  29943  4noncolr3  29947  3dimlem3  29955  3dimlem3OLDN  29956  3dimlem4  29958  3dimlem4OLDN  29959  llncvrlpln  30052  lplncvrlvol  30110  snatpsubN  30244  linepsubN  30246  pmapjat1  30347  pclfinclN  30444  pl42N  30477  ltrneq2  30642  cdleme7aa  30736  cdleme18d  30789  cdleme21b  30820  trlord  31063  trlcoat  31217  dochkrshp  31881  lcfl8  31997
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 178
  Copyright terms: Public domain W3C validator