Theorem syl6 35

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Jan-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

Step	Hyp	Ref	Expression
1		syl6.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl6.2	. . 3 |- ( ch -> th )
3	2	a1i 11	. 2 |- ( ps -> ( ch -> th ) )
4	1, 3	sylcom 30	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl56  36  syl6com  37  a1dd  50  syl6mpi  67  syl6c  70  syl10  79  com34  91  con1d  139  expi  161  looinv  194  syl6ib  241  syl6ibr  242  syl6bi  243  syl6bir  244  jaoi  394  syl6an  568  pm2.37  889  pm2.81  896  oplem1  1007  3jao  1389  al2im  1742  nfimdOLDOLD  1824  exlimdv  1861  spimfw  1878  ax13b  1964  nf5-1  2023  hbald  2041  19.9d  2070  19.9ht  2143  spimed  2255  cbv2h  2269  axc15  2303  ax12  2304  axc11n  2307  axc11nOLD  2308  axc11nOLDOLD  2309  axc11nALT  2310  ax12v2OLD  2342  equvini  2346  hbsb2  2359  dfsb2  2373  sbequi  2375  sbft  2379  sbi1  2392  mo3  2507  mopick  2535  moexex  2541  dvelimdc  2786  necon1ad  2811  necon4bd  2814  rsp2  2936  mo2icl  3385  reuss2  3907  reupick2  3913  elpwunsn  4224  pwpw0  4344  sssn  4358  pwsnALT  4429  dfiun2g  4552  disjiun  4640  axsep  4780  reusv1  4866  reusv3i  4875  ralxfrALT  4887  opth1  4944  copsexg  4956  opelopabt  4987  wefrc  5108  frinxp  5184  ssrelrn  5315  issref  5509  ordunidif  5773  oneqmini  5776  suctr  5808  suctrOLD  5809  ordsssuc2  5814  fv3  6206  ndmfv  6218  ssimaex  6263  fvopab3ig  6278  iinpreima  6345  fvcofneq  6367  dff3  6372  dff4  6373  ffnfv  6388  fnsnb  6432  elunirn  6509  f1mpt  6518  isomin  6587  oprabid  6677  mpt2eq123  6714  sorpsscmpl  6948  dfwe2  6981  ssorduni  6985  ssonprc  6992  nlimsucg  7042  ordunisuc2  7044  tfinds  7059  ssnlim  7083  fun11iun  7126  f1oweALT  7152  el2mpt2cl  7251  f1o2ndf1  7285  frxp  7287  soxp  7290  brtpos  7361  rntpos  7365  dftpos4  7371  onfununi  7438  onnseq  7441  smores2  7451  smo11  7461  tfr3  7495  rdglim2  7528  tz7.48lem  7536  tz7.49  7540  seqomlem2  7546  oawordex  7637  oa00  7639  oaass  7641  om00  7655  odi  7659  omass  7660  oeordi  7667  oelim2  7675  omsmo  7734  eroveu  7842  eceqoveq  7853  map0g  7897  fundmen  8030  sdomdif  8108  onsdominel  8109  nneneq  8143  php3  8146  onomeneq  8150  pssnn  8178  f1finf1o  8187  findcard3  8203  unblem1  8212  fiint  8237  ixpfi2  8264  dffi2  8329  elfiun  8336  fisup2g  8374  fiinf2g  8406  wemaplem2  8452  preleq  8514  inf3lem2  8526  inf3lem3  8527  inf3lem6  8530  noinfep  8557  epfrs  8607  tcmin  8617  r1sdom  8637  r1ord3g  8642  r1ord2  8644  tz9.12lem3  8652  rankelb  8687  bndrank  8704  rankunb  8713  rankuni2b  8716  cplem1  8752  karden  8758  carduni  8807  infxpenlem  8836  dfac8alem  8852  alephdom  8904  cardinfima  8920  alephval3  8933  dfac5lem4  8949  dfac5lem5  8950  dfac5  8951  dfac2  8953  kmlem13  8984  ackbij1b  9061  cfub  9071  coflim  9083  cflim2  9085  cfslbn  9089  cfslb2n  9090  cofsmo  9091  cfsmolem  9092  sornom  9099  fincssdom  9145  isf32lem1  9175  isf32lem2  9176  isf32lem9  9183  isf34lem4  9199  isfin1-3  9208  axcc4  9261  domtriomlem  9264  axdc2lem  9270  axdc3lem2  9273  zorn2lem4  9321  zorn2lem6  9323  zornn0g  9327  axdclem2  9342  uniimadom  9366  cardmin  9386  ficard  9387  konigthlem  9390  alephreg  9404  cfpwsdom  9406  axextnd  9413  fpwwe2lem6  9457  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  canthp1lem2  9475  winalim2  9518  tskuni  9605  grupr  9619  grur1a  9641  axgroth6  9650  grothomex  9651  eltskm  9665  addclpi  9714  nqereu  9751  ltexnq  9797  nsmallnq  9799  genpn0  9825  genpss  9826  genpnmax  9829  ltaddpr  9856  reclem3pr  9871  reclem4pr  9872  suplem1pr  9874  supsrlem  9932  1re  10039  dedekindle  10201  addid1  10216  negn0  10459  negf1o  10460  negfi  10971  fiminre  10972  sup2  10979  supadd  10991  supmullem1  10993  supmullem2  10994  zmulcl  11426  zeo  11463  uz11  11710  uzwo  11751  eqreznegel  11774  lbzbi  11776  qextlt  12034  qextle  12035  xrsupsslem  12137  xrinfmsslem  12138  supxrun  12146  supxrpnf  12148  supxrunb1  12149  supxrunb2  12150  fzm1  12420  uzrdgfni  12757  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashreshashfun  13226  leisorel  13244  fundmge2nop0  13274  wrdsymb0  13339  swrdccatin2d  13500  cshinj  13557  repswcshw  13558  rennim  13979  sqrlem6  13988  caubnd  14098  sqreulem  14099  rlimclim  14277  caucvgrlem  14403  fsumcvg  14443  supcvg  14588  prodeq2ii  14643  fprodcvg  14660  prodmo  14666  dvdslelem  15031  bitsinv1lem  15163  bitsshft  15197  smuval2  15204  smupvallem  15205  gcdcllem1  15221  bezoutlem2  15257  bezoutlem3  15258  algcvga  15292  isprm3  15396  isprm5  15419  oddprmdvds  15607  vdwlem13  15697  vdwnnlem1  15699  vdwnnlem3  15701  ramub1lem1  15730  prmgaplem5  15759  imasaddfnlem  16188  divsfval  16207  catpropd  16369  joindmss  17007  meetdmss  17021  psdmrn  17207  odlem1  17954  gexlem1  17994  cygctb  18293  lmodfopnelem1  18899  islss  18935  lspsneq0  19012  lspsneq  19122  mvrf1  19425  evlseu  19516  mpfrcl  19518  psgnodpmr  19936  obselocv  20072  ppttop  20811  epttop  20813  elcls  20877  restntr  20986  cnprest  21093  regsep  21138  nrmsep3  21159  lmmo  21184  cmpsublem  21202  cmpsub  21203  hauscmplem  21209  txcnpi  21411  txcnp  21423  fbun  21644  fbfinnfr  21645  trfbas2  21647  fgcl  21682  filssufilg  21715  ufinffr  21733  isfcls  21813  fclsrest  21828  flimfnfcls  21832  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  cnextcn  21871  imasf1oxms  22294  metequiv2  22315  tngngpim  22463  iccpnfcnv  22743  iccpnfhmeo  22744  iscau2  23075  caun0  23079  minveclem3b  23199  itg1climres  23481  mbfi1fseqlem4  23485  ellimc3  23643  limccnp2  23656  dvlip  23756  itgsubstlem  23811  elply2  23952  coefv0  24004  coemulc  24011  ulmss  24151  sineq0  24273  scvxcvx  24712  sqf11  24865  ppiublem1  24927  fsumvma  24938  ostth  25328  mptelee  25775  brbtwn2  25785  colinearalg  25790  axcontlem4  25847  upgrres1  26205  usgr2trlncl  26656  umgrclwwlksge2  26912  clwlksfclwwlk  26962  clwwlksnun  26974  upgr4cycl4dv4e  27045  1to3vfriendship  27145  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrncvvdeqlem8  27170  frgrwopreg  27187  numclwwlkovf2exlem2  27212  numclwwlk2lem1  27235  frgrreg  27252  frgrogt3nreg  27255  nmcvcn  27550  chlimi  28091  ocsh  28142  shsvs  28182  h1datomi  28440  stcl  29075  stge0  29083  stle1  29084  stm1addi  29104  stm1add3i  29106  cvnsym  29149  mdbr2  29155  dmdbr2  29162  mdsl0  29169  mdsl1i  29180  mdsl2i  29181  cvmdi  29183  atexch  29240  atcvat4i  29256  cdj1i  29292  xrge0iifcnv  29979  esumpr2  30129  sigaclci  30195  cntmeas  30289  mbfmcnt  30330  ballotlemfc0  30554  ballotlemfcc  30555  bnj142OLD  30794  bnj1379  30901  bnj607  30986  bnj908  31001  bnj938  31007  bnj1174  31071  bnj1280  31088  iccllysconn  31232  funpsstri  31663  fundmpss  31664  fprb  31669  dfon2lem3  31690  dfon2lem4  31691  dfon2lem6  31693  dfon2lem9  31696  dfon2  31697  hbimtg  31712  hbaltg  31713  dftrpred3g  31733  poseq  31750  frrlem5b  31785  frrlem5d  31787  sltres  31815  nosepdmlem  31833  nocvxminlem  31893  nocvxmin  31894  dfrdg4  32058  btwntriv2  32119  btwncomim  32120  btwnswapid  32124  btwnexch3  32127  ifscgr  32151  lineunray  32254  hilbert1.2  32262  cldbnd  32321  tailfb  32372  meran3  32412  arg-ax  32415  ontopbas  32427  onsuct0  32440  limsucncmpi  32444  ordcmp  32446  onint1  32448  bj-gl4  32580  bj-alrimhi  32604  bj-alexim  32605  bj-ax6e  32653  bj-hbalt  32671  axc11n11r  32673  bj-hbsb3t  32712  bj-spimedv  32719  bj-cbv2hv  32731  bj-sbftv  32763  bj-axsep  32793  bj-equsal1t  32809  bj-mo3OLD  32832  bj-syl66ib  32833  bj-0int  33055  bj-bary1lem1  33161  topdifinffinlem  33195  isbasisrelowllem1  33203  isbasisrelowllem2  33204  iooelexlt  33210  finxpreclem1  33226  finxpreclem2  33227  wl-spae  33306  wl-19.8eqv  33309  wl-nfeqfb  33323  wl-lem-moexsb  33350  wl-mo3t  33358  wl-ax11-lem3  33364  fin2so  33396  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  ismblfin  33450  indexdom  33529  fzmul  33537  heibor1lem  33608  heibor  33620  exidu1  33655  rngoideu  33702  zerdivemp1x  33746  ispridl2  33837  orcomdd  33891  cnf1dd  33892  cnfn1dd  33894  cnfn2dd  33895  prtlem14  34159  prter2  34166  aev-o  34216  ax12eq  34226  ax12el  34227  ax12indn  34228  ax12indi  34229  lsatn0  34286  lsatcmp  34290  lsatcv0  34318  lfl1dim  34408  lfl1dim2N  34409  lkrss2N  34456  lub0N  34476  glb0N  34480  glbconxN  34664  hl2at  34691  cvrexchlem  34705  cvratlem  34707  cvrat4  34729  psubspi  35033  pointpsubN  35037  elpaddn0  35086  paddasslem17  35122  ispsubcl2N  35233  ldilval  35399  trlord  35857  diaelrnN  36334  cdlemm10N  36407  cdlemn11pre  36499  dihord2pre  36514  dihglblem2N  36583  dihglblem3N  36584  mapdrvallem2  36934  incssnn0  37274  fphpd  37380  rmxycomplete  37482  dford3lem1  37593  iocinico  37797  al3im  37938  brtrclfv2  38019  frege129d  38055  frege60a  38172  frege60c  38217  frege70  38227  rfovcnvf1od  38298  clsk1indlem3  38341  neik0pk1imk0  38345  gneispace  38432  gneispaceel2  38442  gneispacess2  38444  dvconstbi  38533  axc5c4c711toc7  38605  axc5c4c711to11  38606  pm14.24  38633  sbiota1  38635  bi33imp12  38696  bi123imp0  38702  ee233  38725  vk15.4j  38734  ssralv2  38737  alrim3con13v  38743  tratrb  38746  onfrALTlem3  38759  onfrALTlem2  38761  19.41rg  38766  hbimpg  38770  hbalg  38771  ax6e2ndeq  38775  e2  38856  ee223  38859  sspwtrALT  39049  sspwtrALT2  39058  suctrALT2  39072  trintALT  39117  isosctrlem1ALT  39170  fnchoice  39188  mptfnd  39451  stoweidlem62  40279  2reu1  41186  ffnafv  41251  lswn0  41380  bgoldbnnsum3prm  41692  bgoldbtbndlem2  41694  bgoldbtbndlem4  41696  ply1mulgsumlem2  42175  iunord  42422  setrec2fun  42439