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

Theorem syl6 29
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 10 . 2  |-  ( ps 
->  ( ch  ->  th )
)
41, 3sylcom 25 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl56  30  syl6com  31  a1dd  42  syl6mpi  58  syl6c  60  com34  77  con1d  116  expi  141  looinv  174  syl6ib  217  syl6ibr  218  syl6bi  219  syl6bir  220  jaoi  368  pm2.37  817  pm2.81  824  oplem1  930  3jao  1243  ee12an  1353  ee23  1354  exlimdv  1626  spimfw  1636  hbald  1726  sp  1728  hbimd  1733  nfald  1787  19.21t  1802  ax12olem1  1880  ax12olem2  1881  ax10lem2  1890  ax10lem4  1894  ax10  1897  a16g  1898  spimt  1927  cbv1h  1931  cbv2h  1933  equvini  1940  sbft  1978  sbied  1989  sb3  2005  dfsb2  2008  hbsb2  2010  sbn  2015  sbi1  2016  sb9i  2047  sbal1  2078  aev-o  2134  ax11eq  2145  ax11el  2146  ax11indn  2147  ax11indi  2148  mo  2178  moexex  2225  2mo  2234  2eu1  2236  dvelimdc  2452  rsp2  2618  rgen2a  2622  mo2icl  2957  reu6  2967  reupick2  3467  pwpw0  3779  sssn  3788  pwsnALT  3838  dfiun2g  3951  disjiun  4029  axsep  4156  opth1  4260  copsexg  4268  opelopabt  4293  wefrc  4403  ordunidif  4456  oneqmini  4459  suctr  4491  trsuc2OLD  4493  ordsssuc2  4497  reusv3i  4557  reusv7OLD  4562  ralxfrALT  4569  elpwunsn  4584  dfwe2  4589  ssorduni  4593  ssonprc  4599  nlimsucg  4649  ordunisuc2  4651  tfinds  4666  ssnlim  4690  frinxp  4771  issref  5072  iotaval  5246  fun11iun  5509  fv3  5557  ndmfv  5568  ssimaex  5600  fvopab3ig  5615  iinpreima  5671  dff3  5689  dff4  5690  ffnfv  5701  fconstfv  5750  elunirnALT  5795  f1mpt  5801  isomin  5850  f1oweALT  5867  oprabid  5898  mpt2eq123  5923  frxp  6241  soxp  6244  brtpos  6259  rntpos  6263  dftpos4  6269  sorpsscmpl  6304  riotasvdOLD  6364  onfununi  6374  onnseq  6377  smores2  6387  smo11  6397  tfrlem1  6407  tfr3  6431  rdglim2  6461  tz7.48lem  6469  tz7.49  6473  seqomlem2  6479  abianfp  6487  oawordex  6571  oa00  6573  oaass  6575  om00  6589  odi  6593  omass  6594  oeordi  6601  oelim2  6609  omsmo  6668  eroveu  6769  eceqoveq  6779  map0g  6823  fundmen  6950  sdomdif  7025  onsdominel  7026  nneneq  7060  php3  7063  onomeneq  7066  pssnn  7097  f1finf1o  7102  findcard3  7116  unblem1  7125  fiint  7149  ixpfi2  7170  dffi2  7192  elfiun  7199  fisup2g  7233  wemaplem2  7278  preleq  7334  inf3lem2  7346  inf3lem3  7347  inf3lem6  7350  noinfep  7376  cantnfreslem  7393  epfrs  7429  tcmin  7442  r1sdom  7462  r1ord3g  7467  r1ord2  7469  tz9.12lem3  7477  rankelb  7512  bndrank  7529  rankunb  7538  rankuni2b  7541  cplem1  7575  karden  7581  carduni  7630  infxpenlem  7657  dfac8alem  7672  alephdom  7724  cardinfima  7740  alephval3  7753  dfac5lem4  7769  dfac5lem5  7770  dfac5  7771  dfac2  7773  kmlem13  7804  ackbij1b  7881  cfub  7891  coflim  7903  cflim2  7905  cfslbn  7909  cfslb2n  7910  cofsmo  7911  cfsmolem  7912  sornom  7919  fincssdom  7965  isf32lem1  7995  isf32lem2  7996  isf32lem9  8003  isf34lem4  8019  isfin1-3  8028  axcc4  8081  domtriomlem  8084  axdc2lem  8090  axdc3lem2  8093  zorn2lem4  8142  zorn2lem6  8144  zornn0g  8148  axdclem2  8163  uniimadom  8182  cardmin  8202  ficard  8203  konigthlem  8206  alephreg  8220  cfpwsdom  8222  axextnd  8229  fpwwe2lem6  8273  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  canthp1lem2  8291  winalim2  8334  tskuni  8421  grupr  8435  grur1a  8457  axgroth6  8466  grothomex  8467  eltskm  8481  addclpi  8532  nqereu  8569  ltexnq  8615  nsmallnq  8617  genpn0  8643  genpss  8644  genpnmax  8647  ltaddpr  8674  reclem3pr  8689  reclem4pr  8690  suplem1pr  8692  supsrlem  8749  1re  8853  addid1  9008  lbinfm  9723  sup2  9726  supmullem1  9736  supmullem2  9737  infmrcl  9749  zmulcl  10082  zeo  10113  uzindOLD  10122  uz11  10266  uzwo  10297  uzwoOLD  10298  eqreznegel  10319  negn0  10320  lbzbi  10322  qextlt  10546  qextle  10547  xrsupsslem  10641  xrinfmsslem  10642  supxrun  10650  supxrpnf  10653  supxrunb1  10654  supxrunb2  10655  uzrdgfni  11037  leisorel  11414  rennim  11740  sqrlem6  11749  caubnd  11858  sqreulem  11859  rlimclim  12036  caucvgrlem  12161  sumeq2ii  12182  fsumcvg  12201  supcvg  12330  dvdslelem  12589  bitsinv1lem  12648  bitsshft  12682  smuval2  12689  smupvallem  12690  gcdcllem1  12706  bezoutlem2  12734  bezoutlem3  12735  algcvga  12765  isprm3  12783  isprm5  12807  vdwlem13  13056  vdwnnlem1  13058  vdwnnlem3  13060  ramub1lem1  13089  imasaddfnlem  13446  divsfval  13465  catpropd  13628  psdmrn  14332  odlem1  14866  gexlem1  14906  cygctb  15194  islss  15708  lspsneq0  15785  lspsneq  15891  mvrf1  16186  obselocv  16644  ppttop  16760  epttop  16762  elcls  16826  restntr  16928  cnprest  17033  regsep  17078  nrmsep3  17099  lmmo  17124  cmpsublem  17142  cmpsub  17143  hauscmplem  17149  txcnpi  17318  txcnp  17330  tgqtop  17419  kqfvima  17437  fbun  17551  fbfinnfr  17552  trfbas2  17554  fgcl  17589  filssufilg  17622  ufinffr  17640  isfcls  17720  fclsrest  17735  flimfnfcls  17739  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  imasf1oxms  18051  metequiv2  18072  iccpnfcnv  18458  iccpnfhmeo  18459  iscau2  18719  caun0  18723  minveclem3b  18808  itg1climres  19085  mbfi1fseqlem4  19089  ellimc3  19245  limccnp2  19258  dvlip  19356  itgsubstlem  19411  evlseu  19416  mpfrcl  19418  elply2  19594  coefv0  19645  coemulc  19652  ulmss  19790  scvxcvx  20296  sqf11  20393  ppiublem1  20457  fsumvma  20468  ostth  20804  exidu1  21009  rngoideu  21067  nmcvcn  21284  chlimi  21830  ocsh  21878  shsvs  21918  h1datomi  22176  stcl  22812  stge0  22820  stle1  22821  stm1addi  22841  stm1add3i  22843  cvnsym  22886  mdbr2  22892  dmdbr2  22899  mdsl0  22906  mdsl1i  22917  mdsl2i  22918  cvmdi  22920  atexch  22977  atcvat4i  22993  cdj1i  23029  ballotlemfc0  23067  ballotlemfcc  23068  iundifdifd  23175  xrge0iifcnv  23330  esumpr2  23454  sigaclci  23508  cntmeas  23568  mbfmcnt  23588  iccllyscon  23796  ghomf1olem  24016  dedekindle  24098  cprodeq2ii  24135  fprodcvg  24153  prodmo  24159  funpsstri  24192  fundmpss  24193  fprb  24200  dfon2lem3  24212  dfon2lem4  24213  dfon2lem6  24215  dfon2lem9  24218  dfon2  24219  hbimtg  24234  hbaltg  24235  dftrpred3g  24307  poseq  24324  soseq  24325  frrlem5b  24357  frrlem5d  24359  sltres  24389  nocvxminlem  24415  nocvxmin  24416  nofulllem5  24431  dfrdg4  24560  mptelee  24595  brbtwn2  24605  colinearalg  24610  axcontlem4  24667  btwntriv2  24707  btwncomim  24708  btwnswapid  24712  btwnexch3  24715  ifscgr  24739  lineunray  24842  hilbert1.2  24850  meran3  24924  arg-ax  24927  ontopbas  24939  onsuct0  24952  limsucncmpi  24956  ordcmp  24958  onint1  24960  supadd  24996  domrngref  25163  imrestr  25201  ab2rexex2g  25235  sssu  25244  mapmapmap  25251  cljo  25289  clme  25290  oriso  25317  mgmlion  25440  grpodivone  25476  imtr  25501  rltrran  25517  zerdivemp1  25539  intfmu2  25622  nsn  25633  osneisi  25634  intopcoaconlem3b  25641  intopcoaconb  25643  prcnt  25654  fgsb2  25658  cmptdst  25671  limptlimpr2lem2  25678  islimrs4  25685  bwt2  25695  iintlem1  25713  flfneicn  25728  lvsovso  25729  supexr  25734  claddrvr  25751  issubrv  25775  clsmulrv  25786  distmlva  25791  icccon2  25803  icccon4  25805  hdrmp  25809  cmpmorp  25882  ismonc  25917  isepic  25927  tartarmap  25991  fnctartar  26010  fnctartar2  26011  domcatfun  26028  codcatfun  26037  setiscat  26082  clscnc  26113  pgapspf2  26156  isconcl5a  26204  isconcl5ab  26205  isib2g1a1  26219  isibg1a2  26220  isibg2a  26221  isibg1a3a  26225  isibg1spa  26226  isibg1a5a  26227  bsstr  26231  nbssntr  26232  bsstrs  26249  cldbnd  26347  tailfb  26429  indexdom  26516  fzmul  26546  equivbnd  26617  heibor1lem  26636  heibor  26648  zerdivemp1x  26689  ispridl2  26766  prtlem14  26845  prter2  26852  incssnn0  26889  fphpd  27002  rmxycomplete  27105  dford3lem1  27222  dvconstbi  27654  ax4567to6  27707  ax4567to7  27708  pm14.24  27735  sbiota1  27737  fnchoice  27803  stoweidlem62  27914  2reu1  28067  ffnafv  28139  nbgra0nb  28278  spthispth  28359  wlkdvspthlem  28365  4cycl4dv  28413  1to3vfriendship  28432  3cyclfrgrarn1  28435  n4cyclfrgra  28440  bi33imp12  28554  ee233  28580  vk15.4j  28590  ssralv2  28593  alrim3con13v  28595  tratrb  28598  3ax5  28599  onfrALTlem3  28608  onfrALTlem2  28610  19.41rg  28615  hbimpg  28619  hbalg  28620  a9e2ndeq  28624  e2  28708  ee223  28711  sspwtrALT  28912  sspwtrALT2  28913  pwtrOLD  28915  pwtrrOLD  28917  suctrALT2  28929  trintALT  28973  bnj142  29070  bnj1379  29179  bnj607  29264  bnj908  29279  bnj938  29285  bnj1174  29349  bnj1280  29366  hbaldwAUX7  29425  nfaldwAUX7  29429  ax12olem2wAUX7  29433  ax10lem4NEW7  29448  ax10NEW7  29450  spimtNEW7  29484  cbv1hwAUX7  29488  cbv2hwAUX7  29490  equviniNEW7  29502  sbiedNEW7  29515  a16gNEW7  29521  hbsb2NEW7  29529  sbftNEW7  29531  sbnNEW7  29537  sbi1NEW7  29538  sbal1NEW7  29587  sb3NEW7  29608  dfsb2NEW7  29609  ax7w6AUX7  29622  hbaldOLD7  29638  nfaldOLD7  29644  ax12olem2OLD7  29660  cbv1hOLD7  29673  cbv2hOLD7  29675  sb9iOLD7  29712  a12stdy2-x12  29734  ax10lem18ALT  29746  a12stdy2  29749  a12study3  29757  a12study10  29758  a12study10n  29759  a12study11  29760  a12study11n  29761  ax9lem3  29764  ax9lem5  29766  ax9lem9  29770  ax9lem15  29776  lsatn0  29811  lsatcmp  29815  lsatcv0  29843  lfl1dim  29933  lfl1dim2N  29934  lkrss2N  29981  lub0N  30001  glbconxN  30189  hl2at  30216  cvrexchlem  30230  cvratlem  30232  cvrat4  30254  psubspi  30558  pointpsubN  30562  elpaddn0  30611  paddasslem17  30647  ispsubcl2N  30758  ldilval  30924  trlord  31380  diaelrnN  31857  cdlemm10N  31930  cdlemn11pre  32022  dihord2pre  32037  dihglblem2N  32106  dihglblem3N  32107  mapdrvallem2  32457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator