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  1703  hbald  1757  spOLD  1766  19.9ht  1794  19.23t  1820  hbimdOLD  1837  nfaldOLD  1874  19.21tOLD  1888  spimtOLD  1959  spimed  1963  cbv1hOLD  1978  cbv2h  1982  ax12olem1OLD  2014  ax12olem2OLD  2015  ax10  2028  ax10lem2OLD  2029  ax10lem4OLD  2033  ax10OLD  2035  a16gOLD  2052  ax11v2  2081  equviniOLD  2087  sb3  2096  hbsb2  2099  dfsb2  2112  sbft  2119  sbftOLD  2120  sbnOLD  2135  sbi1  2136  sbiedOLD  2157  sb9i  2176  sbal1  2209  aev-o  2265  ax11eq  2276  ax11el  2277  ax11indn  2278  ax11indi  2279  mo  2309  moexex  2356  2mo  2365  2eu1  2367  dvelimdc  2598  rsp2  2774  rgen2a  2778  mo2icl  3119  reu6  3129  reupick2  3612  pwpw0  3970  sssn  3981  pwsnALT  4034  dfiun2g  4147  disjiun  4227  axsep  4354  opth1  4463  copsexg  4471  opelopabt  4496  wefrc  4605  ordunidif  4658  oneqmini  4661  suctrALT  4693  ordsssuc2  4699  reusv3i  4759  reusv7OLD  4764  ralxfrALT  4771  elpwunsn  4786  dfwe2  4791  ssorduni  4795  ssonprc  4801  nlimsucg  4851  ordunisuc2  4853  tfinds  4868  ssnlim  4892  frinxp  4972  issref  5276  iotaval  5458  fun11iun  5724  fv3  5773  ndmfv  5784  ssimaex  5817  fvopab3ig  5832  iinpreima  5889  dff3  5911  dff4  5912  ffnfv  5923  fconstfv  5983  elunirnALT  6029  f1mpt  6036  isomin  6086  f1oweALT  6103  oprabid  6134  mpt2eq123  6162  f1o2ndf1  6483  frxp  6485  soxp  6488  brtpos  6517  rntpos  6521  dftpos4  6527  sorpsscmpl  6562  riotasvdOLD  6622  onfununi  6632  onnseq  6635  smores2  6645  smo11  6655  tfrlem1  6665  tfr3  6689  rdglim2  6719  tz7.48lem  6727  tz7.49  6731  seqomlem2  6737  abianfp  6745  oawordex  6829  oa00  6831  oaass  6833  om00  6847  odi  6851  omass  6852  oeordi  6859  oelim2  6867  omsmo  6926  eroveu  7028  eceqoveq  7038  map0g  7082  fundmen  7209  sdomdif  7284  onsdominel  7285  nneneq  7319  php3  7322  onomeneq  7325  pssnn  7356  f1finf1o  7364  findcard3  7379  unblem1  7388  fiint  7412  ixpfi2  7434  dffi2  7457  elfiun  7464  fisup2g  7500  wemaplem2  7545  preleq  7601  inf3lem2  7613  inf3lem3  7614  inf3lem6  7617  noinfep  7643  cantnfreslem  7660  epfrs  7696  tcmin  7709  r1sdom  7729  r1ord3g  7734  r1ord2  7736  tz9.12lem3  7744  rankelb  7779  bndrank  7796  rankunb  7805  rankuni2b  7808  cplem1  7844  karden  7850  carduni  7899  infxpenlem  7926  dfac8alem  7941  alephdom  7993  cardinfima  8009  alephval3  8022  dfac5lem4  8038  dfac5lem5  8039  dfac5  8040  dfac2  8042  kmlem13  8073  ackbij1b  8150  cfub  8160  coflim  8172  cflim2  8174  cfslbn  8178  cfslb2n  8179  cofsmo  8180  cfsmolem  8181  sornom  8188  fincssdom  8234  isf32lem1  8264  isf32lem2  8265  isf32lem9  8272  isf34lem4  8288  isfin1-3  8297  axcc4  8350  domtriomlem  8353  axdc2lem  8359  axdc3lem2  8362  zorn2lem4  8410  zorn2lem6  8412  zornn0g  8416  axdclem2  8431  uniimadom  8450  cardmin  8470  ficard  8471  konigthlem  8474  alephreg  8488  cfpwsdom  8490  axextnd  8497  fpwwe2lem6  8541  fpwwe2lem12  8547  fpwwe2lem13  8548  fpwwe2  8549  canthp1lem2  8559  winalim2  8602  tskuni  8689  grupr  8703  grur1a  8725  axgroth6  8734  grothomex  8735  eltskm  8749  addclpi  8800  nqereu  8837  ltexnq  8883  nsmallnq  8885  genpn0  8911  genpss  8912  genpnmax  8915  ltaddpr  8942  reclem3pr  8957  reclem4pr  8958  suplem1pr  8960  supsrlem  9017  1re  9121  addid1  9277  sup2  9995  supmullem1  10005  supmullem2  10006  infmrcl  10018  zmulcl  10355  zeo  10386  uzindOLD  10395  uz11  10539  uzwo  10570  uzwoOLD  10571  eqreznegel  10592  negn0  10593  lbzbi  10595  qextlt  10820  qextle  10821  xrsupsslem  10916  xrinfmsslem  10917  supxrun  10925  supxrpnf  10928  supxrunb1  10929  supxrunb2  10930  uzrdgfni  11329  hasheqf1oi  11666  leisorel  11740  rennim  12075  sqrlem6  12084  caubnd  12193  sqreulem  12194  rlimclim  12371  caucvgrlem  12497  sumeq2ii  12518  fsumcvg  12537  supcvg  12666  dvdslelem  12925  bitsinv1lem  12984  bitsshft  13018  smuval2  13025  smupvallem  13026  gcdcllem1  13042  bezoutlem2  13070  bezoutlem3  13071  algcvga  13101  isprm3  13119  isprm5  13143  vdwlem13  13392  vdwnnlem1  13394  vdwnnlem3  13396  ramub1lem1  13425  imasaddfnlem  13784  divsfval  13803  catpropd  13966  psdmrn  14670  odlem1  15204  gexlem1  15244  cygctb  15532  islss  16042  lspsneq0  16119  lspsneq  16225  mvrf1  16520  obselocv  16986  ppttop  17102  epttop  17104  elcls  17168  restntr  17277  cnprest  17384  regsep  17429  nrmsep3  17450  lmmo  17475  cmpsublem  17493  cmpsub  17494  hauscmplem  17500  bwth  17504  txcnpi  17671  txcnp  17683  tgqtop  17775  kqfvima  17793  fbun  17903  fbfinnfr  17904  trfbas2  17906  fgcl  17941  filssufilg  17974  ufinffr  17992  isfcls  18072  fclsrest  18087  flimfnfcls  18091  alexsubALTlem2  18110  alexsubALTlem3  18111  alexsubALTlem4  18112  alexsubALT  18113  cnextcn  18129  imasf1oxms  18550  metequiv2  18571  iccpnfcnv  19000  iccpnfhmeo  19001  iscau2  19261  caun0  19265  minveclem3b  19360  itg1climres  19635  mbfi1fseqlem4  19639  ellimc3  19797  limccnp2  19810  dvlip  19908  itgsubstlem  19963  evlseu  19968  mpfrcl  19970  elply2  20146  coefv0  20197  coemulc  20204  ulmss  20344  scvxcvx  20855  sqf11  20953  ppiublem1  21017  fsumvma  21028  ostth  21364  usgrafisinds  21458  nbgra0nb  21472  nbgraf1olem5  21486  cusgrafi  21522  spthispth  21604  wlkdvspthlem  21638  4cycl4dv  21685  exidu1  21945  rngoideu  22003  zerdivemp1  22053  nmcvcn  22222  chlimi  22768  ocsh  22816  shsvs  22856  h1datomi  23114  stcl  23750  stge0  23758  stle1  23759  stm1addi  23779  stm1add3i  23781  cvnsym  23824  mdbr2  23830  dmdbr2  23837  mdsl0  23844  mdsl1i  23855  mdsl2i  23856  cvmdi  23858  atexch  23915  atcvat4i  23931  cdj1i  23967  xrge0iifcnv  24350  esumpr2  24489  sigaclci  24546  cntmeas  24611  mbfmcnt  24649  ballotlemfc0  24781  ballotlemfcc  24782  iccllyscon  24968  ghomf1olem  25136  dedekindle  25219  prodeq2ii  25270  fprodcvg  25287  prodmo  25293  funpsstri  25420  fundmpss  25421  fprb  25428  dfon2lem3  25443  dfon2lem4  25444  dfon2lem6  25446  dfon2lem9  25449  dfon2  25450  hbimtg  25465  hbaltg  25466  dftrpred3g  25542  poseq  25559  soseq  25560  frrlem5b  25618  frrlem5d  25620  sltres  25650  nocvxminlem  25676  nocvxmin  25677  nofulllem5  25692  dfrdg4  25826  mptelee  25865  brbtwn2  25875  colinearalg  25880  axcontlem4  25937  btwntriv2  25977  btwncomim  25978  btwnswapid  25982  btwnexch3  25985  ifscgr  26009  lineunray  26112  hilbert1.2  26120  meran3  26194  arg-ax  26197  ontopbas  26209  onsuct0  26222  limsucncmpi  26226  ordcmp  26228  onint1  26230  supadd  26270  ismblfin  26283  cldbnd  26367  tailfb  26444  indexdom  26474  fzmul  26482  heibor1lem  26556  heibor  26568  zerdivemp1x  26609  ispridl2  26686  prtlem14  26761  prter2  26768  incssnn0  26803  fphpd  26915  rmxycomplete  27018  dford3lem1  27135  dvconstbi  27566  ax4567to6  27619  ax4567to7  27620  pm14.24  27647  sbiota1  27649  fnchoice  27714  stoweidlem62  27825  2reu1  27978  ffnafv  28049  wrdsymb0  28226  swrdccatin2d  28279  2cshw2lem3  28312  lswrdn0  28318  cshwssizelem1a  28337  usgra2adedgwlkon  28379  nbhashuvtx1  28455  1to3vfriendship  28496  3cyclfrgrarn1  28500  n4cyclfrgra  28506  frgrancvvdeqlemB  28525  frg2wot1  28544  frg2woteq  28547  bi33imp12  28671  bi123imp0  28677  ee233  28700  vk15.4j  28710  ssralv2  28713  alrim3con13v  28715  tratrb  28718  3ax5  28719  onfrALTlem3  28728  onfrALTlem2  28730  19.41rg  28735  hbimpg  28739  hbalg  28740  a9e2ndeq  28744  e2  28830  ee223  28833  sspwtrALT  29033  sspwtrALT2  29034  suctrALT2  29047  trintALT  29091  isosctrlem1ALT  29144  bnj142  29191  bnj1379  29300  bnj607  29385  bnj908  29400  bnj938  29406  bnj1174  29470  bnj1280  29487  hbaldwAUX7  29546  nfaldwAUX7  29550  ax12olem2wAUX7  29554  ax10lem4NEW7  29569  ax10NEW7  29571  spimtNEW7  29605  cbv1hwAUX7  29609  cbv2hwAUX7  29611  equviniNEW7  29625  sbiedNEW7  29638  a16gNEW7  29644  hbsb2NEW7  29652  sbftNEW7  29654  sbnNEW7  29660  sbi1NEW7  29661  sb8dwAUX7  29688  sbal1NEW7  29713  sb3NEW7  29735  dfsb2NEW7  29736  ax7w6AUX7  29750  hbaldOLD7  29782  nfaldOLD7  29788  ax12olem2OLD7  29804  cbv1hOLD7  29817  cbv2hOLD7  29819  sb9iOLD7  29856  lsatn0  29895  lsatcmp  29899  lsatcv0  29927  lfl1dim  30017  lfl1dim2N  30018  lkrss2N  30065  lub0N  30085  glbconxN  30273  hl2at  30300  cvrexchlem  30314  cvratlem  30316  cvrat4  30338  psubspi  30642  pointpsubN  30646  elpaddn0  30695  paddasslem17  30731  ispsubcl2N  30842  ldilval  31008  trlord  31464  diaelrnN  31941  cdlemm10N  32014  cdlemn11pre  32106  dihord2pre  32121  dihglblem2N  32190  dihglblem3N  32191  mapdrvallem2  32541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator