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  spimfw  1627  hbald  1714  sp  1716  hbimd  1721  nfald  1775  19.21t  1790  ax12olem1  1868  ax12olem2  1869  ax10lem2  1877  ax10lem4  1881  ax10  1884  a16g  1885  spimt  1914  cbv1h  1918  cbv2h  1920  equvini  1927  sbft  1965  sbied  1976  sb3  1992  dfsb2  1995  hbsb2  1997  sbn  2002  sbi1  2003  sb9i  2034  sbal1  2065  aev-o  2121  ax11eq  2132  ax11el  2133  ax11indn  2134  ax11indi  2135  mo  2165  moexex  2212  2mo  2221  2eu1  2223  dvelimdc  2439  rsp2  2605  rgen2a  2609  mo2icl  2944  reu6  2954  reupick2  3454  pwpw0  3763  sssn  3772  pwsnALT  3822  dfiun2g  3935  disjiun  4013  axsep  4140  opth1  4244  copsexg  4252  opelopabt  4277  wefrc  4387  ordunidif  4440  oneqmini  4443  suctr  4475  trsuc2OLD  4477  ordsssuc2  4481  reusv3i  4541  reusv7OLD  4546  ralxfrALT  4553  elpwunsn  4568  dfwe2  4573  ssorduni  4577  ssonprc  4583  nlimsucg  4633  ordunisuc2  4635  tfinds  4650  ssnlim  4674  frinxp  4755  issref  5056  iotaval  5230  fun11iun  5493  fv3  5541  ndmfv  5552  ssimaex  5584  fvopab3ig  5599  iinpreima  5655  dff3  5673  dff4  5674  ffnfv  5685  fconstfv  5734  elunirnALT  5779  f1mpt  5785  isomin  5834  f1oweALT  5851  oprabid  5882  mpt2eq123  5907  frxp  6225  soxp  6228  brtpos  6243  rntpos  6247  dftpos4  6253  sorpsscmpl  6288  riotasvdOLD  6348  onfununi  6358  onnseq  6361  smores2  6371  smo11  6381  tfrlem1  6391  tfr3  6415  rdglim2  6445  tz7.48lem  6453  tz7.49  6457  seqomlem2  6463  abianfp  6471  oawordex  6555  oa00  6557  oaass  6559  om00  6573  odi  6577  omass  6578  oeordi  6585  oelim2  6593  omsmo  6652  eroveu  6753  eceqoveq  6763  map0g  6807  fundmen  6934  sdomdif  7009  onsdominel  7010  nneneq  7044  php3  7047  onomeneq  7050  pssnn  7081  f1finf1o  7086  findcard3  7100  unblem1  7109  fiint  7133  ixpfi2  7154  dffi2  7176  elfiun  7183  fisup2g  7217  wemaplem2  7262  preleq  7318  inf3lem2  7330  inf3lem3  7331  inf3lem6  7334  noinfep  7360  cantnfreslem  7377  epfrs  7413  tcmin  7426  r1sdom  7446  r1ord3g  7451  r1ord2  7453  tz9.12lem3  7461  rankelb  7496  bndrank  7513  rankunb  7522  rankuni2b  7525  cplem1  7559  karden  7565  carduni  7614  infxpenlem  7641  dfac8alem  7656  alephdom  7708  cardinfima  7724  alephval3  7737  dfac5lem4  7753  dfac5lem5  7754  dfac5  7755  dfac2  7757  kmlem13  7788  ackbij1b  7865  cfub  7875  coflim  7887  cflim2  7889  cfslbn  7893  cfslb2n  7894  cofsmo  7895  cfsmolem  7896  sornom  7903  fincssdom  7949  isf32lem1  7979  isf32lem2  7980  isf32lem9  7987  isf34lem4  8003  isfin1-3  8012  axcc4  8065  domtriomlem  8068  axdc2lem  8074  axdc3lem2  8077  zorn2lem4  8126  zorn2lem6  8128  zornn0g  8132  axdclem2  8147  uniimadom  8166  cardmin  8186  ficard  8187  konigthlem  8190  alephreg  8204  cfpwsdom  8206  axextnd  8213  fpwwe2lem6  8257  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  canthp1lem2  8275  winalim2  8318  tskuni  8405  grupr  8419  grur1a  8441  axgroth6  8450  grothomex  8451  eltskm  8465  addclpi  8516  nqereu  8553  ltexnq  8599  nsmallnq  8601  genpn0  8627  genpss  8628  genpnmax  8631  ltaddpr  8658  reclem3pr  8673  reclem4pr  8674  suplem1pr  8676  supsrlem  8733  1re  8837  addid1  8992  lbinfm  9707  sup2  9710  supmullem1  9720  supmullem2  9721  infmrcl  9733  zmulcl  10066  zeo  10097  uzindOLD  10106  uz11  10250  uzwo  10281  uzwoOLD  10282  eqreznegel  10303  negn0  10304  lbzbi  10306  qextlt  10530  qextle  10531  xrsupsslem  10625  xrinfmsslem  10626  supxrun  10634  supxrpnf  10637  supxrunb1  10638  supxrunb2  10639  uzrdgfni  11021  leisorel  11398  rennim  11724  sqrlem6  11733  caubnd  11842  sqreulem  11843  rlimclim  12020  caucvgrlem  12145  sumeq2ii  12166  fsumcvg  12185  supcvg  12314  dvdslelem  12573  bitsinv1lem  12632  bitsshft  12666  smuval2  12673  smupvallem  12674  gcdcllem1  12690  bezoutlem2  12718  bezoutlem3  12719  algcvga  12749  isprm3  12767  isprm5  12791  vdwlem13  13040  vdwnnlem1  13042  vdwnnlem3  13044  ramub1lem1  13073  imasaddfnlem  13430  divsfval  13449  catpropd  13612  psdmrn  14316  odlem1  14850  gexlem1  14890  cygctb  15178  islss  15692  lspsneq0  15769  lspsneq  15875  mvrf1  16170  obselocv  16628  ppttop  16744  epttop  16746  elcls  16810  restntr  16912  cnprest  17017  regsep  17062  nrmsep3  17083  lmmo  17108  cmpsublem  17126  cmpsub  17127  hauscmplem  17133  txcnpi  17302  txcnp  17314  tgqtop  17403  kqfvima  17421  fbun  17535  fbfinnfr  17536  trfbas2  17538  fgcl  17573  filssufilg  17606  ufinffr  17624  isfcls  17704  fclsrest  17719  flimfnfcls  17723  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  imasf1oxms  18035  metequiv2  18056  iccpnfcnv  18442  iccpnfhmeo  18443  iscau2  18703  caun0  18707  minveclem3b  18792  itg1climres  19069  mbfi1fseqlem4  19073  ellimc3  19229  limccnp2  19242  dvlip  19340  itgsubstlem  19395  evlseu  19400  mpfrcl  19402  elply2  19578  coefv0  19629  coemulc  19636  ulmss  19774  scvxcvx  20280  sqf11  20377  ppiublem1  20441  fsumvma  20452  ostth  20788  exidu1  20993  rngoideu  21051  nmcvcn  21268  chlimi  21814  ocsh  21862  shsvs  21902  h1datomi  22160  stcl  22796  stge0  22804  stle1  22805  stm1addi  22825  stm1add3i  22827  cvnsym  22870  mdbr2  22876  dmdbr2  22883  mdsl0  22890  mdsl1i  22901  mdsl2i  22902  cvmdi  22904  atexch  22961  atcvat4i  22977  cdj1i  23013  ballotlemfc0  23051  ballotlemfcc  23052  iundifdifd  23159  xrge0iifcnv  23315  esumpr2  23439  sigaclci  23493  cntmeas  23553  mbfmcnt  23573  iccllyscon  23781  ghomf1olem  24001  dedekindle  24083  funpsstri  24121  fundmpss  24122  fprb  24129  dfon2lem3  24141  dfon2lem4  24142  dfon2lem6  24144  dfon2lem9  24147  dfon2  24148  hbimtg  24163  hbaltg  24164  dftrpred3g  24236  poseq  24253  soseq  24254  frrlem5b  24286  frrlem5d  24288  sltres  24318  nocvxminlem  24344  nocvxmin  24345  nofulllem5  24360  dfrdg4  24488  mptelee  24523  brbtwn2  24533  colinearalg  24538  axcontlem4  24595  btwntriv2  24635  btwncomim  24636  btwnswapid  24640  btwnexch3  24643  ifscgr  24667  lineunray  24770  hilbert1.2  24778  meran3  24852  arg-ax  24855  ontopbas  24867  onsuct0  24880  limsucncmpi  24884  ordcmp  24886  onint1  24888  domrngref  25060  imrestr  25098  ab2rexex2g  25132  sssu  25141  mapmapmap  25148  cljo  25186  clme  25187  oriso  25214  mgmlion  25337  grpodivone  25373  imtr  25398  rltrran  25414  zerdivemp1  25436  intfmu2  25519  nsn  25530  osneisi  25531  intopcoaconlem3b  25538  intopcoaconb  25540  prcnt  25551  fgsb2  25555  cmptdst  25568  limptlimpr2lem2  25575  islimrs4  25582  bwt2  25592  iintlem1  25610  flfneicn  25625  lvsovso  25626  supexr  25631  claddrvr  25648  issubrv  25672  clsmulrv  25683  distmlva  25688  icccon2  25700  icccon4  25702  hdrmp  25706  cmpmorp  25779  ismonc  25814  isepic  25824  tartarmap  25888  fnctartar  25907  fnctartar2  25908  domcatfun  25925  codcatfun  25934  setiscat  25979  clscnc  26010  pgapspf2  26053  isconcl5a  26101  isconcl5ab  26102  isib2g1a1  26116  isibg1a2  26117  isibg2a  26118  isibg1a3a  26122  isibg1spa  26123  isibg1a5a  26124  bsstr  26128  nbssntr  26129  bsstrs  26146  cldbnd  26244  tailfb  26326  indexdom  26413  fzmul  26443  equivbnd  26514  heibor1lem  26533  heibor  26545  zerdivemp1x  26586  ispridl2  26663  prtlem14  26742  prter2  26749  incssnn0  26786  fphpd  26899  rmxycomplete  27002  dford3lem1  27119  dvconstbi  27551  ax4567to6  27604  ax4567to7  27605  pm14.24  27632  sbiota1  27634  fnchoice  27700  stoweidlem62  27811  2reu1  27964  ffnafv  28033  nbgra0nb  28144  1to3vfriendship  28186  ee233  28281  vk15.4j  28291  ssralv2  28294  alrim3con13v  28296  tratrb  28299  3ax5  28300  onfrALTlem3  28309  onfrALTlem2  28311  19.41rg  28316  hbimpg  28320  hbalg  28321  a9e2ndeq  28325  e2  28403  ee223  28406  sspwtrALT  28596  sspwtrALT2  28597  pwtrOLD  28599  pwtrrOLD  28601  suctrALT2  28613  trintALT  28657  bnj142  28754  bnj1379  28863  bnj607  28948  bnj908  28963  bnj938  28969  bnj1174  29033  bnj1280  29050  a12stdy2-x12  29112  ax10lem18ALT  29124  a12stdy2  29127  a12study3  29135  a12study10  29136  a12study10n  29137  a12study11  29138  a12study11n  29139  ax9lem3  29142  ax9lem5  29144  ax9lem9  29148  ax9lem15  29154  lsatn0  29189  lsatcmp  29193  lsatcv0  29221  lfl1dim  29311  lfl1dim2N  29312  lkrss2N  29359  lub0N  29379  glbconxN  29567  hl2at  29594  cvrexchlem  29608  cvratlem  29610  cvrat4  29632  psubspi  29936  pointpsubN  29940  elpaddn0  29989  paddasslem17  30025  ispsubcl2N  30136  ldilval  30302  trlord  30758  diaelrnN  31235  cdlemm10N  31308  cdlemn11pre  31400  dihord2pre  31415  dihglblem2N  31484  dihglblem3N  31485  mapdrvallem2  31835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator