NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl GIF version

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 (φψ)
syl.2 (ψχ)
Assertion
Ref Expression
syl (φχ)

Proof of Theorem syl
StepHypRef Expression
1 syl.1 . 2 (φψ)
2 syl.2 . . 3 (ψχ)
32a1i 10 . 2 (φ → (ψχ))
41, 3mpd 14 1 (φχ)
Colors of variables: wff setvar class
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  2502  neeq1d  2529  neeq2d  2530  neleq12d  2609  ral2imi  2690  reximdai  2722  r19.12  2727  rexlimd2  2736  r19.29  2754  raleqdv  2813  rexeqdv  2814  rabeqbidv  2854  rabeqbidva  2855  cgsexg  2890  cgsex2g  2891  cgsex4g  2892  vtoclgft  2905  vtoclgf  2913  vtocleg  2925  spcgft  2931  rspct  2948  rspc2ev  2963  pm13.183  2979  dedhb  3006  eueq3  3011  moeq3  3013  mob  3018  morex  3020  euind  3023  reuind  3039  2rmorex  3040  2reu5  3044  sbceq1d  3051  sbcco2  3069  sbcieg  3078  sbceqal  3097  sbcabel  3123  spesbcd  3128  csbeq1d  3142  csbvarg  3163  sbcnestgf  3183  csbidmg  3190  csbco3g  3193  nineq1d  3240  nineq2d  3241  compleqd  3245  symdifeq1d  3254  symdifeq2d  3255  sseldi  3271  sseld  3272  sseq1d  3298  sseq2d  3299  uniiunlem  3353  psseq1d  3361  psseq2d  3362  pssssd  3366  pssned  3367  difeq1d  3384  difeq2d  3385  difss2d  3396  ssdifd  3402  sscond  3403  ssdifssd  3404  uneq1d  3417  uneq2d  3418  ineq1d  3456  ineq2d  3457  uneqin  3506  reuss2  3535  reupick2  3541  abvor0  3567  eq0rdv  3585  ssdisj  3600  ssnelpssd  3614  uneqdifeq  3638  ifsb  3671  ifeq1d  3676  ifeq2d  3677  ifbid  3680  elimif  3691  ifbothda  3692  ifeqor  3699  ifnot  3700  ifan  3701  dedth  3703  elimhyp  3710  elimhyp2v  3711  elimhyp3v  3712  elimhyp4v  3713  elimdhyp  3715  keephyp2v  3717  keephyp3v  3718  pweqd  3727  elpwid  3731  sneqd  3746  elpr2  3752  ifpr  3774  rabsnt  3797  preq1d  3805  preq2d  3806  tpeq1d  3811  tpeq2d  3812  tpeq3d  3813  snnzg  3833  snssd  3853  ssunsn2  3865  unsneqsn  3887  unieqd  3902  unissd  3915  inteqd  3931  intmin3  3954  intmin4  3955  intab  3956  ss2iun  3984  iineq2  3986  iineq2d  3989  iuneq2dv  3990  iuneq1d  3992  dfiin2g  4000  ssiun  4008  iinss  4017  riinn0  4040  opkeq1d  4065  opkeq2d  4066  inexg  4100  xpkeq1d  4204  xpkeq2d  4205  cnvkeqd  4217  ins2keqd  4222  ins3keqd  4223  imakeq1d  4228  imakeq2d  4229  cokeq1d  4234  cokeq2d  4235  p6eqd  4240  sikeqd  4243  opkelimagekg  4271  cokrelk  4284  xpkexg  4288  uni1exg  4292  pw1exg  4302  cokexg  4309  imagekexg  4311  uniexg  4316  pwexg  4328  pw1equn  4331  pw1eqadj  4332  sspw1  4335  sspw12  4336  iotaval  4350  iotassuni  4355  iota4  4357  iota4an  4358  iotabidv  4360  iota2df  4365  dfiota4  4372  addceq2  4384  addceq1d  4389  addceq2d  4390  dfnnc2  4395  peano5  4409  nnsucelr  4428  nndisjeq  4429  leltfintr  4458  ltfintr  4459  ltfintri  4466  ssfin  4470  ncfinprop  4474  ncfinlower  4483  eqtfinrelk  4486  tfinprop  4489  tfinnnul  4490  tfin11  4493  tfinpw1  4494  ncfintfin  4495  tfindi  4496  tfinsuc  4498  tfinltfinlem1  4500  tfinltfin  4501  evennn  4506  oddnn  4507  sucevenodd  4510  sucoddeven  4511  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnadjoinpw  4521  sfindbl  4530  sfintfin  4532  tfinnn  4534  sfinltfin  4535  sfin111  4536  spfininduct  4540  vfinspnn  4541  t1csfin1c  4545  vfin1cltv  4547  vfinncvntnn  4548  vfinspsslem1  4550  vfinspss  4551  vfinspeqtncv  4553  vfinncsp  4554  vinf  4555  nulnnn  4556  peano4  4557  addccan2  4559  dfphi2  4569  opeq1d  4584  opeq2d  4585  phi11lem1  4595  copsexg  4607  copsex2t  4608  copsex2g  4609  mosubopt  4612  phidisjnn  4615  phialllem1  4616  phialllem2  4617  phiall  4618  breq1d  4649  breqd  4650  breq2d  4651  opelopabsb  4697  ssopab2dv  4715  coexg  4749  xpeq1d  4807  xpeq2d  4808  opeliunxp  4820  ssrel  4844  coeq1d  4878  coeq2d  4879  cnveqd  4888  dmeqd  4909  opeldm  4910  reseq1d  4933  reseq2d  4934  imaeq1d  4941  imaeq2d  4942  rneqd  4958  rnss  4959  dmiin  4965  dmcoeq  4974  ssres2  4991  imass1  5023  imass2  5024  xpsndisj  5049  dmxpss  5052  dmsnopss  5067  dmexg  5105  dfxp2  5113  funss  5126  funeqd  5129  funun  5146  funprg  5149  funprgOLD  5150  fununi  5160  funcnvuni  5161  fun11uni  5162  fneq1d  5175  fneq2d  5176  fnco  5191  2elresin  5194  fnssresb  5195  feq1d  5214  feq2d  5215  ffun  5225  fdm  5226  fssxp  5232  ffdm  5234  fcoi1  5240  fcoi2  5241  dmfex  5247  f00  5249  fnconstg  5252  f1fn  5259  f1fun  5260  f1dm  5261  fofun  5270  fofn  5271  f1of  5287  f1ofn  5288  f1ofun  5289  f1odm  5290  f1orescnv  5301  f1imacnv  5302  foimacnv  5303  fun11iun  5305  resdif  5306  resin  5307  f1ococnv2  5309  f1ococnv1  5310  f1cnv  5311  f1cocnv1  5312  f1cocnv2  5313  f1o00  5317  fo00  5318  f1osng  5323  fvprc  5325  fveq1d  5330  fveq2d  5332  tz6.12i  5348  ndmfv  5349  elfvdm  5351  nfvres  5352  nfunsn  5353  fnbrfvb  5358  fvun  5378  fvun1  5379  fvopab4ndm  5390  fvreseq  5398  respreima  5410  fnasrn  5417  dff3  5420  dffo3  5422  dffo4  5423  dffo5  5424  fsn  5432  fsng  5433  fsn2  5434  ressnop0  5436  fressnfv  5439  fvconst  5440  fvunsn  5444  fconst3  5457  dff13  5471  f1fveq  5473  f1ofveu  5480  f1ocnvdm  5481  isocnv  5491  isores1  5494  isotr  5495  isomin  5496  isoini  5497  isoini2  5498  1stfo  5505  2ndfo  5506  funsi  5520  oveq1d  5537  oveq2d  5538  oveqd  5539  fnoprabg  5585  ovg  5601  oprssdm  5612  ndmovg  5613  ndmovass  5618  ndmovdistr  5619  ndmovord  5620  ndmovordi  5621  caovmo  5645  elovex12  5648  fmpt  5692  fmpt2d  5695  fvmptss  5705  fvmptex  5721  fvmptss2  5725  f1od  5726  f1o2d  5727  brtxp  5783  fixexg  5788  otelins2  5791  otelins3  5792  oqelins4  5794  txpcofun  5803  epprc  5827  pprodeq1  5834  pprodeq2  5835  pw1fnval  5851  pw1fnf1o  5855  brfullfung  5865  fvdomfn  5868  fvranfn  5869  clos1eq1  5874  clos1eq2  5875  clos1induct  5880  clos1basesuc  5882  clos1nrel  5886  trd  5921  frd  5922  extd  5923  symd  5924  refd  5927  antid  5929  connexd  5931  frds  5935  weds  5938  ersym  5952  ertr  5954  ertrd  5955  erref  5959  ecss  5966  erth  5968  erth2  5969  erthi  5970  erdisj  5972  ecelqsg  5979  qsexg  5982  uniqs  5984  uniqs2  5985  qsss  5986  qsdisj  5995  ecoptocl  5996  mapsspm  6021  mapsspw  6022  map0b  6024  mapsn  6026  bren  6030  ensymi  6036  entr  6038  en0  6042  fundmen  6043  en2sn  6047  unen  6048  xpen  6055  enadj  6060  enpw1  6062  enmap2lem3  6065  enmap2lem5  6067  enmap2  6068  enmap1lem3  6071  enmap1lem5  6073  enmap1  6074  enprmaplem3  6078  enprmaplem5  6080  enprmap  6082  nenpw1pwlem2  6085  enpw  6087  nceqd  6110  ncelncs  6120  eqncg  6126  ncseqnc  6128  ncdisjun  6136  1cnc  6139  peano4nc  6150  ncspw1eu  6159  tccl  6160  pw1eltc  6162  tcdi  6164  pw1fin  6169  nntccl  6170  ovcelem1  6171  ce0addcnnul  6179  ce0nn  6180  ceclnn1  6189  ce0  6190  ncpw1pwneg  6201  ltcpw1pwg  6202  sbthlem1  6203  sbthlem3  6205  sbth  6206  addlecncs  6209  dflec2  6210  leconnnc  6218  ce2lt  6220  dflec3  6221  nclenc  6222  lenc  6223  tcncg  6224  ce0t  6232  tce2  6236  te0c  6237  ce0lenc1  6239  finnc  6243  brtcfn  6246  ncfin  6247  nclenn  6249  addcdi  6250  nnltp1c  6262  addccan2nclem2  6264  ncslesuc  6267  nmembers1lem2  6269  nmembers1lem3  6270  nmembers1  6271  nnc3n3p1  6278  nnc3p1n3p2  6280  spacval  6282  spacind  6287  nchoicelem1  6289  nchoicelem2  6290  nchoicelem3  6291  nchoicelem4  6292  nchoicelem6  6294  nchoicelem7  6295  nchoicelem9  6297  nchoicelem11  6299  nchoicelem12  6300  nchoicelem13  6301  nchoicelem14  6302  nchoicelem16  6304  nchoicelem17  6305  nchoicelem19  6307  freceq12  6311  frecxp  6314  dmfrec  6316  fnfreclem1  6317  fnfreclem2  6318  fnfreclem3  6319  fnfrec  6320  frec0  6321  frecsuc  6322  scancan  6331  canncb  6332
  Copyright terms: Public domain W3C validator