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

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

Proof of Theorem sylbid
StepHypRef Expression
1 sylbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 200 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbid.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 43 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3imtr4d  261  ax11eq  2272  ax11el  2273  nlimsucg  4824  poltletr  5271  xp11  5306  xpcan  5307  xpcan2  5308  foconst  5666  fvmptdf  5818  suppss  5865  fnpr  5952  fnprOLD  5953  soisores  6049  isomin  6059  weniso  6077  ovmpt2df  6207  bropopvvv  6428  f1o2ndf1  6456  riotaxfrd  6583  eusvobj2  6584  smoiso  6626  tfrlem5  6643  tz7.48lem  6700  oevn0  6761  oaass  6806  omword1  6818  omlimcl  6823  odi  6824  oneo  6826  omeulem1  6827  oewordi  6836  oeworde  6838  oelimcl  6845  oaabs2  6890  omabs  6892  nnneo  6896  dom2lem  7149  fundmen  7182  onfin  7299  domfi  7332  dif1enOLD  7342  dif1en  7343  isfinite2  7367  unfilem1  7373  elfiun  7437  dffi3  7438  supisoex  7478  ordiso2  7486  ordtypelem7  7495  brwdom3  7552  unxpwdom2  7558  noinfepOLD  7617  cantnflem1  7647  cantnf  7651  r1sdom  7702  r1ord3g  7707  rankr1ai  7726  rankonidlem  7756  bndrank  7769  rankunb  7778  tcrank  7810  wdomfil  7944  wdomnumr  7947  alephordi  7957  alephdom  7964  dfac3  8004  dfac12lem3  8027  cfeq0  8138  cfsmolem  8152  sornom  8159  fin23lem28  8222  fin23lem30  8224  isf32lem2  8236  fin1a2lem9  8290  axcc2lem  8318  axdc3lem2  8333  axdc4lem  8337  ttukeylem5  8395  alephreg  8459  pwcfsdom  8460  fpwwe2lem13  8519  fpwwe2  8520  pwfseqlem3  8537  gchina  8576  inatsk  8655  intgru  8691  grur1  8697  grutsk1  8698  addcanpi  8778  mulcanpi  8779  addnidpi  8780  ltexnq  8854  ltbtwnnq  8857  genpss  8883  genpcd  8885  genpnmax  8886  addclprlem1  8895  mulclprlem  8898  distrlem1pr  8904  distrlem4pr  8905  distrlem5pr  8906  ltexprlem3  8917  ltexprlem6  8920  ltexpri  8922  reclem4pr  8929  axpre-sup  9046  lelttr  9167  ltletr  9168  letr  9169  le2add  9512  ltleadd  9513  lt2sub  9528  le2sub  9529  mulge0  9547  prodgt0  9857  squeeze0  9915  addltmul  10205  elnnz  10294  zextlt  10346  uzind2  10364  uzindOLD  10366  indstr  10547  qreccl  10596  rpnnen1lem1  10602  rpnnen1lem2  10603  rpnnen1lem3  10604  rpnnen1lem5  10606  xrlelttr  10748  xrltletr  10749  xrletr  10750  xrrebnd  10758  qbtwnre  10787  qbtwnxr  10788  qextlt  10791  qextle  10792  xltnegi  10804  xmulasslem  10866  xlemul1a  10869  iccid  10963  icoshft  11021  prunioo  11027  difreicc  11030  iccsplit  11031  fzm1  11129  elfznelfzo  11194  injresinjlem  11201  modirr  11288  om2uzf1oi  11295  seqf1olem1  11364  sqlecan  11489  facdiv  11580  facwordi  11582  faclbnd  11583  bcpasc  11614  hasheqf1oi  11637  hashdom  11655  hashgt12el  11684  hashgt12el2  11685  hash2pr  11689  hashtpg  11693  seqcoll  11714  sqrlem6  12055  resqrex  12058  absnid  12105  cau3lem  12160  sqreu  12166  rlim2lt  12293  rlim3  12294  o1lo1  12333  o1lo12  12334  rlimuni  12346  climuni  12348  lo1resb  12360  o1resb  12362  2clim  12368  o1rlimmul  12414  lo1le  12447  fsumss  12521  fsumabs  12582  cvgcmpce  12599  geomulcvg  12655  mertenslem2  12664  reeff1  12723  efieq1re  12802  dvdsmultr2  12887  dvdsleabs  12898  odd2np1lem  12909  odd2np1  12910  divalglem8  12922  sadcaddlem  12971  gcdneg  13028  gcddiv  13051  dvdssqim  13055  algcvga  13072  prmind2  13092  coprmdvds  13104  coprmdvds2  13105  qredeq  13108  euclemma  13110  nprmdvds1  13113  prmdvdsexpr  13118  prmfac1  13120  divgcdodd  13121  crt  13169  eulerthlem2  13173  fermltl  13175  coprimeprodsq2  13186  pythagtriplem2  13193  iserodd  13211  pcpremul  13219  pcdvdsb  13244  pc2dvds  13254  pc11  13255  pcfac  13270  prmpwdvds  13274  prmreclem4  13289  prmreclem5  13290  1arith  13297  4sqlem11  13325  vdwlem6  13356  vdwlem7  13357  vdwlem9  13359  vdwlem10  13360  vdwlem11  13361  ramub1lem2  13397  ramcl  13399  prmlem0  13430  firest  13662  imasaddfnlem  13755  imasvscafn  13764  erlecpbl  13777  xpsff1o  13795  setcmon  14244  setcepi  14245  setciso  14248  pltnle  14425  pltletr  14430  plelttr  14431  psref  14642  dirge  14684  imasmnd2  14734  imasgrp2  14935  ghmpreima  15029  gaorber  15087  mndodcongi  15183  sylow1lem1  15234  odcau  15240  sylow2alem1  15253  sylow2alem2  15254  lsmsubm  15289  lsmsubg  15290  lsmmod  15309  lsmdisj2  15316  efgtlen  15360  efgredlemc  15379  efgcpbllemb  15389  torsubg  15471  frgpnabllem1  15486  cyggexb  15510  gsumval3a  15514  dprdsubg  15584  dprddisj2  15599  dmdprdsplit2lem  15605  dmdprdsplit2  15606  ablfacrp  15626  ablfac1eulem  15632  pgpfac1lem3  15637  imasrng  15727  unitgrp  15774  lmhmima  16125  lsmcl  16157  lsmelval2  16159  lspsneleq  16189  lpiss  16323  xrsdsreclb  16747  gzrngunitlem  16765  znidomb  16844  frgpcyg  16856  tgtop  17040  neips  17179  neindisj  17183  restbas  17224  tgrest  17225  restcld  17238  restcldr  17240  ordtbas2  17257  ordtbas  17258  tgcn  17318  tgcnp  17319  subbascn  17320  cnconst2  17349  cnconst  17350  cnpresti  17354  cmpsublem  17464  tgcmp  17466  uncmp  17468  hauscmplem  17471  bwth  17475  conndisj  17481  nconsubb  17488  1stcfb  17510  2ndc1stc  17516  1stcrest  17518  2ndcctbss  17520  1stccnp  17527  llyrest  17550  nllyrest  17551  nllyidm  17554  cldllycmp  17560  1stckgen  17588  txcls  17638  txbasval  17640  txcnpi  17642  txcnp  17654  ptcnplem  17655  txdis1cn  17669  txlly  17670  txnlly  17671  pthaus  17672  tx1stc  17684  xkohaus  17687  xkococn  17694  basqtop  17745  qtopeu  17750  qtoprest  17751  qtopomap  17752  qtopcmap  17753  kqfvima  17764  kqsat  17765  kqcldsat  17767  fbfinnfr  17875  fgfil  17909  fgabs  17913  trfil2  17921  ufilmax  17941  isufil2  17942  ufprim  17943  ufileu  17953  filufint  17954  cfinufil  17962  elfm2  17982  rnelfmlem  17986  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem4  17991  fmfnfm  17992  ufldom  17996  flffbas  18029  flimfnfcls  18062  alexsublem  18077  alexsubALT  18084  symgtgp  18133  divstgpopn  18151  divstgplem  18152  tsmsxplem1  18184  bldisj  18430  xbln0  18446  blssps  18456  blss  18457  blin2  18461  blcls  18538  prdsxmslem2  18561  metustfbasOLD  18597  metustfbas  18598  xrsblre  18844  xrsmopn  18845  recld2  18847  reperflem  18851  reconnlem2  18860  cnmpt2pc  18955  cnheibor  18982  lebnumlem3  18990  nmhmcn  19130  cphsqrcl2  19151  iscau3  19233  iscau4  19234  iscmet3lem2  19247  lmcau  19267  cmetss  19269  bcth3  19286  cmetcusp1OLD  19307  cmetcusp1  19308  minveclem3b  19331  ivthlem2  19351  ivthlem3  19352  ovolctb  19388  ovolscalem1  19411  ovolicc2lem3  19417  ovolicc2lem4  19418  dyaddisjlem  19489  dyadmbllem  19493  opnmbllem  19495  subopnmbl  19498  volivth  19501  mbfimaopn2  19551  i1faddlem  19587  i1fmullem  19588  itg10a  19604  itg1ge0a  19605  mbfi1fseqlem4  19612  mbfi1flimlem  19616  dveflem  19865  dvlip2  19881  dvne0  19897  lhop1lem  19899  lhop1  19900  lhop2  19901  lhop  19902  dvcvx  19906  dvfsumrlim  19917  ftc1lem6  19927  itgsubst  19935  coe1mul3  20024  dvdsq1p  20085  coemullem  20170  coe1termlem  20178  dgrco  20195  coecj  20198  aaliou3lem7  20268  ulmcn  20317  reeff1o  20365  sincosq3sgn  20410  sincosq4sgn  20411  sineq0  20431  recosf1o  20439  efopn  20551  cxpge0  20576  cxpcn3lem  20633  cxpeq  20643  angpieqvd  20674  atantayl2  20780  rlimcnp  20806  xrlimcnp  20809  cxploglim  20818  ftalem2  20858  muval1  20918  ppiublem1  20988  chtub  20998  dchrmulcl  21035  dchrsum2  21054  bclbnd  21066  bposlem1  21070  bposlem5  21074  lgsdirnn0  21125  lgsqrlem2  21128  lgseisenlem2  21136  lgsquadlem1  21140  2sqblem  21163  chtppilimlem2  21170  dchrisumlem3  21187  dchrisum0lem1  21212  pntlem3  21305  ostth2lem2  21330  ostth3  21334  usgra0v  21393  usgraedgrn  21403  usgra2edg  21404  usgrarnedg  21406  usgra1v  21411  usgraidx2v  21414  usgrafisindb0  21424  usgrafisindb1  21425  nbgraisvtx  21445  nbgraf1olem1  21453  nbgraf1olem5  21457  nb3graprlem1  21462  cusgrarn  21470  cusgrasize2inds  21488  uvtxnbgra  21504  trliswlk  21541  pthdepisspth  21576  redwlk  21608  cyclnspth  21620  fargshiftf1  21626  usgrcyclnl1  21629  usgrcyclnl2  21630  3v3e3cycl1  21633  4cycl4v4e  21655  4cycl4dv  21656  4cycl4dv4e  21657  vdusgra0nedg  21681  usgravd0nedg  21685  isabloda  21889  blocnilem  22307  ipasslem11  22343  h1de2ctlem  23059  spansneleq  23074  spansnss  23075  normcan  23080  spansncvi  23156  nmcexi  23531  elpjrn  23695  stadd3i  23753  cvcon3  23789  dmdbr5  23813  ssdmd2  23819  atom1d  23858  superpos  23859  cvexchlem  23873  atcv0eq  23884  atexch  23886  atcvat4i  23902  atdmd  23903  atmd2  23905  mdsymlem3  23910  mdsymlem5  23912  sumdmdlem  23923  cdjreui  23937  cnre2csqlem  24310  ballotlemfrceq  24788  erdszelem4  24882  erdszelem9  24887  sconpi1  24928  relexpsucl  25134  rtrclreclem.trans  25148  mulge0b  25193  fprodss  25276  dvdspw  25371  predpo  25461  uzsinds  25493  omsinds  25496  soseq  25531  wsuclem  25578  sltres  25621  nodenselem3  25640  nodenselem4  25641  nodenselem5  25642  nodenselem8  25645  nofulllem5  25663  brbtwn2  25846  colinearalg  25851  axbtwnid  25880  axlowdimlem14  25896  axlowdimlem15  25897  axcontlem2  25906  cgrid2  25939  cgrextend  25944  btwnswapid2  25954  btwnexch3  25956  btwnexch  25961  ifscgr  25980  btwnxfr  25992  colineardim1  25997  colinearxfr  26011  lineext  26012  fscgr  26016  brsegle2  26045  seglecgr12im  26046  seglecgr12  26047  segletr  26050  segleantisym  26051  colinbtwnle  26054  broutsideof2  26058  outsideofeq  26066  outsidele  26068  lineunray  26083  lineelsb2  26084  elhf2  26118  ordtopcon  26191  ordtopt0  26194  opnmbllem0  26244  mblfinlem3  26247  ovoliunnfl  26250  voliunnfl  26252  itg2addnclem  26258  itg2addnclem2  26259  itg2addnclem3  26260  itg2gt0cn  26262  ftc1cnnc  26281  ftc2nc  26291  areacirclem1  26294  areacirclem2  26295  areacirclem4  26297  areacirc  26299  nn0prpwlem  26327  nn0prpw  26328  cldbnd  26331  fgmin  26401  tailfb  26408  indexdom  26438  fzmul  26446  fzadd2  26447  sdclem2  26448  sdclem1  26449  fdc  26451  incsequz  26454  sstotbnd2  26485  equivbnd  26501  prdstotbnd  26505  grpokerinj  26562  keridl  26644  smprngopr  26664  ispridlc  26682  dmncan2  26689  diophin  26833  diophun  26834  fphpdo  26880  pellexlem1  26894  pell1234qrne0  26918  pell14qrgt0  26924  pell1234qrdich  26926  pell1qrge1  26935  elpell1qr2  26937  pell1qrgap  26939  pellfundex  26951  rmxypairf1o  26976  jm2.26a  27073  setindtr  27097  rpnnen3  27105  dnnumch3  27124  fnwe2lem2  27128  pwssplit4  27170  lindfrn  27270  f1lindf  27271  hbtlem5  27311  pmtrfrn  27379  symggen  27390  psgnunilem2  27397  oprabv  28091  elovmpt2rab  28092  elovmpt2rab1  28093  elovmpt3rab1  28095  2elfz2melfz  28128  ubmelm1fzo  28138  subsubelfzo0  28146  fzofzim  28147  hashimarni  28175  elovmpt2wrd  28201  swdeq  28218  swrd0swrd  28219  swrdswrd  28221  swrdccatin12lem3a  28230  swrdccat3  28237  swrdccat  28238  swrdccat3blem  28240  prmgt1  28245  2cshw1lem1  28270  2cshw1lem2  28271  2cshw2lem2  28275  2cshwmod  28279  cshwssizelem1a  28301  cshwssizelem4  28306  uvtxnb  28319  usgra2pthspth  28331  usgra2wlkspthlem1  28332  usgra2wlkspth  28334  spthdifv  28335  usgra2pth  28337  wwlknimp  28357  wwlkn0  28359  wlkiswwlk1  28360  wlkiswwlk2  28367  wlklniswwlkn2  28370  el2wlkonot  28389  el2spthonot  28390  el2spthonot0  28391  2wlkonot3v  28395  2spthonot3v  28396  el2wlksotot  28402  usg2wlkonot  28403  usg2wotspth  28404  2spontn0vne  28407  usg2spthonot  28408  usg2spthonot0  28409  nbhashuvtx1  28419  rusgrargra  28433  3vfriswmgra  28457  1to2vfriswmgra  28458  2pthfrgra  28463  frgrancvvdeqlem2  28482  frgrawopreg1  28501  frgrawopreg2  28502  frg2wot1  28508  frg2woteqm  28510  frg2woteq  28511  2spotiundisj  28513  usg2spot2nb  28516  usgreg2spot  28518  2spotmdisj  28519  frgregordn0  28521  lshpdisj  29847  lsat0cv  29893  lcvexchlem4  29897  lcvexchlem5  29898  lsatcv0eq  29907  lfl1dim  29981  lfl1dim2N  29982  lkrss2N  30029  lkreqN  30030  cmtbr3N  30114  omlfh3N  30119  cvrnbtwn  30131  cvrcon3b  30137  atnle  30177  cvlatexch1  30196  cvlsupr2  30203  hlrelat2  30262  cvrexchlem  30278  cvrat  30281  atcvr0eq  30285  atcvrj0  30287  atltcvr  30294  cvrat4  30302  lvolex3N  30397  islpln2a  30407  lplnriaN  30409  llncvrlpln2  30416  islvol2aN  30451  lplncvrlvol2  30474  dalem-cly  30530  dalem44  30575  snatpsubN  30609  pointpsubN  30610  lncvrelatN  30640  cdlemblem  30652  paddasslem16  30694  paddidm  30700  pmodlem2  30706  pmapjoin  30711  llnexchb2  30728  llnexch2N  30729  pclfinclN  30809  linepsubclN  30810  lhpj1  30881  lhp2atnle  30892  lautcvr  30951  trlnidatb  31036  trlnid  31038  cdleme32e  31304  erng1lem  31846  erngdvlem4-rN  31858  diaelrnN  31905  diaf11N  31909  dibf11N  32021  cdlemn11pre  32070  dihord2pre  32085  dihord6apre  32116  dihvalrel  32139  dihglblem5apreN  32151  dihmeetlem13N  32179  mapdordlem2  32497  baerlem3lem2  32570  baerlem5alem2  32571  baerlem5blem2  32572  mapdheq2  32589
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 179
  Copyright terms: Public domain W3C validator