MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylibrd Structured version   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  3191  eqsbc3r  3218  ordtr2  4625  ordsucss  4798  elreldm  5094  ssimaex  5788  fconstfv  5954  fliftfun  6034  isopolem  6065  isosolem  6067  f1oweALT  6074  fnse  6463  brtpos  6488  riotasvd  6592  issmo2  6611  seqomlem1  6707  omcl  6780  oecl  6781  oawordeulem  6797  oaass  6804  omordi  6809  omord  6811  odi  6822  oen0  6829  oeordi  6830  oeordsuc  6837  nnmcl  6855  nnecl  6856  nnmordi  6874  nnmord  6875  nnmwordri  6879  nnaordex  6881  swoord1  6934  ecopovtrn  7007  f1domg  7127  pw2f1olem  7212  domtriord  7253  mapen  7271  mapxpen  7273  mapunen  7276  nndomo  7300  inficl  7430  supmo  7457  inf3lem6  7588  cantnflem1  7645  tcmin  7680  tcrank  7808  cardne  7852  cardlim  7859  cardsdomel  7861  carduni  7868  alephord  7956  cardinfima  7978  dfac5lem4  8007  infdif2  8090  cofsmo  8149  cfcoflem  8152  infpssrlem4  8186  infpssrlem5  8187  fin4en1  8189  isfin2-2  8199  enfin2i  8201  fin23lem27  8208  isf32lem12  8244  isf34lem6  8260  domtriomlem  8322  cardmin  8439  fpwwe2lem12  8516  inar1  8650  gruiun  8674  ltsonq  8846  prub  8871  reclem3pr  8926  mulcmpblnr  8949  mulgt0sr  8980  axpre-sup  9044  leltadd  9512  infm3  9967  peano5nni  10003  zextle  10343  prime  10350  uzindOLD  10364  uzin  10518  ublbneg  10560  zbtwnre  10572  xrre2  10758  xralrple  10791  xmulneg1  10848  supxrbnd  10907  supxrgtmnf  10908  fzrevral  11131  flge  11214  ceile  11235  modadd1  11278  modmul1  11279  seqcl2  11341  facdiv  11578  hash2prb  11689  rlim2lt  12291  rlim3  12292  o1lo1  12331  climshftlem  12368  o1co  12380  o1of2  12406  isercolllem2  12459  isercoll  12461  caucvgrlem2  12468  climcndslem2  12630  sqr2irr  12848  dvds2lem  12862  dvdsle  12895  dvdsfac  12904  divalglem0  12913  ndvdsadd  12928  bitsinv1lem  12953  sadcaddlem  12969  dvdslegcd  13016  bezoutlem2  13039  bezoutlem4  13041  gcdeq  13052  algcvga  13070  prmind2  13090  isprm6  13109  rpexp  13120  rpdvds  13124  eulerthlem2  13171  pclem  13212  pceulem  13219  pc2dvds  13252  fldivp1  13266  infpnlem1  13278  prmunb  13282  mrieqv2d  13864  plttr  14427  joinlem  14447  meetlem  14454  issubg4  14961  gexdvds  15218  pgpssslw  15248  sylow2alem2  15252  efgs1b  15368  efgsfo  15371  lspindpi  16204  obselocv  16955  fiinbas  17017  bastg  17031  tgcl  17034  opnssneib  17179  clslp  17212  tgcnp  17317  iscnp4  17327  cncls2  17337  cncls  17338  cnntr  17339  cnpresti  17352  lmss  17362  lmcnp  17368  cmpsub  17463  tgcmp  17464  dfcon2  17482  t1conperf  17499  1stcfb  17508  1stcrest  17516  kgenss  17575  llycmpkgen2  17582  txdis  17664  qtoptop2  17731  kqt0lem  17768  isr0  17769  regr1lem2  17772  cmphaushmeo  17832  fbun  17872  ssfg  17904  fgtr  17922  ufildr  17963  cnpflf  18033  fclsnei  18051  flimfnfcls  18060  fclscmp  18062  ufilcmp  18064  cnpfcf  18073  alexsublem  18075  alexsubALTlem3  18080  alexsubALTlem4  18081  ptcmplem3  18085  tgphaus  18146  tgpt1  18147  tsmsres  18173  imasdsf1olem  18403  xblss2ps  18431  xblss2  18432  blsscls2  18534  metequiv2  18540  stdbdxmet  18545  nmoi  18762  reconn  18859  mulc1cncf  18935  cncfco  18937  iccpnfhmeo  18970  xrhmeo  18971  evth  18984  pi1grplem  19074  fgcfil  19224  ivthlem2  19349  ivthlem3  19350  ovolicc2lem4  19416  voliunlem1  19444  ioombl1lem4  19455  itg2gt0  19652  limcco  19780  lhop1  19898  pf1ind  19975  tdeglem4  19983  plypf1  20131  coeeulem  20143  coeidlem  20156  coeid3  20159  plymul0or  20198  dvnply2  20204  plydivex  20214  vieta1lem2  20228  plyexmo  20230  aaliou3lem2  20260  ulmss  20313  ulmdvlem3  20318  iblulm  20323  sincosq2sgn  20407  sincosq3sgn  20408  sincosq4sgn  20409  logcnlem5  20537  dcubic  20686  amgm  20829  isnsqf  20918  mumullem2  20963  chtublem  20995  chtub  20996  fsumvma2  20998  vmasum  21000  dchrfi  21039  bposlem1  21068  bposlem3  21070  bposlem7  21074  lgsdir  21114  lgsquadlem2  21139  2sqlem8a  21155  2sqlem10  21158  dchrisum0flb  21204  pntpbnd1  21280  pntlemf  21299  pntlem3  21303  umisuhgra  21362  uslisumgra  21386  usisuslgra  21387  constr3trl  21646  constr3pth  21647  vdusgraval  21678  gxcl  21853  isexid2  21913  lnon0  22299  normpyc  22648  ocsh  22785  ocorth  22793  ococss  22795  shsel2  22824  hsupss  22843  pjhth  22895  shlub  22916  cm2j  23122  lnfncnbd  23560  riesz1  23568  rnbra  23610  leopadd  23635  leopmuli  23636  hstles  23734  stge1i  23741  stle0i  23742  dmdbr5  23811  ssmd2  23815  superpos  23857  chcv1  23858  atoml2i  23886  chirredlem2  23894  atcvat3i  23899  mdsymlem5  23910  mdsymlem6  23911  sumdmdii  23918  sumdmdlem2  23922  sqsscirc2  24307  cnre2csqlem  24308  xrge0iifiso  24321  sigaclci  24515  ballotlemimin  24763  ballotlem7  24793  cvmlift2lem12  25001  dfon2lem8  25417  soseq  25529  axeuclid  25902  segconeq  25944  ifscgr  25978  brofs2  26011  brifs2  26012  endofsegid  26019  fzmul  26444  fdc  26449  incsequz2  26453  sstotbnd2  26483  sstotbnd3  26485  totbndbnd  26498  ispridl2  26648  irrapxlem2  26886  pell14qrdich  26932  monotoddzz  27006  pw2f1ocnv  27108  stoweidlem62  27787  elfzelfzccat  28177  2cshw2lem1  28252  sbcim2g  28623  lsator0sp  29799  lssatle  29813  lshpset2N  29917  lkrlspeqN  29969  omllaw2N  30042  cmtbr3N  30052  lecmtN  30054  cvlcvr1  30137  cvrval4N  30211  cvrat3  30239  3noncolr2  30246  4noncolr3  30250  3dimlem3  30258  3dimlem3OLDN  30259  3dimlem4  30261  3dimlem4OLDN  30262  llncvrlpln  30355  lplncvrlvol  30413  snatpsubN  30547  linepsubN  30549  pmapjat1  30650  pclfinclN  30747  pl42N  30780  ltrneq2  30945  cdleme7aa  31039  cdleme18d  31092  cdleme21b  31123  trlord  31366  trlcoat  31520  dochkrshp  32184  lcfl8  32300
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