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  hbald  1747  spOLD  1756  19.23t  1808  hbimdOLD  1825  nfaldOLD  1865  19.21tOLD  1875  ax12olem1OLD  1957  ax12olem2OLD  1958  ax10lem2  1968  ax10lem4  1974  ax10  1977  a16g  1978  spimt  2001  cbv1h  2005  cbv2h  2007  equvini  2014  sbft  2052  sbied  2063  sb3  2079  dfsb2  2082  hbsb2  2084  sbn  2089  sbi1  2090  sb9i  2121  sbal1  2154  aev-o  2210  ax11eq  2221  ax11el  2222  ax11indn  2223  ax11indi  2224  mo  2254  moexex  2301  2mo  2310  2eu1  2312  dvelimdc  2537  rsp2  2705  rgen2a  2709  mo2icl  3050  reu6  3060  reupick2  3564  pwpw0  3883  sssn  3894  pwsnALT  3946  dfiun2g  4059  disjiun  4137  axsep  4264  opth1  4369  copsexg  4377  opelopabt  4402  wefrc  4511  ordunidif  4564  oneqmini  4567  suctr  4599  ordsssuc2  4604  reusv3i  4664  reusv7OLD  4669  ralxfrALT  4676  elpwunsn  4691  dfwe2  4696  ssorduni  4700  ssonprc  4706  nlimsucg  4756  ordunisuc2  4758  tfinds  4773  ssnlim  4797  frinxp  4877  issref  5181  iotaval  5363  fun11iun  5629  fv3  5678  ndmfv  5689  ssimaex  5721  fvopab3ig  5736  iinpreima  5793  dff3  5815  dff4  5816  ffnfv  5827  fconstfv  5887  elunirnALT  5933  f1mpt  5940  isomin  5990  f1oweALT  6007  oprabid  6038  mpt2eq123  6066  frxp  6386  soxp  6389  brtpos  6418  rntpos  6422  dftpos4  6428  sorpsscmpl  6463  riotasvdOLD  6523  onfununi  6533  onnseq  6536  smores2  6546  smo11  6556  tfrlem1  6566  tfr3  6590  rdglim2  6620  tz7.48lem  6628  tz7.49  6632  seqomlem2  6638  abianfp  6646  oawordex  6730  oa00  6732  oaass  6734  om00  6748  odi  6752  omass  6753  oeordi  6760  oelim2  6768  omsmo  6827  eroveu  6929  eceqoveq  6939  map0g  6983  fundmen  7110  sdomdif  7185  onsdominel  7186  nneneq  7220  php3  7223  onomeneq  7226  pssnn  7257  f1finf1o  7265  findcard3  7280  unblem1  7289  fiint  7313  ixpfi2  7334  dffi2  7357  elfiun  7364  fisup2g  7398  wemaplem2  7443  preleq  7499  inf3lem2  7511  inf3lem3  7512  inf3lem6  7515  noinfep  7541  cantnfreslem  7558  epfrs  7594  tcmin  7607  r1sdom  7627  r1ord3g  7632  r1ord2  7634  tz9.12lem3  7642  rankelb  7677  bndrank  7694  rankunb  7703  rankuni2b  7706  cplem1  7740  karden  7746  carduni  7795  infxpenlem  7822  dfac8alem  7837  alephdom  7889  cardinfima  7905  alephval3  7918  dfac5lem4  7934  dfac5lem5  7935  dfac5  7936  dfac2  7938  kmlem13  7969  ackbij1b  8046  cfub  8056  coflim  8068  cflim2  8070  cfslbn  8074  cfslb2n  8075  cofsmo  8076  cfsmolem  8077  sornom  8084  fincssdom  8130  isf32lem1  8160  isf32lem2  8161  isf32lem9  8168  isf34lem4  8184  isfin1-3  8193  axcc4  8246  domtriomlem  8249  axdc2lem  8255  axdc3lem2  8258  zorn2lem4  8306  zorn2lem6  8308  zornn0g  8312  axdclem2  8327  uniimadom  8346  cardmin  8366  ficard  8367  konigthlem  8370  alephreg  8384  cfpwsdom  8386  axextnd  8393  fpwwe2lem6  8437  fpwwe2lem12  8443  fpwwe2lem13  8444  fpwwe2  8445  canthp1lem2  8455  winalim2  8498  tskuni  8585  grupr  8599  grur1a  8621  axgroth6  8630  grothomex  8631  eltskm  8645  addclpi  8696  nqereu  8733  ltexnq  8779  nsmallnq  8781  genpn0  8807  genpss  8808  genpnmax  8811  ltaddpr  8838  reclem3pr  8853  reclem4pr  8854  suplem1pr  8856  supsrlem  8913  1re  9017  addid1  9172  sup2  9890  supmullem1  9900  supmullem2  9901  infmrcl  9913  zmulcl  10250  zeo  10281  uzindOLD  10290  uz11  10434  uzwo  10465  uzwoOLD  10466  eqreznegel  10487  negn0  10488  lbzbi  10490  qextlt  10715  qextle  10716  xrsupsslem  10811  xrinfmsslem  10812  supxrun  10820  supxrpnf  10823  supxrunb1  10824  supxrunb2  10825  uzrdgfni  11219  hasheqf1oi  11556  leisorel  11630  rennim  11965  sqrlem6  11974  caubnd  12083  sqreulem  12084  rlimclim  12261  caucvgrlem  12387  sumeq2ii  12408  fsumcvg  12427  supcvg  12556  dvdslelem  12815  bitsinv1lem  12874  bitsshft  12908  smuval2  12915  smupvallem  12916  gcdcllem1  12932  bezoutlem2  12960  bezoutlem3  12961  algcvga  12991  isprm3  13009  isprm5  13033  vdwlem13  13282  vdwnnlem1  13284  vdwnnlem3  13286  ramub1lem1  13315  imasaddfnlem  13674  divsfval  13693  catpropd  13856  psdmrn  14560  odlem1  15094  gexlem1  15134  cygctb  15422  islss  15932  lspsneq0  16009  lspsneq  16115  mvrf1  16410  obselocv  16872  ppttop  16988  epttop  16990  elcls  17054  restntr  17162  cnprest  17269  regsep  17314  nrmsep3  17335  lmmo  17360  cmpsublem  17378  cmpsub  17379  hauscmplem  17385  txcnpi  17555  txcnp  17567  tgqtop  17659  kqfvima  17677  fbun  17787  fbfinnfr  17788  trfbas2  17790  fgcl  17825  filssufilg  17858  ufinffr  17876  isfcls  17956  fclsrest  17971  flimfnfcls  17975  alexsubALTlem2  17994  alexsubALTlem3  17995  alexsubALTlem4  17996  alexsubALT  17997  cnextcn  18013  imasf1oxms  18403  metequiv2  18424  iccpnfcnv  18834  iccpnfhmeo  18835  iscau2  19095  caun0  19099  minveclem3b  19190  itg1climres  19467  mbfi1fseqlem4  19471  ellimc3  19627  limccnp2  19640  dvlip  19738  itgsubstlem  19793  evlseu  19798  mpfrcl  19800  elply2  19976  coefv0  20027  coemulc  20034  ulmss  20174  scvxcvx  20685  sqf11  20783  ppiublem1  20847  fsumvma  20858  ostth  21194  usgrafisinds  21287  nbgra0nb  21301  nbgraf1olem5  21315  cusgrafi  21351  spthispth  21421  wlkdvspthlem  21449  4cycl4dv  21496  exidu1  21756  rngoideu  21814  zerdivemp1  21864  nmcvcn  22033  chlimi  22579  ocsh  22627  shsvs  22667  h1datomi  22925  stcl  23561  stge0  23569  stle1  23570  stm1addi  23590  stm1add3i  23592  cvnsym  23635  mdbr2  23641  dmdbr2  23648  mdsl0  23655  mdsl1i  23666  mdsl2i  23667  cvmdi  23669  atexch  23726  atcvat4i  23742  cdj1i  23778  xrge0iifcnv  24117  esumpr2  24248  sigaclci  24305  cntmeas  24368  mbfmcnt  24406  ballotlemfc0  24523  ballotlemfcc  24524  iccllyscon  24710  ghomf1olem  24878  dedekindle  24961  prodeq2ii  25012  fprodcvg  25029  prodmo  25035  funpsstri  25139  fundmpss  25140  fprb  25147  dfon2lem3  25159  dfon2lem4  25160  dfon2lem6  25162  dfon2lem9  25165  dfon2  25166  hbimtg  25181  hbaltg  25182  dftrpred3g  25254  poseq  25271  soseq  25272  frrlem5b  25304  frrlem5d  25306  sltres  25336  nocvxminlem  25362  nocvxmin  25363  nofulllem5  25378  dfrdg4  25507  mptelee  25542  brbtwn2  25552  colinearalg  25557  axcontlem4  25614  btwntriv2  25654  btwncomim  25655  btwnswapid  25659  btwnexch3  25662  ifscgr  25686  lineunray  25789  hilbert1.2  25797  meran3  25871  arg-ax  25874  ontopbas  25886  onsuct0  25899  limsucncmpi  25903  ordcmp  25905  onint1  25907  supadd  25942  cldbnd  26014  tailfb  26091  indexdom  26121  fzmul  26129  heibor1lem  26203  heibor  26215  zerdivemp1x  26256  ispridl2  26333  prtlem14  26408  prter2  26415  incssnn0  26450  fphpd  26562  rmxycomplete  26665  dford3lem1  26782  dvconstbi  27214  ax4567to6  27267  ax4567to7  27268  pm14.24  27295  sbiota1  27297  fnchoice  27362  stoweidlem62  27473  2reu1  27626  ffnafv  27698  1to3vfriendship  27755  3cyclfrgrarn1  27759  n4cyclfrgra  27765  frgrancvvdeqlemB  27784  bi33imp12  27913  bi123imp0  27919  ee233  27939  vk15.4j  27949  ssralv2  27952  alrim3con13v  27954  tratrb  27957  3ax5  27958  onfrALTlem3  27967  onfrALTlem2  27969  19.41rg  27974  hbimpg  27978  hbalg  27979  a9e2ndeq  27983  e2  28067  ee223  28070  sspwtrALT  28270  sspwtrALT2  28271  suctrALT2  28284  trintALT  28328  bnj142  28425  bnj1379  28534  bnj607  28619  bnj908  28634  bnj938  28640  bnj1174  28704  bnj1280  28721  hbaldwAUX7  28780  nfaldwAUX7  28784  ax12olem2wAUX7  28788  ax10lem4NEW7  28803  ax10NEW7  28805  spimtNEW7  28839  cbv1hwAUX7  28843  cbv2hwAUX7  28845  equviniNEW7  28857  sbiedNEW7  28870  a16gNEW7  28876  hbsb2NEW7  28884  sbftNEW7  28886  sbnNEW7  28892  sbi1NEW7  28893  sbal1NEW7  28942  sb3NEW7  28964  dfsb2NEW7  28965  ax7w6AUX7  28978  hbaldOLD7  28994  nfaldOLD7  29000  ax12olem2OLD7  29016  cbv1hOLD7  29029  cbv2hOLD7  29031  sb9iOLD7  29068  a12stdy2-x12  29089  ax10lem18ALT  29101  a12stdy2  29104  a12study3  29112  a12study10  29113  a12study10n  29114  a12study11  29115  a12study11n  29116  ax9lem3  29119  ax9lem5  29121  ax9lem9  29125  ax9lem15  29131  lsatn0  29166  lsatcmp  29170  lsatcv0  29198  lfl1dim  29288  lfl1dim2N  29289  lkrss2N  29336  lub0N  29356  glbconxN  29544  hl2at  29571  cvrexchlem  29585  cvratlem  29587  cvrat4  29609  psubspi  29913  pointpsubN  29917  elpaddn0  29966  paddasslem17  30002  ispsubcl2N  30113  ldilval  30279  trlord  30735  diaelrnN  31212  cdlemm10N  31285  cdlemn11pre  31377  dihord2pre  31392  dihglblem2N  31461  dihglblem3N  31462  mapdrvallem2  31812
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator