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

Theorem sylibrd 237
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 226 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3imtr4d  271  sbciegft  3327  eqsbc3r  3353  elreldm  5071  ordtr2  5478  ssimaex  5938  fconstfvOLD  6134  fliftfun  6212  isopolem  6243  isosolem  6245  ordsucss  6651  f1oweALT  6783  fnse  6916  brtpos  6982  issmo2  7068  seqomlem1  7167  omcl  7238  oecl  7239  oawordeulem  7255  oaass  7262  omordi  7267  omord  7269  odi  7280  oen0  7287  oeordi  7288  oeordsuc  7295  nnmcl  7313  nnecl  7314  nnmordi  7332  nnmord  7333  nnmwordri  7337  nnaordex  7339  swoord1  7392  ecopovtrn  7466  f1domg  7588  pw2f1olem  7674  domtriord  7716  mapen  7734  mapxpen  7736  mapunen  7739  nndomo  7764  inficl  7937  supmo  7964  infmo  8009  inf3lem6  8136  cantnflem1  8191  tcmin  8222  tcrank  8352  cardne  8396  cardlim  8403  cardsdomel  8405  carduni  8412  alephord  8502  cardinfima  8524  dfac5lem4  8553  infdif2  8636  cofsmo  8695  cfcoflem  8698  infpssrlem4  8732  infpssrlem5  8733  fin4en1  8735  isfin2-2  8745  enfin2i  8747  fin23lem27  8754  isf32lem12  8790  isf34lem6  8806  domtriomlem  8868  cardmin  8985  fpwwe2lem12  9062  inar1  9196  gruiun  9220  ltsonq  9390  prub  9415  reclem3pr  9470  mulcmpblnr  9491  mulgt0sr  9525  axpre-sup  9589  leltadd  10094  infm3  10564  peano5nni  10608  zextle  11005  prime  11012  uzin  11187  ublbneg  11244  zbtwnre  11258  mul2lt0bi  11398  xrre2  11461  xralrple  11494  xmulneg1  11551  supxrbnd  11610  supxrgtmnf  11611  fzrevral  11873  flge  12034  ceile  12069  modadd1  12127  modmul1  12136  seqcl2  12224  facdiv  12465  hashss  12579  hash2prb  12622  elfzelfzccat  12708  repswswrd  12868  cshwcsh2id  12908  rlim2lt  13539  rlim3  13540  o1lo1  13579  climshftlem  13616  o1co  13628  o1of2  13654  isercolllem2  13707  isercoll  13709  caucvgrlem2  13718  climcndslem2  13886  sqrt2irr  14279  dvds2lem  14293  dvdsle  14328  dvdsfac  14338  divalglem0  14349  ndvdsadd  14367  bitsinv1lem  14393  sadcaddlem  14409  dvdslegcd  14456  bezoutlem2OLD  14482  bezoutlem4OLD  14484  bezoutlem2  14485  bezoutlem4  14487  gcdeq  14498  algcvga  14516  prmind2  14613  isprm6  14644  rpexp  14650  rpdvds  14654  eulerthlem2  14708  pclem  14766  pceulem  14773  pc2dvds  14806  fldivp1  14820  infpnlem1  14832  prmunb  14836  mrieqv2d  15523  plttr  16194  clatl  16340  issubg4  16814  gexdvds  17213  pgpssslw  17244  sylow2alem2  17248  efgs1b  17364  efgsfo  17367  lspindpi  18333  pf1ind  18921  psgnodpm  19133  psgndif  19147  obselocv  19268  mdetunilem9  19622  fiinbas  19944  bastg  19958  tgcl  19962  opnssneib  20108  clslp  20141  tgcnp  20246  iscnp4  20256  cncls2  20266  cncls  20267  cnntr  20268  cnpresti  20281  lmss  20291  lmcnp  20297  cmpsub  20392  tgcmp  20393  dfcon2  20411  t1conperf  20428  1stcfb  20437  1stcrest  20445  kgenss  20535  llycmpkgen2  20542  txdis  20624  qtoptop2  20691  kqt0lem  20728  isr0  20729  regr1lem2  20732  cmphaushmeo  20792  fbun  20832  ssfg  20864  fgtr  20882  ufildr  20923  cnpflf  20993  fclsnei  21011  flimfnfcls  21020  fclscmp  21022  ufilcmp  21024  cnpfcf  21033  alexsublem  21036  alexsubALTlem3  21041  alexsubALTlem4  21042  ptcmplem3  21046  tgphaus  21108  tgpt1  21109  tsmsres  21135  imasdsf1olem  21365  xblss2ps  21393  xblss2  21394  blsscls2  21496  metequiv2  21502  stdbdxmet  21507  nmoi  21710  nmoiOLD  21726  reconn  21823  mulc1cncf  21914  cncfco  21916  iccpnfhmeo  21950  xrhmeo  21951  evth  21964  pi1grplem  22057  fgcfil  22218  ivthlem2  22380  ivthlem3  22381  ovolicc2lem4OLD  22450  ovolicc2lem4  22451  voliunlem1  22480  ioombl1lem4  22491  itg2gt0  22695  limcco  22825  lhop1  22943  tdeglem4  22986  plypf1  23143  coeeulem  23155  coeidlem  23168  coeid3  23171  plymul0or  23211  dvnply2  23217  plydivex  23227  vieta1lem2  23241  plyexmo  23243  aaliou3lem2  23276  ulmss  23329  ulmdvlem3  23334  iblulm  23339  sincosq2sgn  23431  sincosq3sgn  23432  sincosq4sgn  23433  logcnlem5  23568  dcubic  23749  amgm  23893  isnsqf  24039  mumullem2  24084  chtublem  24116  chtub  24117  fsumvma2  24119  vmasum  24121  dchrfi  24160  bposlem1  24189  bposlem3  24191  bposlem7  24195  lgsdir  24235  lgsquadlem2  24260  2sqlem8a  24276  2sqlem10  24279  dchrisum0flb  24325  pntpbnd1  24401  pntlemf  24420  pntlem3  24424  axeuclid  24970  umisuhgra  25031  uslisushgra  25067  uslisumgra  25068  usisuslgra  25069  constr3trl  25363  constr3pth  25364  wwlknext  25428  wwlkextsur  25435  clwwisshclwwlem1  25509  vdusgraval  25611  gxcl  25969  isexid2  26029  lnon0  26415  normpyc  26775  ocsh  26912  ocorth  26920  ococss  26922  shsel2  26951  hsupss  26970  pjhth  27022  shlub  27043  cm2j  27249  lnfncnbd  27686  riesz1  27694  rnbra  27736  leopadd  27761  leopmuli  27762  hstles  27860  stge1i  27867  stle0i  27868  dmdbr5  27937  ssmd2  27941  superpos  27983  chcv1  27984  atoml2i  28012  chirredlem2  28020  atcvat3i  28025  mdsymlem5  28036  mdsymlem6  28037  sumdmdii  28044  sumdmdlem2  28048  isarchiofld  28569  sqsscirc2  28704  cnre2csqlem  28705  xrge0iifiso  28730  sigaclci  28943  omssubadd  29117  omssubaddOLD  29121  eulerpartlemb  29190  ballotlemimin  29327  ballotlem7  29357  ballotlemiminOLD  29365  ballotlem7OLD  29395  cvmlift2lem12  30026  dfon2lem8  30424  soseq  30480  segconeq  30763  ifscgr  30797  brofs2  30830  brifs2  30831  endofsegid  30838  dissneqlem  31677  tan2h  31845  poimirlem31  31879  poimir  31881  fzmul  31977  fdc  31982  incsequz2  31986  sstotbnd2  32014  sstotbnd3  32016  totbndbnd  32029  ispridl2  32179  mpt2bi123f  32314  riotasvd  32441  lsator0sp  32480  lssatle  32494  lshpset2N  32598  lkrlspeqN  32650  omllaw2N  32723  cmtbr3N  32733  lecmtN  32735  cvlcvr1  32818  cvrval4N  32892  cvrat3  32920  3noncolr2  32927  4noncolr3  32931  3dimlem3  32939  3dimlem3OLDN  32940  3dimlem4  32942  3dimlem4OLDN  32943  llncvrlpln  33036  lplncvrlvol  33094  snatpsubN  33228  linepsubN  33230  pmapjat1  33331  pclfinclN  33428  pl42N  33461  ltrneq2  33626  cdleme7aa  33721  cdleme18d  33774  cdleme21b  33806  trlord  34049  trlcoat  34203  dochkrshp  34867  lcfl8  34983  irrapxlem2  35581  pell14qrdich  35629  monotoddzz  35705  pw2f1ocnv  35806  iocinico  36010  sbcim2g  36751  stoweidlem62  37710  stoweidlem62OLD  37711  gcdzeq  38413  elfzelfzlble  38657
  Copyright terms: Public domain W3C validator