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

Theorem syl6 31
Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)
Hypotheses
Ref Expression
syl6.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6
StepHypRef Expression
1 syl6.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6.2 . . 3  |-  ( ch 
->  th )
32a1i 11 . 2  |-  ( ps 
->  ( ch  ->  th )
)
41, 3sylcom 27 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl56  32  syl6com  33  a1dd  44  syl6mpi  60  syl6c  62  com34  79  con1d  118  expi  143  looinv  175  syl6ib  218  syl6ibr  219  syl6bi  220  syl6bir  221  jaoi  369  pm2.37  818  pm2.81  825  oplem1  931  3jao  1245  ee12an  1372  ee23  1373  exlimdv  1646  spimfw  1656  ax12b  1701  hbald  1755  spOLD  1764  19.9ht  1792  19.23t  1818  hbimdOLD  1835  nfaldOLD  1872  19.21tOLD  1886  spimtOLD  1956  spimed  1960  cbv1hOLD  1975  cbv2h  1979  ax12olem1OLD  2011  ax12olem2OLD  2012  ax10  2025  ax10lem2OLD  2026  ax10lem4OLD  2030  ax10OLD  2032  a16gOLD  2049  ax11v2  2074  equviniOLD  2080  sb3  2088  hbsb2  2091  sbft  2103  sbftOLD  2104  dfsb2  2115  sbnOLD  2118  sbi1  2119  sbiedOLD  2124  sb9i  2169  sbal1  2202  aev-o  2258  ax11eq  2269  ax11el  2270  ax11indn  2271  ax11indi  2272  mo  2302  moexex  2349  2mo  2358  2eu1  2360  dvelimdc  2591  rsp2  2760  rgen2a  2764  mo2icl  3105  reu6  3115  reupick2  3619  pwpw0  3938  sssn  3949  pwsnALT  4002  dfiun2g  4115  disjiun  4194  axsep  4321  opth1  4426  copsexg  4434  opelopabt  4459  wefrc  4568  ordunidif  4621  oneqmini  4624  suctr  4656  ordsssuc2  4661  reusv3i  4721  reusv7OLD  4726  ralxfrALT  4733  elpwunsn  4748  dfwe2  4753  ssorduni  4757  ssonprc  4763  nlimsucg  4813  ordunisuc2  4815  tfinds  4830  ssnlim  4854  frinxp  4934  issref  5238  iotaval  5420  fun11iun  5686  fv3  5735  ndmfv  5746  ssimaex  5779  fvopab3ig  5794  iinpreima  5851  dff3  5873  dff4  5874  ffnfv  5885  fconstfv  5945  elunirnALT  5991  f1mpt  5998  isomin  6048  f1oweALT  6065  oprabid  6096  mpt2eq123  6124  f1o2ndf1  6445  frxp  6447  soxp  6450  brtpos  6479  rntpos  6483  dftpos4  6489  sorpsscmpl  6524  riotasvdOLD  6584  onfununi  6594  onnseq  6597  smores2  6607  smo11  6617  tfrlem1  6627  tfr3  6651  rdglim2  6681  tz7.48lem  6689  tz7.49  6693  seqomlem2  6699  abianfp  6707  oawordex  6791  oa00  6793  oaass  6795  om00  6809  odi  6813  omass  6814  oeordi  6821  oelim2  6829  omsmo  6888  eroveu  6990  eceqoveq  7000  map0g  7044  fundmen  7171  sdomdif  7246  onsdominel  7247  nneneq  7281  php3  7284  onomeneq  7287  pssnn  7318  f1finf1o  7326  findcard3  7341  unblem1  7350  fiint  7374  ixpfi2  7396  dffi2  7419  elfiun  7426  fisup2g  7460  wemaplem2  7505  preleq  7561  inf3lem2  7573  inf3lem3  7574  inf3lem6  7577  noinfep  7603  cantnfreslem  7620  epfrs  7656  tcmin  7669  r1sdom  7689  r1ord3g  7694  r1ord2  7696  tz9.12lem3  7704  rankelb  7739  bndrank  7756  rankunb  7765  rankuni2b  7768  cplem1  7802  karden  7808  carduni  7857  infxpenlem  7884  dfac8alem  7899  alephdom  7951  cardinfima  7967  alephval3  7980  dfac5lem4  7996  dfac5lem5  7997  dfac5  7998  dfac2  8000  kmlem13  8031  ackbij1b  8108  cfub  8118  coflim  8130  cflim2  8132  cfslbn  8136  cfslb2n  8137  cofsmo  8138  cfsmolem  8139  sornom  8146  fincssdom  8192  isf32lem1  8222  isf32lem2  8223  isf32lem9  8230  isf34lem4  8246  isfin1-3  8255  axcc4  8308  domtriomlem  8311  axdc2lem  8317  axdc3lem2  8320  zorn2lem4  8368  zorn2lem6  8370  zornn0g  8374  axdclem2  8389  uniimadom  8408  cardmin  8428  ficard  8429  konigthlem  8432  alephreg  8446  cfpwsdom  8448  axextnd  8455  fpwwe2lem6  8499  fpwwe2lem12  8505  fpwwe2lem13  8506  fpwwe2  8507  canthp1lem2  8517  winalim2  8560  tskuni  8647  grupr  8661  grur1a  8683  axgroth6  8692  grothomex  8693  eltskm  8707  addclpi  8758  nqereu  8795  ltexnq  8841  nsmallnq  8843  genpn0  8869  genpss  8870  genpnmax  8873  ltaddpr  8900  reclem3pr  8915  reclem4pr  8916  suplem1pr  8918  supsrlem  8975  1re  9079  addid1  9235  sup2  9953  supmullem1  9963  supmullem2  9964  infmrcl  9976  zmulcl  10313  zeo  10344  uzindOLD  10353  uz11  10497  uzwo  10528  uzwoOLD  10529  eqreznegel  10550  negn0  10551  lbzbi  10553  qextlt  10778  qextle  10779  xrsupsslem  10874  xrinfmsslem  10875  supxrun  10883  supxrpnf  10886  supxrunb1  10887  supxrunb2  10888  uzrdgfni  11286  hasheqf1oi  11623  leisorel  11697  rennim  12032  sqrlem6  12041  caubnd  12150  sqreulem  12151  rlimclim  12328  caucvgrlem  12454  sumeq2ii  12475  fsumcvg  12494  supcvg  12623  dvdslelem  12882  bitsinv1lem  12941  bitsshft  12975  smuval2  12982  smupvallem  12983  gcdcllem1  12999  bezoutlem2  13027  bezoutlem3  13028  algcvga  13058  isprm3  13076  isprm5  13100  vdwlem13  13349  vdwnnlem1  13351  vdwnnlem3  13353  ramub1lem1  13382  imasaddfnlem  13741  divsfval  13760  catpropd  13923  psdmrn  14627  odlem1  15161  gexlem1  15201  cygctb  15489  islss  15999  lspsneq0  16076  lspsneq  16182  mvrf1  16477  obselocv  16943  ppttop  17059  epttop  17061  elcls  17125  restntr  17234  cnprest  17341  regsep  17386  nrmsep3  17407  lmmo  17432  cmpsublem  17450  cmpsub  17451  hauscmplem  17457  bwth  17461  txcnpi  17628  txcnp  17640  tgqtop  17732  kqfvima  17750  fbun  17860  fbfinnfr  17861  trfbas2  17863  fgcl  17898  filssufilg  17931  ufinffr  17949  isfcls  18029  fclsrest  18044  flimfnfcls  18048  alexsubALTlem2  18067  alexsubALTlem3  18068  alexsubALTlem4  18069  alexsubALT  18070  cnextcn  18086  imasf1oxms  18507  metequiv2  18528  iccpnfcnv  18957  iccpnfhmeo  18958  iscau2  19218  caun0  19222  minveclem3b  19317  itg1climres  19594  mbfi1fseqlem4  19598  ellimc3  19754  limccnp2  19767  dvlip  19865  itgsubstlem  19920  evlseu  19925  mpfrcl  19927  elply2  20103  coefv0  20154  coemulc  20161  ulmss  20301  scvxcvx  20812  sqf11  20910  ppiublem1  20974  fsumvma  20985  ostth  21321  usgrafisinds  21415  nbgra0nb  21429  nbgraf1olem5  21443  cusgrafi  21479  spthispth  21561  wlkdvspthlem  21595  4cycl4dv  21642  exidu1  21902  rngoideu  21960  zerdivemp1  22010  nmcvcn  22179  chlimi  22725  ocsh  22773  shsvs  22813  h1datomi  23071  stcl  23707  stge0  23715  stle1  23716  stm1addi  23736  stm1add3i  23738  cvnsym  23781  mdbr2  23787  dmdbr2  23794  mdsl0  23801  mdsl1i  23812  mdsl2i  23813  cvmdi  23815  atexch  23872  atcvat4i  23888  cdj1i  23924  xrge0iifcnv  24307  esumpr2  24446  sigaclci  24503  cntmeas  24568  mbfmcnt  24606  ballotlemfc0  24738  ballotlemfcc  24739  iccllyscon  24925  ghomf1olem  25093  dedekindle  25176  prodeq2ii  25228  fprodcvg  25245  prodmo  25251  funpsstri  25376  fundmpss  25377  fprb  25384  dfon2lem3  25396  dfon2lem4  25397  dfon2lem6  25399  dfon2lem9  25402  dfon2  25403  hbimtg  25418  hbaltg  25419  dftrpred3g  25491  poseq  25508  soseq  25509  frrlem5b  25541  frrlem5d  25543  sltres  25573  nocvxminlem  25599  nocvxmin  25600  nofulllem5  25615  dfrdg4  25745  mptelee  25782  brbtwn2  25792  colinearalg  25797  axcontlem4  25854  btwntriv2  25894  btwncomim  25895  btwnswapid  25899  btwnexch3  25902  ifscgr  25926  lineunray  26029  hilbert1.2  26037  meran3  26111  arg-ax  26114  ontopbas  26126  onsuct0  26139  limsucncmpi  26143  ordcmp  26145  onint1  26147  supadd  26185  ismblfin  26193  cldbnd  26266  tailfb  26343  indexdom  26373  fzmul  26381  heibor1lem  26455  heibor  26467  zerdivemp1x  26508  ispridl2  26585  prtlem14  26660  prter2  26667  incssnn0  26702  fphpd  26814  rmxycomplete  26917  dford3lem1  27034  dvconstbi  27466  ax4567to6  27519  ax4567to7  27520  pm14.24  27547  sbiota1  27549  fnchoice  27614  stoweidlem62  27725  2reu1  27878  ffnafv  27949  lswrdn0  28149  shwrdssizelem1a  28165  usgra2adedgwlkon  28191  1to3vfriendship  28256  3cyclfrgrarn1  28260  n4cyclfrgra  28266  frgrancvvdeqlemB  28285  frg2wot1  28304  frg2woteq  28307  bi33imp12  28431  bi123imp0  28437  ee233  28457  vk15.4j  28467  ssralv2  28470  alrim3con13v  28472  tratrb  28475  3ax5  28476  onfrALTlem3  28485  onfrALTlem2  28487  19.41rg  28492  hbimpg  28496  hbalg  28497  a9e2ndeq  28501  e2  28586  ee223  28589  sspwtrALT  28789  sspwtrALT2  28790  suctrALT2  28803  trintALT  28847  isosctrlem1ALT  28901  bnj142  28947  bnj1379  29056  bnj607  29141  bnj908  29156  bnj938  29162  bnj1174  29226  bnj1280  29243  hbaldwAUX7  29302  nfaldwAUX7  29306  ax12olem2wAUX7  29310  ax10lem4NEW7  29325  ax10NEW7  29327  spimtNEW7  29361  cbv1hwAUX7  29365  cbv2hwAUX7  29367  equviniNEW7  29379  sbiedNEW7  29392  a16gNEW7  29398  hbsb2NEW7  29406  sbftNEW7  29408  sbnNEW7  29414  sbi1NEW7  29415  sbal1NEW7  29464  sb3NEW7  29486  dfsb2NEW7  29487  ax7w6AUX7  29501  hbaldOLD7  29523  nfaldOLD7  29529  ax12olem2OLD7  29545  cbv1hOLD7  29558  cbv2hOLD7  29560  sb9iOLD7  29597  lsatn0  29636  lsatcmp  29640  lsatcv0  29668  lfl1dim  29758  lfl1dim2N  29759  lkrss2N  29806  lub0N  29826  glbconxN  30014  hl2at  30041  cvrexchlem  30055  cvratlem  30057  cvrat4  30079  psubspi  30383  pointpsubN  30387  elpaddn0  30436  paddasslem17  30472  ispsubcl2N  30583  ldilval  30749  trlord  31205  diaelrnN  31682  cdlemm10N  31755  cdlemn11pre  31847  dihord2pre  31862  dihglblem2N  31931  dihglblem3N  31932  mapdrvallem2  32282
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator