Theorem syl 15

Description: An inference version of the transitive laws for implication imim2 49 and imim1 70, which Russell and Whitehead call "the principle of the syllogism...because...the syllogism in Barbara is derived from them" (quote after Theorem *2.06 of [WhiteheadRussell] p. 101). Some authors call this law a "hypothetical syllogism."

(A bit of trivia: this is the most commonly referenced assertion in our database. In second place is eqid 2353, followed by syl2anc 642, adantr 451, syl3anc 1182, and ax-mp 5. The Metamath program command 'show usage' shows the number of references.) (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 20-Oct-2011.) (Proof shortened by Wolf Lammen, 26-Jul-2012.)

Hypotheses

Ref	Expression
syl.1	|- (ph -> ps)
syl.2	|- (ps -> ch)

Assertion

Ref	Expression
syl	|- (ph -> ch)

Proof of Theorem syl

Step	Hyp	Ref	Expression
1		syl.1	. 2 |- (ph -> ps)
2		syl.2	. . 3 |- (ps -> ch)
3	2	a1i 10	. 2 |- (ph -> (ps -> ch))
4	1, 3	mpd 14	1 |- (ph -> ch)

Syntax hints:   -> wi 4

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

This theorem is referenced by:  3syl  18  a1d  22  a2d  23  sylcom  25  syl2im  34  sylsyld  52  pm2.86i  92  con4d  97  pm2.18d  103  notnotrd  105  nsyl4  134  bi1  178  sylbi  187  sylib  188  biimpd  198  sylibr  203  sylbir  204  orrd  367  orcoms  378  orcd  381  orcs  383  biortn  395  simpld  445  biantrud  493  biantrurd  494  condan  769  dedlem0a  918  elimh  922  dedt  923  simp1d  967  simp2d  968  simp3d  969  3adant1  973  3adant2  974  3adant3  975  syl12anc  1180  syl21anc  1181  syl3anc  1182  syl3an1  1215  syl3an  1224  nanbi1d  1301  nanbi2d  1302  ee10  1376  cadan  1392  nic-axALT  1439  merco1  1478  al2imi  1561  alimdh  1563  alrimih  1565  exbi  1581  eximdh  1588  albidh  1590  exbidh  1591  19.29  1596  19.29r2  1598  19.29x  1599  19.25  1603  19.40-2  1610  exlimiv  1634  19.8w  1660  spimeh  1667  equcoms  1681  equequ1OLD  1685  hbalw  1709  a7s  1735  hbal  1736  sps  1754  19.21bi  1758  19.23bi  1759  nfrd  1763  hbnOLD  1777  19.9d  1782  nfnd  1791  nfndOLD  1792  nfimdOLD  1809  equsalhwOLD  1839  cbv3hv  1850  cbv3hvOLD  1851  nfald  1852  nfaldOLD  1853  19.41  1879  hbnd  1883  sb4a  1923  sb4e  1924  ax10lem1  1936  ax10lem3  1938  dvelimv  1939  ax10lem5  1942  aecoms  1947  ax9  1949  ax9o  1950  hbae  1953  hbnaes  1957  equs4  1959  spimed  1977  equveli  1988  equs45f  1989  aev  1991  ax11v2  1992  cbvald  2008  stdpc4  2024  sb6f  2039  hbsb2a  2041  hbsb2e  2042  hbsb3  2043  ax16i  2046  ax16ALT2  2048  sbequi  2059  spsbim  2076  sbbid  2078  dvelimdf  2082  sbco3  2088  sbcom  2089  nfsbd  2111  sbal2  2134  ax5  2146  aecom-o  2151  aecoms-o  2152  hbae-o  2153  equid1  2158  sps-o  2159  ax46to4  2163  ax46to6  2164  ax67  2165  ax67to7  2168  ax467to4  2170  ax467to7  2172  equid1ALT  2176  ax10from10o  2177  ax10-16  2190  ax11eq  2193  ax11el  2194  ax11indalem  2197  ax11inda2ALT  2198  ax11inda  2200  ax11v2-o  2201  eujustALT  2207  mo  2226  mo2  2233  exmoeu  2246  euor2  2272  moexex  2273  2eu2ex  2278  2exeu  2281  2mo  2282  2eu1  2284  2eu5  2288  bamalip  2324  axi5r  2326  bm1.1  2338  eqeq1d  2361  eqeq2d  2364  eleq1d  2419  eleq2d  2420  nfcrd  2503  neeq1d  2530  neeq2d  2531  neleq12d  2610  ral2imi  2691  reximdai  2723  r19.12  2728  rexlimd2  2737  r19.29  2755  raleqdv  2814  rexeqdv  2815  rabeqbidv  2855  rabeqbidva  2856  cgsexg  2891  cgsex2g  2892  cgsex4g  2893  vtoclgft  2906  vtoclgf  2914  vtocleg  2926  spcgft  2932  rspct  2949  rspc2ev  2964  pm13.183  2980  dedhb  3007  eueq3  3012  moeq3  3014  mob  3019  morex  3021  euind  3024  reuind  3040  2rmorex  3041  2reu5  3045  sbceq1d  3052  sbcco2  3070  sbcieg  3079  sbceqal  3098  sbcabel  3124  spesbcd  3129  csbeq1d  3143  csbvarg  3164  sbcnestgf  3184  csbidmg  3191  csbco3g  3194  nineq1d  3241  nineq2d  3242  compleqd  3246  symdifeq1d  3255  symdifeq2d  3256  sseldi  3272  sseld  3273  sseq1d  3299  sseq2d  3300  uniiunlem  3354  psseq1d  3362  psseq2d  3363  pssssd  3367  pssned  3368  difeq1d  3385  difeq2d  3386  difss2d  3397  ssdifd  3403  sscond  3404  ssdifssd  3405  uneq1d  3418  uneq2d  3419  ineq1d  3457  ineq2d  3458  uneqin  3507  reuss2  3536  reupick2  3542  abvor0  3568  eq0rdv  3586  ssdisj  3601  ssnelpssd  3615  uneqdifeq  3639  ifsb  3672  ifeq1d  3677  ifeq2d  3678  ifbid  3681  elimif  3692  ifbothda  3693  ifeqor  3700  ifnot  3701  ifan  3702  dedth  3704  elimhyp  3711  elimhyp2v  3712  elimhyp3v  3713  elimhyp4v  3714  elimdhyp  3716  keephyp2v  3718  keephyp3v  3719  pweqd  3728  elpwid  3732  sneqd  3747  elpr2  3753  ifpr  3775  rabsnt  3798  preq1d  3806  preq2d  3807  tpeq1d  3812  tpeq2d  3813  tpeq3d  3814  snnzg  3834  snssd  3854  ssunsn2  3866  unsneqsn  3888  unieqd  3903  unissd  3916  inteqd  3932  intmin3  3955  intmin4  3956  intab  3957  ss2iun  3985  iineq2  3987  iineq2d  3990  iuneq2dv  3991  iuneq1d  3993  dfiin2g  4001  ssiun  4009  iinss  4018  riinn0  4041  opkeq1d  4066  opkeq2d  4067  inexg  4101  xpkeq1d  4205  xpkeq2d  4206  cnvkeqd  4218  ins2keqd  4223  ins3keqd  4224  imakeq1d  4229  imakeq2d  4230  cokeq1d  4235  cokeq2d  4236  p6eqd  4241  sikeqd  4244  opkelimagekg  4272  cokrelk  4285  xpkexg  4289  uni1exg  4293  pw1exg  4303  cokexg  4310  imagekexg  4312  uniexg  4317  pwexg  4329  pw1equn  4332  pw1eqadj  4333  sspw1  4336  sspw12  4337  iotaval  4351  iotassuni  4356  iota4  4358  iota4an  4359  iotabidv  4361  iota2df  4366  dfiota4  4373  addceq2  4385  addceq1d  4390  addceq2d  4391  dfnnc2  4396  peano5  4410  nnsucelr  4429  nndisjeq  4430  leltfintr  4459  ltfintr  4460  ltfintri  4467  ssfin  4471  ncfinprop  4475  ncfinlower  4484  eqtfinrelk  4487  tfinprop  4490  tfinnnul  4491  tfin11  4494  tfinpw1  4495  ncfintfin  4496  tfindi  4497  tfinsuc  4499  tfinltfinlem1  4501  tfinltfin  4502  evennn  4507  oddnn  4508  sucevenodd  4511  sucoddeven  4512  evenodddisj  4517  eventfin  4518  oddtfin  4519  nnadjoin  4521  nnadjoinpw  4522  sfindbl  4531  sfintfin  4533  tfinnn  4535  sfinltfin  4536  sfin111  4537  spfininduct  4541  vfinspnn  4542  t1csfin1c  4546  vfin1cltv  4548  vfinncvntnn  4549  vfinspsslem1  4551  vfinspss  4552  vfinspeqtncv  4554  vfinncsp  4555  vinf  4556  nulnnn  4557  peano4  4558  addccan2  4560  dfphi2  4570  opeq1d  4585  opeq2d  4586  phi11lem1  4596  copsexg  4608  copsex2t  4609  copsex2g  4610  mosubopt  4613  phidisjnn  4616  phialllem1  4617  phialllem2  4618  phiall  4619  breq1d  4650  breqd  4651  breq2d  4652  opelopabsb  4698  ssopab2dv  4716  coexg  4750  xpeq1d  4808  xpeq2d  4809  opeliunxp  4821  ssrel  4845  coeq1d  4879  coeq2d  4880  cnveqd  4889  dmeqd  4910  opeldm  4911  reseq1d  4934  reseq2d  4935  imaeq1d  4942  imaeq2d  4943  rneqd  4959  rnss  4960  dmiin  4966  dmcoeq  4975  ssres2  4992  imass1  5024  imass2  5025  xpsndisj  5050  dmxpss  5053  dmsnopss  5068  dmexg  5106  dfxp2  5114  funss  5127  funeqd  5130  funun  5147  funprg  5150  funprgOLD  5151  fununi  5161  funcnvuni  5162  fun11uni  5163  fneq1d  5176  fneq2d  5177  fnco  5192  2elresin  5195  fnssresb  5196  feq1d  5215  feq2d  5216  ffun  5226  fdm  5227  fssxp  5233  ffdm  5235  fcoi1  5241  fcoi2  5242  dmfex  5248  f00  5250  fnconstg  5253  f1fn  5260  f1fun  5261  f1dm  5262  fofun  5271  fofn  5272  f1of  5288  f1ofn  5289  f1ofun  5290  f1odm  5291  f1orescnv  5302  f1imacnv  5303  foimacnv  5304  fun11iun  5306  resdif  5307  resin  5308  f1ococnv2  5310  f1ococnv1  5311  f1cnv  5312  f1cocnv1  5313  f1cocnv2  5314  f1o00  5318  fo00  5319  f1osng  5324  fvprc  5326  fveq1d  5331  fveq2d  5333  tz6.12i  5349  ndmfv  5350  elfvdm  5352  nfvres  5353  nfunsn  5354  fnbrfvb  5359  fvun  5379  fvun1  5380  fvopab4ndm  5391  fvreseq  5399  respreima  5411  fnasrn  5418  dff3  5421  dffo3  5423  dffo4  5424  dffo5  5425  fsn  5433  fsng  5434  fsn2  5435  ressnop0  5437  fressnfv  5440  fvconst  5441  fvunsn  5445  fconst3  5458  dff13  5472  f1fveq  5474  f1ofveu  5481  f1ocnvdm  5482  isocnv  5492  isores1  5495  isotr  5496  isomin  5497  isoini  5498  isoini2  5499  1stfo  5506  2ndfo  5507  funsi  5521  oveq1d  5538  oveq2d  5539  oveqd  5540  fnoprabg  5586  ovg  5602  oprssdm  5613  ndmovg  5614  ndmovass  5619  ndmovdistr  5620  ndmovord  5621  ndmovordi  5622  caovmo  5646  elovex12  5649  fmpt  5693  fmpt2d  5696  fvmptss  5706  fvmptex  5722  fvmptss2  5726  f1od  5727  f1o2d  5728  brtxp  5784  fixexg  5789  otelins2  5792  otelins3  5793  oqelins4  5795  txpcofun  5804  epprc  5828  pprodeq1  5835  pprodeq2  5836  pw1fnval  5852  pw1fnf1o  5856  brfullfung  5866  fvdomfn  5869  fvranfn  5870  clos1eq1  5875  clos1eq2  5876  clos1induct  5881  clos1basesuc  5883  clos1nrel  5887  trd  5922  frd  5923  extd  5924  symd  5925  refd  5928  antid  5930  connexd  5932  frds  5936  weds  5939  ersym  5953  ertr  5955  ertrd  5956  erref  5960  ecss  5967  erth  5969  erth2  5970  erthi  5971  erdisj  5973  ecelqsg  5980  qsexg  5983  uniqs  5985  uniqs2  5986  qsss  5987  qsdisj  5996  ecoptocl  5997  mapsspm  6022  mapsspw  6023  map0b  6025  mapsn  6027  bren  6031  ensymi  6037  entr  6039  en0  6043  fundmen  6044  en2sn  6048  unen  6049  xpen  6056  enadj  6061  enpw1  6063  enmap2lem3  6066  enmap2lem5  6068  enmap2  6069  enmap1lem3  6072  enmap1lem5  6074  enmap1  6075  enprmaplem3  6079  enprmaplem5  6081  enprmap  6083  nenpw1pwlem2  6086  enpw  6088  nceqd  6111  ncelncs  6121  eqncg  6127  ncseqnc  6129  ncdisjun  6137  1cnc  6140  peano4nc  6151  ncspw1eu  6160  tccl  6161  pw1eltc  6163  tcdi  6165  pw1fin  6170  nntccl  6171  ovcelem1  6172  ce0addcnnul  6180  ce0nn  6181  ceclnn1  6190  ce0  6191  ncpw1pwneg  6202  ltcpw1pwg  6203  sbthlem1  6204  sbthlem3  6206  sbth  6207  addlecncs  6210  dflec2  6211  leconnnc  6219  ce2lt  6221  dflec3  6222  nclenc  6223  lenc  6224  tcncg  6225  ce0t  6233  tce2  6237  te0c  6238  ce0lenc1  6240  finnc  6244  brtcfn  6247  ncfin  6248  nclenn  6250  addcdi  6251  nnltp1c  6263  addccan2nclem2  6265  ncslesuc  6268  nmembers1lem2  6270  nmembers1lem3  6271  nmembers1  6272  nnc3n3p1  6279  nnc3p1n3p2  6281  spacval  6283  spacind  6288  nchoicelem1  6290  nchoicelem2  6291  nchoicelem3  6292  nchoicelem4  6293  nchoicelem6  6295  nchoicelem7  6296  nchoicelem9  6298  nchoicelem11  6300  nchoicelem12  6301  nchoicelem13  6302  nchoicelem14  6303  nchoicelem16  6305  nchoicelem17  6306  nchoicelem19  6308  freceq12  6312  frecxp  6315  dmfrec  6317  fnfreclem1  6318  fnfreclem2  6319  fnfreclem3  6320  fnfrec  6321  frec0  6322  frecsuc  6323  scancan  6332  canncb  6333