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

Theorem sylbid 207
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 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbid.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 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  ax11eq  2227  ax11el  2228  nlimsucg  4762  poltletr  5209  xp11  5244  xpcan  5245  xpcan2  5246  foconst  5604  fvmptdf  5755  suppss  5802  fnpr  5889  fnprOLD  5890  soisores  5986  isomin  5996  weniso  6014  ovmpt2df  6144  bropopvvv  6365  riotaxfrd  6517  eusvobj2  6518  smoiso  6560  tfrlem5  6577  tz7.48lem  6634  oevn0  6695  oaass  6740  omword1  6752  omlimcl  6757  odi  6758  oneo  6760  omeulem1  6761  oewordi  6770  oeworde  6772  oelimcl  6779  oaabs2  6824  omabs  6826  nnneo  6830  dom2lem  7083  fundmen  7116  onfin  7233  domfi  7266  dif1enOLD  7276  dif1en  7277  isfinite2  7301  unfilem1  7307  elfiun  7370  dffi3  7371  supisoex  7409  ordiso2  7417  ordtypelem7  7426  brwdom3  7483  unxpwdom2  7489  noinfepOLD  7548  cantnflem1  7578  cantnf  7582  r1sdom  7633  r1ord3g  7638  rankr1ai  7657  rankonidlem  7687  bndrank  7700  rankunb  7709  tcrank  7741  wdomfil  7875  wdomnumr  7878  alephordi  7888  alephdom  7895  dfac3  7935  dfac12lem3  7958  cfeq0  8069  cfsmolem  8083  sornom  8090  fin23lem28  8153  fin23lem30  8155  isf32lem2  8167  fin1a2lem9  8221  axcc2lem  8249  axdc3lem2  8264  axdc4lem  8268  ttukeylem5  8326  alephreg  8390  pwcfsdom  8391  fpwwe2lem13  8450  fpwwe2  8451  pwfseqlem3  8468  gchina  8507  inatsk  8586  intgru  8622  grur1  8628  grutsk1  8629  addcanpi  8709  mulcanpi  8710  addnidpi  8711  ltexnq  8785  ltbtwnnq  8788  genpss  8814  genpcd  8816  genpnmax  8817  addclprlem1  8826  mulclprlem  8829  distrlem1pr  8835  distrlem4pr  8836  distrlem5pr  8837  ltexprlem3  8848  ltexprlem6  8851  ltexpri  8853  reclem4pr  8860  axpre-sup  8977  lelttr  9098  ltletr  9099  letr  9100  le2add  9442  ltleadd  9443  lt2sub  9458  le2sub  9459  mulge0  9477  prodgt0  9787  squeeze0  9845  addltmul  10135  elnnz  10224  zextlt  10276  uzind2  10294  uzindOLD  10296  indstr  10477  qreccl  10526  rpnnen1lem1  10532  rpnnen1lem2  10533  rpnnen1lem3  10534  rpnnen1lem5  10536  xrlelttr  10678  xrltletr  10679  xrletr  10680  xrrebnd  10688  qbtwnre  10717  qbtwnxr  10718  qextlt  10721  qextle  10722  xltnegi  10734  xmulasslem  10796  xlemul1a  10799  iccid  10893  icoshft  10951  prunioo  10957  difreicc  10960  iccsplit  10961  fzm1  11057  elfznelfzo  11119  injresinjlem  11126  modirr  11213  om2uzf1oi  11220  seqf1olem1  11289  sqlecan  11414  facdiv  11505  facwordi  11507  faclbnd  11508  bcpasc  11539  hasheqf1oi  11562  hashdom  11580  hashgt12el  11609  hashgt12el2  11610  hash2pr  11614  hashtpg  11618  seqcoll  11639  sqrlem6  11980  resqrex  11983  absnid  12030  cau3lem  12085  sqreu  12091  rlim2lt  12218  rlim3  12219  o1lo1  12258  o1lo12  12259  rlimuni  12271  climuni  12273  lo1resb  12285  o1resb  12287  2clim  12293  o1rlimmul  12339  lo1le  12372  fsumss  12446  fsumabs  12507  cvgcmpce  12524  geomulcvg  12580  mertenslem2  12589  reeff1  12648  efieq1re  12727  dvdsmultr2  12812  dvdsleabs  12823  odd2np1lem  12834  odd2np1  12835  divalglem8  12847  sadcaddlem  12896  gcdneg  12953  gcddiv  12976  dvdssqim  12980  algcvga  12997  prmind2  13017  coprmdvds  13029  coprmdvds2  13030  qredeq  13033  euclemma  13035  nprmdvds1  13038  prmdvdsexpr  13043  prmfac1  13045  divgcdodd  13046  crt  13094  eulerthlem2  13098  fermltl  13100  coprimeprodsq2  13111  pythagtriplem2  13118  iserodd  13136  pcpremul  13144  pcdvdsb  13169  pc2dvds  13179  pc11  13180  pcfac  13195  prmpwdvds  13199  prmreclem4  13214  prmreclem5  13215  1arith  13222  4sqlem11  13250  vdwlem6  13281  vdwlem7  13282  vdwlem9  13284  vdwlem10  13285  vdwlem11  13286  ramub1lem2  13322  ramcl  13324  prmlem0  13355  firest  13587  imasaddfnlem  13680  imasvscafn  13689  erlecpbl  13702  xpsff1o  13720  setcmon  14169  setcepi  14170  setciso  14173  pltnle  14350  pltletr  14355  plelttr  14356  psref  14567  dirge  14609  imasmnd2  14659  imasgrp2  14860  ghmpreima  14954  gaorber  15012  mndodcongi  15108  sylow1lem1  15159  odcau  15165  sylow2alem1  15178  sylow2alem2  15179  lsmsubm  15214  lsmsubg  15215  lsmmod  15234  lsmdisj2  15241  efgtlen  15285  efgredlemc  15304  efgcpbllemb  15314  torsubg  15396  frgpnabllem1  15411  cyggexb  15435  gsumval3a  15439  dprdsubg  15509  dprddisj2  15524  dmdprdsplit2lem  15530  dmdprdsplit2  15531  ablfacrp  15551  ablfac1eulem  15557  pgpfac1lem3  15562  imasrng  15652  unitgrp  15699  lmhmima  16050  lsmcl  16082  lsmelval2  16084  lspsneleq  16114  lpiss  16248  xrsdsreclb  16668  gzrngunitlem  16686  znidomb  16765  frgpcyg  16777  tgtop  16961  neips  17100  neindisj  17104  restbas  17144  tgrest  17145  restcld  17158  restcldr  17160  ordtbas2  17177  ordtbas  17178  tgcn  17238  tgcnp  17239  subbascn  17240  cnconst2  17269  cnconst  17270  cnpresti  17274  cmpsublem  17384  tgcmp  17386  uncmp  17388  hauscmplem  17391  conndisj  17400  nconsubb  17407  1stcfb  17429  2ndc1stc  17435  1stcrest  17437  2ndcctbss  17439  1stccnp  17446  llyrest  17469  nllyrest  17470  nllyidm  17473  cldllycmp  17479  1stckgen  17507  txcls  17557  txbasval  17559  txcnpi  17561  txcnp  17573  ptcnplem  17574  txdis1cn  17588  txlly  17589  txnlly  17590  pthaus  17591  tx1stc  17603  xkohaus  17606  xkococn  17613  basqtop  17664  qtopeu  17669  qtoprest  17670  qtopomap  17671  qtopcmap  17672  kqfvima  17683  kqsat  17684  kqcldsat  17686  fbfinnfr  17794  fgfil  17828  fgabs  17832  trfil2  17840  ufilmax  17860  isufil2  17861  ufprim  17862  ufileu  17872  filufint  17873  cfinufil  17881  elfm2  17901  rnelfmlem  17905  rnelfm  17906  fmfnfmlem2  17908  fmfnfmlem4  17910  fmfnfm  17911  ufldom  17915  flffbas  17948  flimfnfcls  17981  alexsublem  17996  alexsubALT  18003  symgtgp  18052  divstgpopn  18070  divstgplem  18071  tsmsxplem1  18103  bldisj  18329  xbln0  18339  blss  18346  blin2  18349  blcls  18426  prdsxmslem2  18449  metustfbas  18477  xrsblre  18713  xrsmopn  18714  recld2  18716  reperflem  18720  reconnlem2  18729  cnmpt2pc  18824  cnheibor  18851  lebnumlem3  18859  nmhmcn  18999  cphsqrcl2  19020  iscau3  19102  iscau4  19103  iscmet3lem2  19116  lmcau  19136  cmetss  19138  bcth3  19153  cmetcusp1  19174  minveclem3b  19196  ivthlem2  19216  ivthlem3  19217  ovolctb  19253  ovolscalem1  19276  ovolicc2lem3  19282  ovolicc2lem4  19283  dyaddisjlem  19354  dyadmbllem  19358  opnmbllem  19360  subopnmbl  19363  volivth  19366  mbfimaopn2  19416  i1faddlem  19452  i1fmullem  19453  itg10a  19469  itg1ge0a  19470  mbfi1fseqlem4  19477  mbfi1flimlem  19481  dveflem  19730  dvlip2  19746  dvne0  19762  lhop1lem  19764  lhop1  19765  lhop2  19766  lhop  19767  dvcvx  19771  dvfsumrlim  19782  ftc1lem6  19792  itgsubst  19800  coe1mul3  19889  dvdsq1p  19950  coemullem  20035  coe1termlem  20043  dgrco  20060  coecj  20063  aaliou3lem7  20133  ulmcn  20182  reeff1o  20230  sincosq3sgn  20275  sincosq4sgn  20276  sineq0  20296  recosf1o  20304  efopn  20416  cxpge0  20441  cxpcn3lem  20498  cxpeq  20508  angpieqvd  20539  atantayl2  20645  rlimcnp  20671  xrlimcnp  20674  cxploglim  20683  ftalem2  20723  muval1  20783  ppiublem1  20853  chtub  20863  dchrmulcl  20900  dchrsum2  20919  bclbnd  20931  bposlem1  20935  bposlem5  20939  lgsdirnn0  20990  lgsqrlem2  20993  lgseisenlem2  21001  lgsquadlem1  21005  2sqblem  21028  chtppilimlem2  21035  dchrisumlem3  21052  dchrisum0lem1  21077  pntlem3  21170  ostth2lem2  21195  ostth3  21199  usgra0v  21258  usgraedgrn  21267  usgra2edg  21268  usgrarnedg  21270  usgra1v  21275  usgraidx2v  21278  usgrafisindb0  21288  usgrafisindb1  21289  nbusgra  21306  nbgraisvtx  21309  nbgraf1olem1  21317  nbgraf1olem5  21321  nb3graprlem1  21326  cusgrarn  21334  cusgrasize2inds  21352  uvtxnbgra  21368  trliswlk  21403  pthdepisspth  21428  redwlk  21454  cyclnspth  21466  fargshiftf1  21472  usgrcyclnl1  21475  usgrcyclnl2  21476  3v3e3cycl1  21479  4cycl4v4e  21501  4cycl4dv  21502  4cycl4dv4e  21503  vdusgra0nedg  21527  usgravd0nedg  21531  isabloda  21735  blocnilem  22153  ipasslem11  22189  h1de2ctlem  22905  spansneleq  22920  spansnss  22921  normcan  22926  spansncvi  23002  nmcexi  23377  elpjrn  23541  stadd3i  23599  cvcon3  23635  dmdbr5  23659  ssdmd2  23665  atom1d  23704  superpos  23705  cvexchlem  23719  atcv0eq  23730  atexch  23732  atcvat4i  23748  atdmd  23749  atmd2  23751  mdsymlem3  23756  mdsymlem5  23758  sumdmdlem  23769  cdjreui  23783  cnre2csqlem  24112  ballotlemfrceq  24565  erdszelem4  24659  erdszelem9  24664  sconpi1  24705  relexpsucl  24911  rtrclreclem.trans  24925  mulge0b  24970  fprodss  25053  dvdspw  25127  predpo  25208  uzsinds  25240  omsinds  25243  soseq  25278  sltres  25342  nodenselem3  25361  nodenselem4  25362  nodenselem5  25363  nodenselem8  25366  nofulllem5  25384  brbtwn2  25558  colinearalg  25563  axbtwnid  25592  axlowdimlem14  25608  axlowdimlem15  25609  axcontlem2  25618  cgrid2  25651  cgrextend  25656  btwnswapid2  25666  btwnexch3  25668  btwnexch  25673  ifscgr  25692  btwnxfr  25704  colineardim1  25709  colinearxfr  25723  lineext  25724  fscgr  25728  brsegle2  25757  seglecgr12im  25758  seglecgr12  25759  segletr  25762  segleantisym  25763  colinbtwnle  25766  broutsideof2  25770  outsideofeq  25778  outsidele  25780  lineunray  25795  lineelsb2  25796  elhf2  25830  ordtopcon  25903  ordtopt0  25906  ovoliunnfl  25953  voliunnfl  25955  itg2addnclem  25957  itg2addnclem2  25958  itg2addnc  25959  itg2gt0cn  25960  ftc1cnnc  25979  areacirclem2  25982  areacirclem3  25983  areacirclem4  25984  areacirclem5  25986  areacirc  25988  nn0prpwlem  26016  nn0prpw  26017  cldbnd  26020  fgmin  26090  tailfb  26097  indexdom  26127  fzmul  26135  fzadd2  26136  sdclem2  26137  sdclem1  26138  fdc  26140  incsequz  26143  sstotbnd2  26174  equivbnd  26190  prdstotbnd  26194  grpokerinj  26251  keridl  26333  smprngopr  26353  ispridlc  26371  dmncan2  26378  diophin  26522  diophun  26523  fphpdo  26569  pellexlem1  26583  pell1234qrne0  26607  pell14qrgt0  26613  pell1234qrdich  26615  pell1qrge1  26624  elpell1qr2  26626  pell1qrgap  26628  pellfundex  26640  rmxypairf1o  26665  jm2.26a  26762  setindtr  26786  rpnnen3  26794  dnnumch3  26813  fnwe2lem2  26817  pwssplit4  26860  lindfrn  26960  f1lindf  26961  hbtlem5  27001  pmtrfrn  27069  symggen  27080  psgnunilem2  27087  3vfriswmgra  27758  1to2vfriswmgra  27759  2pthfrgra  27764  frgrancvvdeqlem2  27783  frgrawopreg1  27802  frgrawopreg2  27803  lshpdisj  29102  lsat0cv  29148  lcvexchlem4  29152  lcvexchlem5  29153  lsatcv0eq  29162  lfl1dim  29236  lfl1dim2N  29237  lkrss2N  29284  lkreqN  29285  cmtbr3N  29369  omlfh3N  29374  cvrnbtwn  29386  cvrcon3b  29392  atnle  29432  cvlatexch1  29451  cvlsupr2  29458  hlrelat2  29517  cvrexchlem  29533  cvrat  29536  atcvr0eq  29540  atcvrj0  29542  atltcvr  29549  cvrat4  29557  lvolex3N  29652  islpln2a  29662  lplnriaN  29664  llncvrlpln2  29671  islvol2aN  29706  lplncvrlvol2  29729  dalem-cly  29785  dalem44  29830  snatpsubN  29864  pointpsubN  29865  lncvrelatN  29895  cdlemblem  29907  paddasslem16  29949  paddidm  29955  pmodlem2  29961  pmapjoin  29966  llnexchb2  29983  llnexch2N  29984  pclfinclN  30064  linepsubclN  30065  lhpj1  30136  lhp2atnle  30147  lautcvr  30206  trlnidatb  30291  trlnid  30293  cdleme32e  30559  erng1lem  31101  erngdvlem4-rN  31113  diaelrnN  31160  diaf11N  31164  dibf11N  31276  cdlemn11pre  31325  dihord2pre  31340  dihord6apre  31371  dihvalrel  31394  dihglblem5apreN  31406  dihmeetlem13N  31434  mapdordlem2  31752  baerlem3lem2  31825  baerlem5alem2  31826  baerlem5blem2  31827  mapdheq2  31844
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