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

Theorem sylbid 206
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 198 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbid.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 40 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr4d  259  ax11eq  2132  ax11el  2133  nlimsucg  4633  poltletr  5078  xp11  5111  xpcan  5112  xpcan2  5113  foconst  5462  fvmptdf  5611  suppss  5658  soisores  5824  isomin  5834  weniso  5852  ovmpt2df  5979  riotaxfrd  6336  eusvobj2  6337  smoiso  6379  tfrlem5  6396  tz7.48lem  6453  oevn0  6514  oaass  6559  omword1  6571  omlimcl  6576  odi  6577  oneo  6579  omeulem1  6580  oewordi  6589  oeworde  6591  oelimcl  6598  oaabs2  6643  omabs  6645  nnneo  6649  dom2lem  6901  fundmen  6934  onfin  7051  domfi  7084  dif1enOLD  7090  dif1en  7091  isfinite2  7115  unfilem1  7121  elfiun  7183  dffi3  7184  supisoex  7222  ordiso2  7230  ordtypelem7  7239  brwdom3  7296  unxpwdom2  7302  noinfepOLD  7361  cantnflem1  7391  cantnf  7395  r1sdom  7446  r1ord3g  7451  rankr1ai  7470  rankonidlem  7500  bndrank  7513  rankunb  7522  tcrank  7554  wdomfil  7688  wdomnumr  7691  alephordi  7701  alephdom  7708  dfac3  7748  dfac12lem3  7771  cfeq0  7882  cfsmolem  7896  sornom  7903  fin23lem28  7966  fin23lem30  7968  isf32lem2  7980  fin1a2lem9  8034  axcc2lem  8062  axdc3lem2  8077  axdc4lem  8081  ttukeylem5  8140  alephreg  8204  pwcfsdom  8205  fpwwe2lem13  8264  fpwwe2  8265  pwfseqlem3  8282  gchina  8321  inatsk  8400  intgru  8436  grur1  8442  grutsk1  8443  addcanpi  8523  mulcanpi  8524  addnidpi  8525  ltexnq  8599  ltbtwnnq  8602  genpss  8628  genpcd  8630  genpnmax  8631  addclprlem1  8640  mulclprlem  8643  distrlem1pr  8649  distrlem4pr  8650  distrlem5pr  8651  ltexprlem3  8662  ltexprlem6  8665  ltexpri  8667  reclem4pr  8674  axpre-sup  8791  lelttr  8912  ltletr  8913  letr  8914  le2add  9256  ltleadd  9257  lt2sub  9272  le2sub  9273  mulge0  9291  prodgt0  9601  squeeze0  9659  addltmul  9947  elnnz  10034  zextlt  10086  uzind2  10104  uzindOLD  10106  indstr  10287  qreccl  10336  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  xrlelttr  10487  xrltletr  10488  xrletr  10489  xrrebnd  10497  qbtwnre  10526  qbtwnxr  10527  qextlt  10530  qextle  10531  xltnegi  10543  xmulasslem  10605  xlemul1a  10608  iccid  10701  icoshft  10758  prunioo  10764  difreicc  10767  iccsplit  10768  fzm1  10862  modirr  11009  om2uzf1oi  11016  seqf1olem1  11085  sqlecan  11209  facdiv  11300  facwordi  11302  faclbnd  11303  bcpasc  11333  hashdom  11361  seqcoll  11401  sqrlem6  11733  resqrex  11736  absnid  11783  cau3lem  11838  sqreu  11844  rlim2lt  11971  rlim3  11972  o1lo1  12011  o1lo12  12012  rlimuni  12024  climuni  12026  lo1resb  12038  o1resb  12040  2clim  12046  o1rlimmul  12092  lo1le  12125  fsumss  12198  fsumabs  12259  cvgcmpce  12276  geomulcvg  12332  mertenslem2  12341  reeff1  12400  efieq1re  12479  dvdsmultr2  12564  dvdsleabs  12575  odd2np1lem  12586  odd2np1  12587  divalglem8  12599  sadcaddlem  12648  gcdneg  12705  gcddiv  12728  dvdssqim  12732  algcvga  12749  prmind2  12769  coprmdvds  12781  coprmdvds2  12782  qredeq  12785  euclemma  12787  nprmdvds1  12790  prmdvdsexpr  12795  prmfac1  12797  divgcdodd  12798  crt  12846  eulerthlem2  12850  fermltl  12852  coprimeprodsq2  12863  pythagtriplem2  12870  iserodd  12888  pcpremul  12896  pcdvdsb  12921  pc2dvds  12931  pc11  12932  pcfac  12947  prmpwdvds  12951  prmreclem4  12966  prmreclem5  12967  1arith  12974  4sqlem11  13002  vdwlem6  13033  vdwlem7  13034  vdwlem9  13036  vdwlem10  13037  vdwlem11  13038  ramub1lem2  13074  ramcl  13076  prmlem0  13107  firest  13337  imasaddfnlem  13430  imasvscafn  13439  erlecpbl  13452  xpsff1o  13470  setcmon  13919  setcepi  13920  setciso  13923  pltnle  14100  pltletr  14105  plelttr  14106  psref  14317  dirge  14359  imasmnd2  14409  imasgrp2  14610  ghmpreima  14704  gaorber  14762  mndodcongi  14858  sylow1lem1  14909  odcau  14915  sylow2alem1  14928  sylow2alem2  14929  lsmsubm  14964  lsmsubg  14965  lsmmod  14984  lsmdisj2  14991  efgtlen  15035  efgredlemc  15054  efgcpbllemb  15064  torsubg  15146  frgpnabllem1  15161  cyggexb  15185  gsumval3a  15189  dprdsubg  15259  dprddisj2  15274  dmdprdsplit2lem  15280  dmdprdsplit2  15281  ablfacrp  15301  ablfac1eulem  15307  pgpfac1lem3  15312  imasrng  15402  unitgrp  15449  lmhmima  15804  lsmcl  15836  lsmelval2  15838  lspsneleq  15868  lpiss  16002  xrsdsreclb  16418  gzrngunitlem  16436  znidomb  16515  frgpcyg  16527  tgtop  16711  neips  16850  neindisj  16854  restbas  16889  tgrest  16890  restcld  16903  restcldr  16905  ordtbas2  16921  ordtbas  16922  tgcn  16982  tgcnp  16983  subbascn  16984  cnconst2  17011  cnconst  17012  cnpresti  17016  cmpsublem  17126  tgcmp  17128  uncmp  17130  hauscmplem  17133  conndisj  17142  nconsubb  17149  1stcfb  17171  2ndc1stc  17177  1stcrest  17179  2ndcctbss  17181  1stccnp  17188  llyrest  17211  nllyrest  17212  nllyidm  17215  cldllycmp  17221  1stckgen  17249  txcls  17299  txbasval  17301  txcnpi  17302  txcnp  17314  ptcnplem  17315  txdis1cn  17329  txlly  17330  txnlly  17331  pthaus  17332  tx1stc  17344  xkohaus  17347  xkococn  17354  basqtop  17402  qtopeu  17407  qtoprest  17408  qtopomap  17409  qtopcmap  17410  kqfvima  17421  kqsat  17422  kqcldsat  17424  fbfinnfr  17536  fgfil  17570  fgabs  17574  trfil2  17582  ufilmax  17602  isufil2  17603  ufprim  17604  ufileu  17614  filufint  17615  cfinufil  17623  elfm2  17643  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  ufldom  17657  flffbas  17690  flimfnfcls  17723  alexsublem  17738  alexsubALT  17745  symgtgp  17784  divstgpopn  17802  divstgplem  17803  tsmsxplem1  17835  bldisj  17955  xbln0  17965  blss  17972  blin2  17975  blcls  18052  prdsxmslem2  18075  xrsblre  18317  xrsmopn  18318  recld2  18320  reperflem  18323  reconnlem2  18332  cnmpt2pc  18426  cnheibor  18453  lebnumlem3  18461  nmhmcn  18601  cphsqrcl2  18622  iscau3  18704  iscau4  18705  iscmet3lem2  18718  lmcau  18738  cmetss  18740  bcth3  18753  minveclem3b  18792  ivthlem2  18812  ivthlem3  18813  ovolctb  18849  ovolscalem1  18872  ovolicc2lem3  18878  ovolicc2lem4  18879  dyaddisjlem  18950  dyadmbllem  18954  opnmbllem  18956  subopnmbl  18959  volivth  18962  mbfimaopn2  19012  i1faddlem  19048  i1fmullem  19049  itg10a  19065  itg1ge0a  19066  mbfi1fseqlem4  19073  mbfi1flimlem  19077  dveflem  19326  dvlip2  19342  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvcvx  19367  dvfsumrlim  19378  ftc1lem6  19388  itgsubst  19396  coe1mul3  19485  dvdsq1p  19546  coemullem  19631  coe1termlem  19639  dgrco  19656  coecj  19659  aaliou3lem7  19729  ulmcn  19776  reeff1o  19823  sincosq3sgn  19868  sincosq4sgn  19869  sineq0  19889  recosf1o  19897  efopn  20005  cxpge0  20030  cxpcn3lem  20087  cxpeq  20097  angpieqvd  20128  atantayl2  20234  rlimcnp  20260  xrlimcnp  20263  cxploglim  20272  ftalem2  20311  muval1  20371  ppiublem1  20441  chtub  20451  dchrmulcl  20488  dchrsum2  20507  bclbnd  20519  bposlem1  20523  bposlem5  20527  lgsdirnn0  20578  lgsqrlem2  20581  lgseisenlem2  20589  lgsquadlem1  20593  2sqblem  20616  chtppilimlem2  20623  dchrisumlem3  20640  dchrisum0lem1  20665  pntlem3  20758  ostth2lem2  20783  ostth3  20787  isabloda  20966  blocnilem  21382  ipasslem11  21418  h1de2ctlem  22134  spansneleq  22149  spansnss  22150  normcan  22155  spansncvi  22231  nmcexi  22606  elpjrn  22770  stadd3i  22828  cvcon3  22864  dmdbr5  22888  ssdmd2  22894  atom1d  22933  superpos  22934  cvexchlem  22948  atcv0eq  22959  atexch  22961  atcvat4i  22977  atdmd  22978  atmd2  22980  mdsymlem3  22985  mdsymlem5  22987  sumdmdlem  22998  cdjreui  23012  cnre2csqlem  23294  cnre2csqima  23295  erdszelem4  23725  erdszelem9  23730  sconpi1  23770  relexpsucl  24028  rtrclreclem.trans  24043  mulge0b  24086  dvdspw  24103  predpo  24184  uzsinds  24216  omsinds  24219  soseq  24254  sltres  24318  nodenselem3  24337  nodenselem4  24338  nodenselem5  24339  nodenselem8  24342  nofulllem5  24360  brbtwn2  24533  colinearalg  24538  axbtwnid  24567  axlowdimlem14  24583  axlowdimlem15  24584  axcontlem2  24593  cgrid2  24626  cgrextend  24631  btwnswapid2  24641  btwnexch3  24643  btwnexch  24648  ifscgr  24667  btwnxfr  24679  colineardim1  24684  colinearxfr  24698  lineext  24699  fscgr  24703  brsegle2  24732  seglecgr12im  24733  seglecgr12  24734  segletr  24737  segleantisym  24738  colinbtwnle  24741  broutsideof2  24745  outsideofeq  24753  outsidele  24755  lineunray  24770  lineelsb2  24771  elhf2  24805  ordtopcon  24878  ordtopt0  24881  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  areacirclem5  24929  areacirc  24931  copsexgb  24966  repfuntw  25160  elioo1t3  25502  cmptdst  25568  islimrs3  25581  bwt2  25592  iintlem1  25610  dualded  25783  ismonb2  25812  icmpmon  25816  idmon  25817  isepib2  25822  lineval5a  26088  lineval6a  26089  segline  26141  nn0prpwlem  26238  nn0prpw  26239  cldbnd  26244  fgmin  26319  tailfb  26326  indexdom  26413  fzmul  26443  fzadd2  26444  sdclem2  26452  sdclem1  26453  fdc  26455  incsequz  26458  sstotbnd2  26498  equivbnd  26514  prdstotbnd  26518  grpokerinj  26575  keridl  26657  smprngopr  26677  ispridlc  26695  dmncan2  26702  diophin  26852  diophun  26853  fphpdo  26900  pellexlem1  26914  pell1234qrne0  26938  pell14qrgt0  26944  pell1234qrdich  26946  pell1qrge1  26955  elpell1qr2  26957  pell1qrgap  26959  pellfundex  26971  rmxypairf1o  26996  jm2.26a  27093  setindtr  27117  rpnnen3  27125  dnnumch3  27144  fnwe2lem2  27148  pwssplit4  27191  lindfrn  27291  f1lindf  27292  hbtlem5  27332  pmtrfrn  27400  symggen  27411  psgnunilem2  27418  usgra0v  28117  usgraedgrn  28125  usgra1v  28126  nbusgra  28143  nbgraisvtx  28146  uvtxnbgra  28165  cusgrauvtx  28168  3vfriswmgra  28183  1to2vfriswmgra  28184  lshpdisj  29177  lsat0cv  29223  lcvexchlem4  29227  lcvexchlem5  29228  lsatcv0eq  29237  lfl1dim  29311  lfl1dim2N  29312  lkrss2N  29359  lkreqN  29360  cmtbr3N  29444  omlfh3N  29449  cvrnbtwn  29461  cvrcon3b  29467  atnle  29507  cvlatexch1  29526  cvlsupr2  29533  hlrelat2  29592  cvrexchlem  29608  cvrat  29611  atcvr0eq  29615  atcvrj0  29617  atltcvr  29624  cvrat4  29632  lvolex3N  29727  islpln2a  29737  lplnriaN  29739  llncvrlpln2  29746  islvol2aN  29781  lplncvrlvol2  29804  dalem-cly  29860  dalem44  29905  snatpsubN  29939  pointpsubN  29940  lncvrelatN  29970  cdlemblem  29982  paddasslem16  30024  paddidm  30030  pmodlem2  30036  pmapjoin  30041  llnexchb2  30058  llnexch2N  30059  pclfinclN  30139  linepsubclN  30140  lhpj1  30211  lhp2atnle  30222  lautcvr  30281  trlnidatb  30366  trlnid  30368  cdleme32e  30634  erng1lem  31176  erngdvlem4-rN  31188  diaelrnN  31235  diaf11N  31239  dibf11N  31351  cdlemn11pre  31400  dihord2pre  31415  dihord6apre  31446  dihvalrel  31469  dihglblem5apreN  31481  dihmeetlem13N  31509  mapdordlem2  31827  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  mapdheq2  31919
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 177
  Copyright terms: Public domain W3C validator