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  1369  ee23  1370  exlimdv  1643  spimfw  1653  ax12b  1697  hbald  1751  spOLD  1760  19.9ht  1788  19.23t  1814  hbimdOLD  1831  nfaldOLD  1868  19.21tOLD  1882  spimtOLD  1954  spimed  1958  ax12olem1OLD  1977  ax12olem2OLD  1978  ax10  1991  ax10lem2OLD  1992  ax10lem4OLD  1996  ax10OLD  1998  a16gOLD  2013  cbv1h  2031  cbv2h  2033  equviniOLD  2041  sbft  2074  sbied  2085  sb3  2101  dfsb2  2104  hbsb2  2106  sbn  2111  sbi1  2112  sb9i  2143  sbal1  2176  aev-o  2232  ax11eq  2243  ax11el  2244  ax11indn  2245  ax11indi  2246  mo  2276  moexex  2323  2mo  2332  2eu1  2334  dvelimdc  2560  rsp2  2728  rgen2a  2732  mo2icl  3073  reu6  3083  reupick2  3587  pwpw0  3906  sssn  3917  pwsnALT  3970  dfiun2g  4083  disjiun  4162  axsep  4289  opth1  4394  copsexg  4402  opelopabt  4427  wefrc  4536  ordunidif  4589  oneqmini  4592  suctr  4624  ordsssuc2  4629  reusv3i  4689  reusv7OLD  4694  ralxfrALT  4701  elpwunsn  4716  dfwe2  4721  ssorduni  4725  ssonprc  4731  nlimsucg  4781  ordunisuc2  4783  tfinds  4798  ssnlim  4822  frinxp  4902  issref  5206  iotaval  5388  fun11iun  5654  fv3  5703  ndmfv  5714  ssimaex  5747  fvopab3ig  5762  iinpreima  5819  dff3  5841  dff4  5842  ffnfv  5853  fconstfv  5913  elunirnALT  5959  f1mpt  5966  isomin  6016  f1oweALT  6033  oprabid  6064  mpt2eq123  6092  f1o2ndf1  6413  frxp  6415  soxp  6418  brtpos  6447  rntpos  6451  dftpos4  6457  sorpsscmpl  6492  riotasvdOLD  6552  onfununi  6562  onnseq  6565  smores2  6575  smo11  6585  tfrlem1  6595  tfr3  6619  rdglim2  6649  tz7.48lem  6657  tz7.49  6661  seqomlem2  6667  abianfp  6675  oawordex  6759  oa00  6761  oaass  6763  om00  6777  odi  6781  omass  6782  oeordi  6789  oelim2  6797  omsmo  6856  eroveu  6958  eceqoveq  6968  map0g  7012  fundmen  7139  sdomdif  7214  onsdominel  7215  nneneq  7249  php3  7252  onomeneq  7255  pssnn  7286  f1finf1o  7294  findcard3  7309  unblem1  7318  fiint  7342  ixpfi2  7363  dffi2  7386  elfiun  7393  fisup2g  7427  wemaplem2  7472  preleq  7528  inf3lem2  7540  inf3lem3  7541  inf3lem6  7544  noinfep  7570  cantnfreslem  7587  epfrs  7623  tcmin  7636  r1sdom  7656  r1ord3g  7661  r1ord2  7663  tz9.12lem3  7671  rankelb  7706  bndrank  7723  rankunb  7732  rankuni2b  7735  cplem1  7769  karden  7775  carduni  7824  infxpenlem  7851  dfac8alem  7866  alephdom  7918  cardinfima  7934  alephval3  7947  dfac5lem4  7963  dfac5lem5  7964  dfac5  7965  dfac2  7967  kmlem13  7998  ackbij1b  8075  cfub  8085  coflim  8097  cflim2  8099  cfslbn  8103  cfslb2n  8104  cofsmo  8105  cfsmolem  8106  sornom  8113  fincssdom  8159  isf32lem1  8189  isf32lem2  8190  isf32lem9  8197  isf34lem4  8213  isfin1-3  8222  axcc4  8275  domtriomlem  8278  axdc2lem  8284  axdc3lem2  8287  zorn2lem4  8335  zorn2lem6  8337  zornn0g  8341  axdclem2  8356  uniimadom  8375  cardmin  8395  ficard  8396  konigthlem  8399  alephreg  8413  cfpwsdom  8415  axextnd  8422  fpwwe2lem6  8466  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  canthp1lem2  8484  winalim2  8527  tskuni  8614  grupr  8628  grur1a  8650  axgroth6  8659  grothomex  8660  eltskm  8674  addclpi  8725  nqereu  8762  ltexnq  8808  nsmallnq  8810  genpn0  8836  genpss  8837  genpnmax  8840  ltaddpr  8867  reclem3pr  8882  reclem4pr  8883  suplem1pr  8885  supsrlem  8942  1re  9046  addid1  9202  sup2  9920  supmullem1  9930  supmullem2  9931  infmrcl  9943  zmulcl  10280  zeo  10311  uzindOLD  10320  uz11  10464  uzwo  10495  uzwoOLD  10496  eqreznegel  10517  negn0  10518  lbzbi  10520  qextlt  10745  qextle  10746  xrsupsslem  10841  xrinfmsslem  10842  supxrun  10850  supxrpnf  10853  supxrunb1  10854  supxrunb2  10855  uzrdgfni  11253  hasheqf1oi  11590  leisorel  11664  rennim  11999  sqrlem6  12008  caubnd  12117  sqreulem  12118  rlimclim  12295  caucvgrlem  12421  sumeq2ii  12442  fsumcvg  12461  supcvg  12590  dvdslelem  12849  bitsinv1lem  12908  bitsshft  12942  smuval2  12949  smupvallem  12950  gcdcllem1  12966  bezoutlem2  12994  bezoutlem3  12995  algcvga  13025  isprm3  13043  isprm5  13067  vdwlem13  13316  vdwnnlem1  13318  vdwnnlem3  13320  ramub1lem1  13349  imasaddfnlem  13708  divsfval  13727  catpropd  13890  psdmrn  14594  odlem1  15128  gexlem1  15168  cygctb  15456  islss  15966  lspsneq0  16043  lspsneq  16149  mvrf1  16444  obselocv  16910  ppttop  17026  epttop  17028  elcls  17092  restntr  17200  cnprest  17307  regsep  17352  nrmsep3  17373  lmmo  17398  cmpsublem  17416  cmpsub  17417  hauscmplem  17423  txcnpi  17593  txcnp  17605  tgqtop  17697  kqfvima  17715  fbun  17825  fbfinnfr  17826  trfbas2  17828  fgcl  17863  filssufilg  17896  ufinffr  17914  isfcls  17994  fclsrest  18009  flimfnfcls  18013  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  cnextcn  18051  imasf1oxms  18472  metequiv2  18493  iccpnfcnv  18922  iccpnfhmeo  18923  iscau2  19183  caun0  19187  minveclem3b  19282  itg1climres  19559  mbfi1fseqlem4  19563  ellimc3  19719  limccnp2  19732  dvlip  19830  itgsubstlem  19885  evlseu  19890  mpfrcl  19892  elply2  20068  coefv0  20119  coemulc  20126  ulmss  20266  scvxcvx  20777  sqf11  20875  ppiublem1  20939  fsumvma  20950  ostth  21286  usgrafisinds  21380  nbgra0nb  21394  nbgraf1olem5  21408  cusgrafi  21444  spthispth  21526  wlkdvspthlem  21560  4cycl4dv  21607  exidu1  21867  rngoideu  21925  zerdivemp1  21975  nmcvcn  22144  chlimi  22690  ocsh  22738  shsvs  22778  h1datomi  23036  stcl  23672  stge0  23680  stle1  23681  stm1addi  23701  stm1add3i  23703  cvnsym  23746  mdbr2  23752  dmdbr2  23759  mdsl0  23766  mdsl1i  23777  mdsl2i  23778  cvmdi  23780  atexch  23837  atcvat4i  23853  cdj1i  23889  xrge0iifcnv  24272  esumpr2  24411  sigaclci  24468  cntmeas  24533  mbfmcnt  24571  ballotlemfc0  24703  ballotlemfcc  24704  iccllyscon  24890  ghomf1olem  25058  dedekindle  25141  prodeq2ii  25192  fprodcvg  25209  prodmo  25215  funpsstri  25335  fundmpss  25336  fprb  25343  dfon2lem3  25355  dfon2lem4  25356  dfon2lem6  25358  dfon2lem9  25361  dfon2  25362  hbimtg  25377  hbaltg  25378  dftrpred3g  25450  poseq  25467  soseq  25468  frrlem5b  25500  frrlem5d  25502  sltres  25532  nocvxminlem  25558  nocvxmin  25559  nofulllem5  25574  dfrdg4  25703  mptelee  25738  brbtwn2  25748  colinearalg  25753  axcontlem4  25810  btwntriv2  25850  btwncomim  25851  btwnswapid  25855  btwnexch3  25858  ifscgr  25882  lineunray  25985  hilbert1.2  25993  meran3  26067  arg-ax  26070  ontopbas  26082  onsuct0  26095  limsucncmpi  26099  ordcmp  26101  onint1  26103  supadd  26138  ismblfin  26146  cldbnd  26219  tailfb  26296  indexdom  26326  fzmul  26334  heibor1lem  26408  heibor  26420  zerdivemp1x  26461  ispridl2  26538  prtlem14  26613  prter2  26620  incssnn0  26655  fphpd  26767  rmxycomplete  26870  dford3lem1  26987  dvconstbi  27419  ax4567to6  27472  ax4567to7  27473  pm14.24  27500  sbiota1  27502  fnchoice  27567  stoweidlem62  27678  2reu1  27831  ffnafv  27902  usgra2adedgwlkon  28047  1to3vfriendship  28112  3cyclfrgrarn1  28116  n4cyclfrgra  28122  frgrancvvdeqlemB  28141  frg2wot1  28160  frg2woteq  28163  bi33imp12  28287  bi123imp0  28293  ee233  28313  vk15.4j  28323  ssralv2  28326  alrim3con13v  28328  tratrb  28331  3ax5  28332  onfrALTlem3  28341  onfrALTlem2  28343  19.41rg  28348  hbimpg  28352  hbalg  28353  a9e2ndeq  28357  e2  28441  ee223  28444  sspwtrALT  28644  sspwtrALT2  28645  suctrALT2  28658  trintALT  28702  bnj142  28799  bnj1379  28908  bnj607  28993  bnj908  29008  bnj938  29014  bnj1174  29078  bnj1280  29095  hbaldwAUX7  29154  nfaldwAUX7  29158  ax12olem2wAUX7  29162  ax10lem4NEW7  29177  ax10NEW7  29179  spimtNEW7  29213  cbv1hwAUX7  29217  cbv2hwAUX7  29219  equviniNEW7  29231  sbiedNEW7  29244  a16gNEW7  29250  hbsb2NEW7  29258  sbftNEW7  29260  sbnNEW7  29266  sbi1NEW7  29267  sbal1NEW7  29316  sb3NEW7  29338  dfsb2NEW7  29339  ax7w6AUX7  29352  hbaldOLD7  29368  nfaldOLD7  29374  ax12olem2OLD7  29390  cbv1hOLD7  29403  cbv2hOLD7  29405  sb9iOLD7  29442  lsatn0  29482  lsatcmp  29486  lsatcv0  29514  lfl1dim  29604  lfl1dim2N  29605  lkrss2N  29652  lub0N  29672  glbconxN  29860  hl2at  29887  cvrexchlem  29901  cvratlem  29903  cvrat4  29925  psubspi  30229  pointpsubN  30233  elpaddn0  30282  paddasslem17  30318  ispsubcl2N  30429  ldilval  30595  trlord  31051  diaelrnN  31528  cdlemm10N  31601  cdlemn11pre  31693  dihord2pre  31708  dihglblem2N  31777  dihglblem3N  31778  mapdrvallem2  32128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator