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  2243  ax11el  2244  nlimsucg  4781  poltletr  5228  xp11  5263  xpcan  5264  xpcan2  5265  foconst  5623  fvmptdf  5775  suppss  5822  fnpr  5909  fnprOLD  5910  soisores  6006  isomin  6016  weniso  6034  ovmpt2df  6164  bropopvvv  6385  f1o2ndf1  6413  riotaxfrd  6540  eusvobj2  6541  smoiso  6583  tfrlem5  6600  tz7.48lem  6657  oevn0  6718  oaass  6763  omword1  6775  omlimcl  6780  odi  6781  oneo  6783  omeulem1  6784  oewordi  6793  oeworde  6795  oelimcl  6802  oaabs2  6847  omabs  6849  nnneo  6853  dom2lem  7106  fundmen  7139  onfin  7256  domfi  7289  dif1enOLD  7299  dif1en  7300  isfinite2  7324  unfilem1  7330  elfiun  7393  dffi3  7394  supisoex  7432  ordiso2  7440  ordtypelem7  7449  brwdom3  7506  unxpwdom2  7512  noinfepOLD  7571  cantnflem1  7601  cantnf  7605  r1sdom  7656  r1ord3g  7661  rankr1ai  7680  rankonidlem  7710  bndrank  7723  rankunb  7732  tcrank  7764  wdomfil  7898  wdomnumr  7901  alephordi  7911  alephdom  7918  dfac3  7958  dfac12lem3  7981  cfeq0  8092  cfsmolem  8106  sornom  8113  fin23lem28  8176  fin23lem30  8178  isf32lem2  8190  fin1a2lem9  8244  axcc2lem  8272  axdc3lem2  8287  axdc4lem  8291  ttukeylem5  8349  alephreg  8413  pwcfsdom  8414  fpwwe2lem13  8473  fpwwe2  8474  pwfseqlem3  8491  gchina  8530  inatsk  8609  intgru  8645  grur1  8651  grutsk1  8652  addcanpi  8732  mulcanpi  8733  addnidpi  8734  ltexnq  8808  ltbtwnnq  8811  genpss  8837  genpcd  8839  genpnmax  8840  addclprlem1  8849  mulclprlem  8852  distrlem1pr  8858  distrlem4pr  8859  distrlem5pr  8860  ltexprlem3  8871  ltexprlem6  8874  ltexpri  8876  reclem4pr  8883  axpre-sup  9000  lelttr  9121  ltletr  9122  letr  9123  le2add  9466  ltleadd  9467  lt2sub  9482  le2sub  9483  mulge0  9501  prodgt0  9811  squeeze0  9869  addltmul  10159  elnnz  10248  zextlt  10300  uzind2  10318  uzindOLD  10320  indstr  10501  qreccl  10550  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  xrlelttr  10702  xrltletr  10703  xrletr  10704  xrrebnd  10712  qbtwnre  10741  qbtwnxr  10742  qextlt  10745  qextle  10746  xltnegi  10758  xmulasslem  10820  xlemul1a  10823  iccid  10917  icoshft  10975  prunioo  10981  difreicc  10984  iccsplit  10985  fzm1  11082  elfznelfzo  11147  injresinjlem  11154  modirr  11241  om2uzf1oi  11248  seqf1olem1  11317  sqlecan  11442  facdiv  11533  facwordi  11535  faclbnd  11536  bcpasc  11567  hasheqf1oi  11590  hashdom  11608  hashgt12el  11637  hashgt12el2  11638  hash2pr  11642  hashtpg  11646  seqcoll  11667  sqrlem6  12008  resqrex  12011  absnid  12058  cau3lem  12113  sqreu  12119  rlim2lt  12246  rlim3  12247  o1lo1  12286  o1lo12  12287  rlimuni  12299  climuni  12301  lo1resb  12313  o1resb  12315  2clim  12321  o1rlimmul  12367  lo1le  12400  fsumss  12474  fsumabs  12535  cvgcmpce  12552  geomulcvg  12608  mertenslem2  12617  reeff1  12676  efieq1re  12755  dvdsmultr2  12840  dvdsleabs  12851  odd2np1lem  12862  odd2np1  12863  divalglem8  12875  sadcaddlem  12924  gcdneg  12981  gcddiv  13004  dvdssqim  13008  algcvga  13025  prmind2  13045  coprmdvds  13057  coprmdvds2  13058  qredeq  13061  euclemma  13063  nprmdvds1  13066  prmdvdsexpr  13071  prmfac1  13073  divgcdodd  13074  crt  13122  eulerthlem2  13126  fermltl  13128  coprimeprodsq2  13139  pythagtriplem2  13146  iserodd  13164  pcpremul  13172  pcdvdsb  13197  pc2dvds  13207  pc11  13208  pcfac  13223  prmpwdvds  13227  prmreclem4  13242  prmreclem5  13243  1arith  13250  4sqlem11  13278  vdwlem6  13309  vdwlem7  13310  vdwlem9  13312  vdwlem10  13313  vdwlem11  13314  ramub1lem2  13350  ramcl  13352  prmlem0  13383  firest  13615  imasaddfnlem  13708  imasvscafn  13717  erlecpbl  13730  xpsff1o  13748  setcmon  14197  setcepi  14198  setciso  14201  pltnle  14378  pltletr  14383  plelttr  14384  psref  14595  dirge  14637  imasmnd2  14687  imasgrp2  14888  ghmpreima  14982  gaorber  15040  mndodcongi  15136  sylow1lem1  15187  odcau  15193  sylow2alem1  15206  sylow2alem2  15207  lsmsubm  15242  lsmsubg  15243  lsmmod  15262  lsmdisj2  15269  efgtlen  15313  efgredlemc  15332  efgcpbllemb  15342  torsubg  15424  frgpnabllem1  15439  cyggexb  15463  gsumval3a  15467  dprdsubg  15537  dprddisj2  15552  dmdprdsplit2lem  15558  dmdprdsplit2  15559  ablfacrp  15579  ablfac1eulem  15585  pgpfac1lem3  15590  imasrng  15680  unitgrp  15727  lmhmima  16078  lsmcl  16110  lsmelval2  16112  lspsneleq  16142  lpiss  16276  xrsdsreclb  16700  gzrngunitlem  16718  znidomb  16797  frgpcyg  16809  tgtop  16993  neips  17132  neindisj  17136  restbas  17176  tgrest  17177  restcld  17190  restcldr  17192  ordtbas2  17209  ordtbas  17210  tgcn  17270  tgcnp  17271  subbascn  17272  cnconst2  17301  cnconst  17302  cnpresti  17306  cmpsublem  17416  tgcmp  17418  uncmp  17420  hauscmplem  17423  conndisj  17432  nconsubb  17439  1stcfb  17461  2ndc1stc  17467  1stcrest  17469  2ndcctbss  17471  1stccnp  17478  llyrest  17501  nllyrest  17502  nllyidm  17505  cldllycmp  17511  1stckgen  17539  txcls  17589  txbasval  17591  txcnpi  17593  txcnp  17605  ptcnplem  17606  txdis1cn  17620  txlly  17621  txnlly  17622  pthaus  17623  tx1stc  17635  xkohaus  17638  xkococn  17645  basqtop  17696  qtopeu  17701  qtoprest  17702  qtopomap  17703  qtopcmap  17704  kqfvima  17715  kqsat  17716  kqcldsat  17718  fbfinnfr  17826  fgfil  17860  fgabs  17864  trfil2  17872  ufilmax  17892  isufil2  17893  ufprim  17894  ufileu  17904  filufint  17905  cfinufil  17913  elfm2  17933  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  ufldom  17947  flffbas  17980  flimfnfcls  18013  alexsublem  18028  alexsubALT  18035  symgtgp  18084  divstgpopn  18102  divstgplem  18103  tsmsxplem1  18135  bldisj  18381  xbln0  18397  blssps  18407  blss  18408  blin2  18412  blcls  18489  prdsxmslem2  18512  metustfbasOLD  18548  metustfbas  18549  xrsblre  18795  xrsmopn  18796  recld2  18798  reperflem  18802  reconnlem2  18811  cnmpt2pc  18906  cnheibor  18933  lebnumlem3  18941  nmhmcn  19081  cphsqrcl2  19102  iscau3  19184  iscau4  19185  iscmet3lem2  19198  lmcau  19218  cmetss  19220  bcth3  19237  cmetcusp1OLD  19258  cmetcusp1  19259  minveclem3b  19282  ivthlem2  19302  ivthlem3  19303  ovolctb  19339  ovolscalem1  19362  ovolicc2lem3  19368  ovolicc2lem4  19369  dyaddisjlem  19440  dyadmbllem  19444  opnmbllem  19446  subopnmbl  19449  volivth  19452  mbfimaopn2  19502  i1faddlem  19538  i1fmullem  19539  itg10a  19555  itg1ge0a  19556  mbfi1fseqlem4  19563  mbfi1flimlem  19567  dveflem  19816  dvlip2  19832  dvne0  19848  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvcvx  19857  dvfsumrlim  19868  ftc1lem6  19878  itgsubst  19886  coe1mul3  19975  dvdsq1p  20036  coemullem  20121  coe1termlem  20129  dgrco  20146  coecj  20149  aaliou3lem7  20219  ulmcn  20268  reeff1o  20316  sincosq3sgn  20361  sincosq4sgn  20362  sineq0  20382  recosf1o  20390  efopn  20502  cxpge0  20527  cxpcn3lem  20584  cxpeq  20594  angpieqvd  20625  atantayl2  20731  rlimcnp  20757  xrlimcnp  20760  cxploglim  20769  ftalem2  20809  muval1  20869  ppiublem1  20939  chtub  20949  dchrmulcl  20986  dchrsum2  21005  bclbnd  21017  bposlem1  21021  bposlem5  21025  lgsdirnn0  21076  lgsqrlem2  21079  lgseisenlem2  21087  lgsquadlem1  21091  2sqblem  21114  chtppilimlem2  21121  dchrisumlem3  21138  dchrisum0lem1  21163  pntlem3  21256  ostth2lem2  21281  ostth3  21285  usgra0v  21344  usgraedgrn  21354  usgra2edg  21355  usgrarnedg  21357  usgra1v  21362  usgraidx2v  21365  usgrafisindb0  21375  usgrafisindb1  21376  nbgraisvtx  21396  nbgraf1olem1  21404  nbgraf1olem5  21408  nb3graprlem1  21413  cusgrarn  21421  cusgrasize2inds  21439  uvtxnbgra  21455  trliswlk  21492  pthdepisspth  21527  redwlk  21559  cyclnspth  21571  fargshiftf1  21577  usgrcyclnl1  21580  usgrcyclnl2  21581  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv  21607  4cycl4dv4e  21608  vdusgra0nedg  21632  usgravd0nedg  21636  isabloda  21840  blocnilem  22258  ipasslem11  22294  h1de2ctlem  23010  spansneleq  23025  spansnss  23026  normcan  23031  spansncvi  23107  nmcexi  23482  elpjrn  23646  stadd3i  23704  cvcon3  23740  dmdbr5  23764  ssdmd2  23770  atom1d  23809  superpos  23810  cvexchlem  23824  atcv0eq  23835  atexch  23837  atcvat4i  23853  atdmd  23854  atmd2  23856  mdsymlem3  23861  mdsymlem5  23863  sumdmdlem  23874  cdjreui  23888  cnre2csqlem  24261  ballotlemfrceq  24739  erdszelem4  24833  erdszelem9  24838  sconpi1  24879  relexpsucl  25085  rtrclreclem.trans  25099  mulge0b  25144  fprodss  25227  dvdspw  25317  predpo  25398  uzsinds  25430  omsinds  25433  soseq  25468  sltres  25532  nodenselem3  25551  nodenselem4  25552  nodenselem5  25553  nodenselem8  25556  nofulllem5  25574  brbtwn2  25748  colinearalg  25753  axbtwnid  25782  axlowdimlem14  25798  axlowdimlem15  25799  axcontlem2  25808  cgrid2  25841  cgrextend  25846  btwnswapid2  25856  btwnexch3  25858  btwnexch  25863  ifscgr  25882  btwnxfr  25894  colineardim1  25899  colinearxfr  25913  lineext  25914  fscgr  25918  brsegle2  25947  seglecgr12im  25948  seglecgr12  25949  segletr  25952  segleantisym  25953  colinbtwnle  25956  broutsideof2  25960  outsideofeq  25968  outsidele  25970  lineunray  25985  lineelsb2  25986  elhf2  26020  ordtopcon  26093  ordtopt0  26096  mblfinlem  26143  mblfinlem2  26144  ovoliunnfl  26147  voliunnfl  26149  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2gt0cn  26159  ftc1cnnc  26178  areacirclem2  26181  areacirclem3  26182  areacirclem4  26183  areacirclem5  26185  areacirc  26187  nn0prpwlem  26215  nn0prpw  26216  cldbnd  26219  fgmin  26289  tailfb  26296  indexdom  26326  fzmul  26334  fzadd2  26335  sdclem2  26336  sdclem1  26337  fdc  26339  incsequz  26342  sstotbnd2  26373  equivbnd  26389  prdstotbnd  26393  grpokerinj  26450  keridl  26532  smprngopr  26552  ispridlc  26570  dmncan2  26577  diophin  26721  diophun  26722  fphpdo  26768  pellexlem1  26782  pell1234qrne0  26806  pell14qrgt0  26812  pell1234qrdich  26814  pell1qrge1  26823  elpell1qr2  26825  pell1qrgap  26827  pellfundex  26839  rmxypairf1o  26864  jm2.26a  26961  setindtr  26985  rpnnen3  26993  dnnumch3  27012  fnwe2lem2  27016  pwssplit4  27059  lindfrn  27159  f1lindf  27160  hbtlem5  27200  pmtrfrn  27268  symggen  27279  psgnunilem2  27286  ubmelm1fzo  27987  hashimarni  27995  swrd0swrd  28009  swrdswrd  28011  swrdccatin12lem3a  28021  swrdccatin12b  28027  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspth  28038  spthdifv  28039  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  2wlkonot3v  28072  2spthonot3v  28073  el2wlksotot  28079  usg2wlkonot  28080  usg2wotspth  28081  2spontn0vne  28084  usg2spthonot  28085  usg2spthonot0  28086  3vfriswmgra  28109  1to2vfriswmgra  28110  2pthfrgra  28115  frgrancvvdeqlem2  28134  frgrawopreg1  28153  frgrawopreg2  28154  frg2wot1  28160  frg2woteqm  28162  frg2woteq  28163  2spotiundisj  28165  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  frgregordn0  28173  lshpdisj  29470  lsat0cv  29516  lcvexchlem4  29520  lcvexchlem5  29521  lsatcv0eq  29530  lfl1dim  29604  lfl1dim2N  29605  lkrss2N  29652  lkreqN  29653  cmtbr3N  29737  omlfh3N  29742  cvrnbtwn  29754  cvrcon3b  29760  atnle  29800  cvlatexch1  29819  cvlsupr2  29826  hlrelat2  29885  cvrexchlem  29901  cvrat  29904  atcvr0eq  29908  atcvrj0  29910  atltcvr  29917  cvrat4  29925  lvolex3N  30020  islpln2a  30030  lplnriaN  30032  llncvrlpln2  30039  islvol2aN  30074  lplncvrlvol2  30097  dalem-cly  30153  dalem44  30198  snatpsubN  30232  pointpsubN  30233  lncvrelatN  30263  cdlemblem  30275  paddasslem16  30317  paddidm  30323  pmodlem2  30329  pmapjoin  30334  llnexchb2  30351  llnexch2N  30352  pclfinclN  30432  linepsubclN  30433  lhpj1  30504  lhp2atnle  30515  lautcvr  30574  trlnidatb  30659  trlnid  30661  cdleme32e  30927  erng1lem  31469  erngdvlem4-rN  31481  diaelrnN  31528  diaf11N  31532  dibf11N  31644  cdlemn11pre  31693  dihord2pre  31708  dihord6apre  31739  dihvalrel  31762  dihglblem5apreN  31774  dihmeetlem13N  31802  mapdordlem2  32120  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  mapdheq2  32212
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