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

Theorem syl6 32
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 28 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl56  33  syl6com  34  a1dd  45  syl6mpi  61  syl6c  63  com34  80  con1d  119  expi  144  looinv  176  syl6ib  219  syl6ibr  220  syl6bi  221  syl6bir  222  jaoi  370  pm2.37  819  pm2.81  826  oplem1  932  3jao  1246  ee12an  1373  ee23  1374  exlimdv  1647  spimfw  1657  ax12b  1702  hbald  1756  spOLD  1765  19.9ht  1793  19.23t  1819  hbimdOLD  1836  nfaldOLD  1873  19.21tOLD  1887  spimtOLD  1957  spimed  1961  cbv1hOLD  1976  cbv2h  1980  ax12olem1OLD  2012  ax12olem2OLD  2013  ax10  2026  ax10lem2OLD  2027  ax10lem4OLD  2031  ax10OLD  2033  a16gOLD  2050  ax11v2  2079  equviniOLD  2085  sb3  2094  hbsb2  2097  dfsb2  2110  sbft  2117  sbftOLD  2118  sbnOLD  2133  sbi1  2134  sbiedOLD  2153  sb9i  2172  sbal1  2205  aev-o  2261  ax11eq  2272  ax11el  2273  ax11indn  2274  ax11indi  2275  mo  2305  moexex  2352  2mo  2361  2eu1  2363  dvelimdc  2594  rsp2  2770  rgen2a  2774  mo2icl  3115  reu6  3125  reupick2  3629  pwpw0  3948  sssn  3959  pwsnALT  4012  dfiun2g  4125  disjiun  4204  axsep  4331  opth1  4436  copsexg  4444  opelopabt  4469  wefrc  4578  ordunidif  4631  oneqmini  4634  suctrALT  4666  ordsssuc2  4672  reusv3i  4732  reusv7OLD  4737  ralxfrALT  4744  elpwunsn  4759  dfwe2  4764  ssorduni  4768  ssonprc  4774  nlimsucg  4824  ordunisuc2  4826  tfinds  4841  ssnlim  4865  frinxp  4945  issref  5249  iotaval  5431  fun11iun  5697  fv3  5746  ndmfv  5757  ssimaex  5790  fvopab3ig  5805  iinpreima  5862  dff3  5884  dff4  5885  ffnfv  5896  fconstfv  5956  elunirnALT  6002  f1mpt  6009  isomin  6059  f1oweALT  6076  oprabid  6107  mpt2eq123  6135  f1o2ndf1  6456  frxp  6458  soxp  6461  brtpos  6490  rntpos  6494  dftpos4  6500  sorpsscmpl  6535  riotasvdOLD  6595  onfununi  6605  onnseq  6608  smores2  6618  smo11  6628  tfrlem1  6638  tfr3  6662  rdglim2  6692  tz7.48lem  6700  tz7.49  6704  seqomlem2  6710  abianfp  6718  oawordex  6802  oa00  6804  oaass  6806  om00  6820  odi  6824  omass  6825  oeordi  6832  oelim2  6840  omsmo  6899  eroveu  7001  eceqoveq  7011  map0g  7055  fundmen  7182  sdomdif  7257  onsdominel  7258  nneneq  7292  php3  7295  onomeneq  7298  pssnn  7329  f1finf1o  7337  findcard3  7352  unblem1  7361  fiint  7385  ixpfi2  7407  dffi2  7430  elfiun  7437  fisup2g  7473  wemaplem2  7518  preleq  7574  inf3lem2  7586  inf3lem3  7587  inf3lem6  7590  noinfep  7616  cantnfreslem  7633  epfrs  7669  tcmin  7682  r1sdom  7702  r1ord3g  7707  r1ord2  7709  tz9.12lem3  7717  rankelb  7752  bndrank  7769  rankunb  7778  rankuni2b  7781  cplem1  7815  karden  7821  carduni  7870  infxpenlem  7897  dfac8alem  7912  alephdom  7964  cardinfima  7980  alephval3  7993  dfac5lem4  8009  dfac5lem5  8010  dfac5  8011  dfac2  8013  kmlem13  8044  ackbij1b  8121  cfub  8131  coflim  8143  cflim2  8145  cfslbn  8149  cfslb2n  8150  cofsmo  8151  cfsmolem  8152  sornom  8159  fincssdom  8205  isf32lem1  8235  isf32lem2  8236  isf32lem9  8243  isf34lem4  8259  isfin1-3  8268  axcc4  8321  domtriomlem  8324  axdc2lem  8330  axdc3lem2  8333  zorn2lem4  8381  zorn2lem6  8383  zornn0g  8387  axdclem2  8402  uniimadom  8421  cardmin  8441  ficard  8442  konigthlem  8445  alephreg  8459  cfpwsdom  8461  axextnd  8468  fpwwe2lem6  8512  fpwwe2lem12  8518  fpwwe2lem13  8519  fpwwe2  8520  canthp1lem2  8530  winalim2  8573  tskuni  8660  grupr  8674  grur1a  8696  axgroth6  8705  grothomex  8706  eltskm  8720  addclpi  8771  nqereu  8808  ltexnq  8854  nsmallnq  8856  genpn0  8882  genpss  8883  genpnmax  8886  ltaddpr  8913  reclem3pr  8928  reclem4pr  8929  suplem1pr  8931  supsrlem  8988  1re  9092  addid1  9248  sup2  9966  supmullem1  9976  supmullem2  9977  infmrcl  9989  zmulcl  10326  zeo  10357  uzindOLD  10366  uz11  10510  uzwo  10541  uzwoOLD  10542  eqreznegel  10563  negn0  10564  lbzbi  10566  qextlt  10791  qextle  10792  xrsupsslem  10887  xrinfmsslem  10888  supxrun  10896  supxrpnf  10899  supxrunb1  10900  supxrunb2  10901  uzrdgfni  11300  hasheqf1oi  11637  leisorel  11711  rennim  12046  sqrlem6  12055  caubnd  12164  sqreulem  12165  rlimclim  12342  caucvgrlem  12468  sumeq2ii  12489  fsumcvg  12508  supcvg  12637  dvdslelem  12896  bitsinv1lem  12955  bitsshft  12989  smuval2  12996  smupvallem  12997  gcdcllem1  13013  bezoutlem2  13041  bezoutlem3  13042  algcvga  13072  isprm3  13090  isprm5  13114  vdwlem13  13363  vdwnnlem1  13365  vdwnnlem3  13367  ramub1lem1  13396  imasaddfnlem  13755  divsfval  13774  catpropd  13937  psdmrn  14641  odlem1  15175  gexlem1  15215  cygctb  15503  islss  16013  lspsneq0  16090  lspsneq  16196  mvrf1  16491  obselocv  16957  ppttop  17073  epttop  17075  elcls  17139  restntr  17248  cnprest  17355  regsep  17400  nrmsep3  17421  lmmo  17446  cmpsublem  17464  cmpsub  17465  hauscmplem  17471  bwth  17475  txcnpi  17642  txcnp  17654  tgqtop  17746  kqfvima  17764  fbun  17874  fbfinnfr  17875  trfbas2  17877  fgcl  17912  filssufilg  17945  ufinffr  17963  isfcls  18043  fclsrest  18058  flimfnfcls  18062  alexsubALTlem2  18081  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  cnextcn  18100  imasf1oxms  18521  metequiv2  18542  iccpnfcnv  18971  iccpnfhmeo  18972  iscau2  19232  caun0  19236  minveclem3b  19331  itg1climres  19608  mbfi1fseqlem4  19612  ellimc3  19768  limccnp2  19781  dvlip  19879  itgsubstlem  19934  evlseu  19939  mpfrcl  19941  elply2  20117  coefv0  20168  coemulc  20175  ulmss  20315  scvxcvx  20826  sqf11  20924  ppiublem1  20988  fsumvma  20999  ostth  21335  usgrafisinds  21429  nbgra0nb  21443  nbgraf1olem5  21457  cusgrafi  21493  spthispth  21575  wlkdvspthlem  21609  4cycl4dv  21656  exidu1  21916  rngoideu  21974  zerdivemp1  22024  nmcvcn  22193  chlimi  22739  ocsh  22787  shsvs  22827  h1datomi  23085  stcl  23721  stge0  23729  stle1  23730  stm1addi  23750  stm1add3i  23752  cvnsym  23795  mdbr2  23801  dmdbr2  23808  mdsl0  23815  mdsl1i  23826  mdsl2i  23827  cvmdi  23829  atexch  23886  atcvat4i  23902  cdj1i  23938  xrge0iifcnv  24321  esumpr2  24460  sigaclci  24517  cntmeas  24582  mbfmcnt  24620  ballotlemfc0  24752  ballotlemfcc  24753  iccllyscon  24939  ghomf1olem  25107  dedekindle  25190  prodeq2ii  25241  fprodcvg  25258  prodmo  25264  funpsstri  25391  fundmpss  25392  fprb  25399  dfon2lem3  25414  dfon2lem4  25415  dfon2lem6  25417  dfon2lem9  25420  dfon2  25421  hbimtg  25436  hbaltg  25437  dftrpred3g  25513  poseq  25530  soseq  25531  frrlem5b  25589  frrlem5d  25591  sltres  25621  nocvxminlem  25647  nocvxmin  25648  nofulllem5  25663  dfrdg4  25797  mptelee  25836  brbtwn2  25846  colinearalg  25851  axcontlem4  25908  btwntriv2  25948  btwncomim  25949  btwnswapid  25953  btwnexch3  25956  ifscgr  25980  lineunray  26083  hilbert1.2  26091  meran3  26165  arg-ax  26168  ontopbas  26180  onsuct0  26193  limsucncmpi  26197  ordcmp  26199  onint1  26201  supadd  26240  ismblfin  26249  cldbnd  26331  tailfb  26408  indexdom  26438  fzmul  26446  heibor1lem  26520  heibor  26532  zerdivemp1x  26573  ispridl2  26650  prtlem14  26725  prter2  26732  incssnn0  26767  fphpd  26879  rmxycomplete  26982  dford3lem1  27099  dvconstbi  27530  ax4567to6  27583  ax4567to7  27584  pm14.24  27611  sbiota1  27613  fnchoice  27678  stoweidlem62  27789  2reu1  27942  ffnafv  28013  wrdsymb0  28190  swrdccatin2d  28243  2cshw2lem3  28276  lswrdn0  28282  cshwssizelem1a  28301  usgra2adedgwlkon  28343  nbhashuvtx1  28419  1to3vfriendship  28460  3cyclfrgrarn1  28464  n4cyclfrgra  28470  frgrancvvdeqlemB  28489  frg2wot1  28508  frg2woteq  28511  bi33imp12  28635  bi123imp0  28641  ee233  28664  vk15.4j  28674  ssralv2  28677  alrim3con13v  28679  tratrb  28682  3ax5  28683  onfrALTlem3  28692  onfrALTlem2  28694  19.41rg  28699  hbimpg  28703  hbalg  28704  a9e2ndeq  28708  e2  28794  ee223  28797  sspwtrALT  28997  sspwtrALT2  28998  suctrALT2  29011  trintALT  29055  isosctrlem1ALT  29108  bnj142  29155  bnj1379  29264  bnj607  29349  bnj908  29364  bnj938  29370  bnj1174  29434  bnj1280  29451  hbaldwAUX7  29510  nfaldwAUX7  29514  ax12olem2wAUX7  29518  ax10lem4NEW7  29533  ax10NEW7  29535  spimtNEW7  29569  cbv1hwAUX7  29573  cbv2hwAUX7  29575  equviniNEW7  29589  sbiedNEW7  29602  a16gNEW7  29608  hbsb2NEW7  29616  sbftNEW7  29618  sbnNEW7  29624  sbi1NEW7  29625  sb8dwAUX7  29652  sbal1NEW7  29677  sb3NEW7  29699  dfsb2NEW7  29700  ax7w6AUX7  29714  hbaldOLD7  29746  nfaldOLD7  29752  ax12olem2OLD7  29768  cbv1hOLD7  29781  cbv2hOLD7  29783  sb9iOLD7  29820  lsatn0  29859  lsatcmp  29863  lsatcv0  29891  lfl1dim  29981  lfl1dim2N  29982  lkrss2N  30029  lub0N  30049  glbconxN  30237  hl2at  30264  cvrexchlem  30278  cvratlem  30280  cvrat4  30302  psubspi  30606  pointpsubN  30610  elpaddn0  30659  paddasslem17  30695  ispsubcl2N  30806  ldilval  30972  trlord  31428  diaelrnN  31905  cdlemm10N  31978  cdlemn11pre  32070  dihord2pre  32085  dihglblem2N  32154  dihglblem3N  32155  mapdrvallem2  32505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator