ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl Structured version   GIF version

Theorem syl 14
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." (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 9 . 2 (φ → (ψχ))
41, 3mpd 13 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  3syl  17  4syl  18  a1d  22  a2d  23  sylcom  25  syl2im  34  sylsyld  52  pm2.86i  92  simpld  105  simprd  107  sylbi  114  sylbir  125  sylib  127  biimpd  132  sylibr  137  biantrud  288  biantrurd  289  pm2.01d  536  pm2.21d  537  pm2.24d  540  pm5.21nii  607  ord  630  orcoms  636  orcd  639  orcs  641  biortn  651  pm4.67dc  769  annimim  770  imordc  784  pm4.54dc  793  pm4.55dc  832  dn1dc  853  dedlem0a  861  oplem1  868  simp1d  902  simp2d  903  simp3d  904  3adant1  908  3adant2  909  3adant3  910  syl12anc  1117  syl21anc  1118  syl3anc  1119  syl3an1  1152  syl3an  1161  ecased  1222  xornbi  1258  pm5.15dc  1261  anxordi  1272  mpisyl  1311  a7s  1319  al2imi  1323  alimdh  1332  alrimih  1334  alcoms  1341  hbal  1342  albidh  1345  alequcoms  1386  nalequcoms  1387  nfrd  1390  sps  1408  hbor  1416  19.21bi  1428  nford  1437  nfand  1438  hbimd  1443  19.23bi  1461  exbi  1473  eximdh  1480  exbidh  1483  19.29  1489  19.29r2  1491  19.29x  1492  19.35-1  1493  19.25  1495  19.40-2  1501  i19.24  1508  i19.39  1509  alexim  1514  exanaliim  1516  hbnt  1521  hbnd  1523  nfnd  1525  19.9d  1529  19.36i  1540  19.41h  1553  ax9o  1566  equcoms  1572  ax10  1583  hbae  1584  hbaes  1586  hbnaes  1589  naecoms  1590  equs4  1591  equsexd  1595  spimt  1602  spimh  1603  cbv1h  1611  cbv2  1613  equvini  1619  equveli  1620  nfald  1621  nfexd  1622  stdpc4  1636  sbh  1637  equs5e  1654  ax10oe  1656  sb4a  1660  equs45f  1661  sb6f  1662  sb4e  1664  hbsb2a  1665  hbsb2e  1666  hbsb3  1667  ax16  1672  dveeq2  1674  ax11v2  1679  equs5or  1689  sbequi  1698  spsbe  1701  spsbim  1702  sbbid  1704  sbidm  1709  ax16i  1716  sbi2v  1750  cbvexdh  1779  nfsbt  1828  sbalyz  1853  dvelimdf  1870  sbal2  1876  mo23  1919  mor  1920  modc  1921  eu2  1922  mo3h  1931  euor2  1936  moexexdc  1962  2eu2ex  1967  bamalip  1999  bm1.1  2003  eqeq1d  2026  eqeq2d  2029  eleq1d  2084  eleq2d  2085  nfcrd  2169  neeq1d  2198  neeq2d  2199  neleq12d  2277  ral2imi  2359  rexim  2387  reximdai  2391  r19.12  2396  rexlimd2  2405  r19.29  2424  r19.29d2r  2429  r19.29_2a  2430  r19.35-1  2434  r19.36av  2435  raleqdv  2485  rexeqdv  2486  rabeqbidv  2526  rabeqbidva  2527  cgsexg  2562  cgsex2g  2563  cgsex4g  2564  vtoclgft  2577  vtoclgf  2585  vtocleg  2597  spcgft  2603  spcegft  2605  spc3gv  2618  rspct  2622  rspc2ev  2637  eqvincg  2641  pm13.183  2654  dedhb  2683  eueq3dc  2688  mosubt  2691  mob  2696  morex  2698  euind  2701  reuind  2717  sbceq1d  2742  sbcco2  2759  sbceqal  2787  sbcabel  2812  spesbcd  2817  rmo2i  2821  csbeq1d  2831  csbvarg  2850  sbcnestgf  2870  csbidmg  2875  csbco3g  2877  sseldi  2916  sseld  2917  sseq1d  2945  sseq2d  2946  uniiunlem  3001  psseq1d  3009  psseq2d  3010  pssssd  3014  pssned  3015  difeq1d  3034  difeq2d  3035  difss2d  3046  ssdifd  3052  sscond  3053  ssdifssd  3054  uneq1d  3069  uneq2d  3070  ineq1d  3110  ineq2d  3111  uneqin  3161  reuss2  3190  reupick2  3196  eq0rdv  3234  ssdisj  3250  ssnelpssd  3263  uneqdifeqim  3281  ralm  3300  ifeq1d  3318  ifeq2d  3319  ifbid  3322  pweqd  3335  elpwid  3340  sneqd  3359  elpr2  3365  rabsnt  3415  preq1d  3423  preq2d  3424  tpeq1d  3429  tpeq2d  3430  tpeq3d  3431  snnzg  3455  snmg  3456  prmg  3459  snssd  3479  opeq1d  3525  opeq2d  3526  oteq1d  3531  oteq2d  3532  oteq3d  3533  opprc1  3541  opprc2  3542  oprcl  3543  unieqd  3561  unissd  3574  inteqd  3590  intmin3  3612  intmin4  3613  intab  3614  ss2iun  3642  iineq2  3644  iineq2d  3647  iuneq2dv  3648  iuneq1d  3650  dfiin2g  3660  ssiun  3669  iinss  3678  riinm  3699  disjss2  3718  disjeq2  3719  disjeq2dv  3720  disjss1  3721  disjeq1  3722  disjeq1d  3723  invdisj  3729  breq1d  3744  breqd  3745  breq2d  3746  mpteq1d  3812  triun  3837  trint  3839  repizf  3843  a9evsep  3849  nalset  3857  elssabg  3872  inteximm  3873  iinexgm  3878  pwne  3883  class2seteq  3886  bnd2  3896  abssexg  3904  snexgOLD  3905  snexg  3906  prelpwi  3920  rext  3921  pwel  3924  exss  3933  opexg  3934  opexgOLD  3935  opm  3941  opth1  3943  opth  3944  copsex2t  3952  copsex2g  3953  0nelop  3955  moop2  3958  opelopabsb  3967  ssopab2dv  3985  pwssunim  3991  poeq2  4007  sotritric  4031  sotritrieq  4032  sess1  4038  sess2  4039  seeq1  4040  seeq2  4041  onelss  4069  ordtr1  4070  ontr1  4071  limuni2  4079  suctr  4104  trsuc  4105  tpexg  4125  eusvnf  4131  eusvnfb  4132  ralxfr2d  4142  rexxfr2d  4143  ralxfrALT  4145  reuhypd  4149  eldifpw  4154  op1stbg  4156  iunpw  4157  ssorduni  4159  ssonuni  4160  onun2  4162  onss  4165  orduni  4167  bm2.5ii  4168  ordsucim  4172  suceloni  4173  sucelon  4175  ordsucss  4176  onsucsssucr  4180  sucunielr  4181  ordtriexmidlem  4188  ordtri2orexmid  4191  onsucsssucexmid  4192  ordsucunielexmid  4196  regexmidlem1  4198  elirr  4204  en2lp  4212  opthreg  4214  ordsoexmid  4220  ordsuc  4221  ordpwsucss  4223  onnmin  4224  tfi  4228  tfisi  4233  peano2  4241  peano5  4244  findes  4249  nnord  4257  peano2b  4260  nn0eln0  4264  xpeq1d  4291  xpeq2d  4292  otelxp1  4302  mosubopt  4328  releqd  4347  relssdv  4355  xpsspw  4373  xpiindim  4396  relop  4409  ideqg  4410  coeq1d  4420  coeq2d  4421  cnveqd  4434  dmeqd  4460  rneqd  4486  rnss  4487  dmiin  4503  elrnmptg  4509  riinint  4516  dmrnssfld  4518  dmcosseq  4526  dmcoeq  4527  reseq1d  4534  reseq2d  4535  ssres2  4561  imaeq1d  4590  imaeq2d  4591  imasng  4613  elreimasng  4614  iniseg  4620  imass1  4623  imass2  4624  issref  4630  poirr2  4640  xpsndisj  4672  xpima1  4690  xpimasn  4692  opswapg  4730  elxp4  4731  elxp5  4732  relcoi1  4772  cnviinm  4782  iotaval  4801  iotanul  4805  iota4  4808  iota4an  4809  iotabidv  4811  iota2df  4814  funmo  4839  funss  4842  funeq  4843  funeqd  4845  funeu  4848  funco  4862  funun  4866  funcnvsn  4867  funprg  4871  funtpg  4872  fntpg  4877  fununi  4889  funcnvuni  4890  fun11uni  4891  funcnvres2  4896  imadiflem  4900  funimaexglem  4904  fneq1d  4911  fneq2d  4912  fnrel  4919  fneu  4925  fnco  4929  fnresdm  4930  2elresin  4932  fnssresb  4933  feq1d  4956  feq2d  4957  feq123d  4959  ffun  4970  frel  4971  fdm  4972  fco2  4978  fssxp  4979  ffdm  4982  fresin  4989  fcoi1  4991  fcoi2  4992  dmfex  5000  f00  5002  fnconstg  5005  f1fn  5014  f1fun  5015  f1rel  5016  f1dm  5017  f1ssres  5020  fofun  5028  fofn  5029  foima  5032  f1eq123d  5042  foeq123d  5043  f1oeq123d  5044  f1of  5047  f1ofn  5048  f1ofun  5049  f1orel  5050  f1odm  5051  f1ores  5062  f1orescnv  5063  f1imacnv  5064  foimacnv  5065  fun11iun  5068  resdif  5069  f1cnv  5071  fococnv2  5073  f1ococnv2  5074  f1cocnv2  5075  f1ococnv1  5076  f1cocnv1  5077  f1o00  5082  fo00  5083  f1osng  5088  brprcneu  5092  fvprc  5093  fveq1d  5101  fveq2d  5103  fvssunirng  5111  relfvssunirn  5112  funfvex  5113  fvexg  5115  sefvex  5117  relelfvdm  5126  nfvres  5127  nfunsn  5128  fnbrfvb  5135  funbrfv2b  5139  fvelrnb  5142  feqmptd  5147  fniinfv  5152  ssimaex  5155  funfvdm  5157  fvun1  5160  dmfco  5162  fvco2  5163  fvmptssdm  5176  fvmptdf  5179  fvmptdv2  5181  mpteqb  5182  eqfnfv  5186  fvreseq  5192  fndmdif  5193  fndmin  5195  chfnrn  5199  fvimacnvi  5202  fvimacnv  5203  fniniseg  5208  fniniseg2  5210  inpreima  5214  difpreima  5215  respreima  5216  fvelrn  5219  elrnrexdm  5227  ralrnmpt  5230  rexrnmpt  5231  dff3im  5233  dffo3  5235  dffo4  5236  dffo5  5237  fmpt  5240  f1ompt  5241  fmpt2d  5248  f1oresrab  5250  fmptco  5251  fmptcof  5252  fcompt  5254  fsn  5256  fsng  5257  fsn2  5258  dfmptg  5263  ressnop0  5265  fprg  5267  ftpg  5268  fressnfv  5271  fvconst  5272  fmptap  5274  fmptpr  5276  fvunsng  5278  fsnunf  5283  fsnunfv  5284  fconst3m  5301  resfunexg  5303  eufnfv  5310  fniunfv  5322  elunirn  5326  fnunirn  5327  dff13  5328  f1mpt  5331  f1ocnvfv2  5339  f1ocnvdm  5342  fcof1  5344  cbvfo  5346  cbvexfo  5347  cocan1  5348  fcof1o  5350  foeqcnvco  5351  f1eqcocnv  5352  fliftrel  5353  fliftel  5354  fliftfun  5357  fliftf  5360  isocnv  5372  isocnv2  5373  isores1  5375  isoini  5378  isoini2  5379  isopolem  5382  isopo  5383  isosolem  5384  isoso  5385  f1oiso  5386  riotass2  5414  riotass  5415  eusvobj1  5419  f1ofveu  5420  acexmidlemab  5426  acexmidlemcase  5427  acexmidlem1  5428  acexmidlem2  5429  oveq1d  5447  oveq2d  5448  oveqd  5449  ovprc1  5460  ovprc2  5461  brabvv  5470  ssoprab2  5480  fnoprabg  5521  mpt22eqb  5529  ralrnmpt2  5534  rexrnmpt2  5535  ovmpt2dxf  5545  ovmpt2df  5551  ovi3  5556  ovg  5558  ovres  5559  ovconst2  5571  f1ocnvd  5621  f1ocnv2d  5623  f1opw2  5625  f1opw  5626  suppssfv  5627  suppssov1  5628  offval  5638  ofrfval  5639  ofrval  5641  off  5643  offval2  5645  ofrfval2  5646  suppssof1  5647  ofco  5648  offveqb  5649  caofref  5651  caofinvl  5652  caofrss  5654  caoftrn  5655  cofunexg  5657  cofunex2g  5658  fnexALT  5659  fornex  5661  f1dmex  5662  abrexexg  5664  iunexg  5665  oprabexd  5673  offres  5681  ofmresex  5683  1stexg  5713  2ndexg  5714  op1steq  5724  1st2nd  5726  1stdm  5727  releldm2  5730  sbcopeq1a  5732  csbopeq1a  5733  dfoprab3  5736  eloprabi  5741  mpt2fvex  5748  mpt2exg  5753  fmpt2co  5756  1stconst  5761  2ndconst  5762  f2ndf  5766  fo2ndf  5767  f1o2ndf1  5768  mpt2xopn0yelv  5772  tposss  5779  tposeq  5780  tposeqd  5781  brtpos2  5784  brtposg  5787  tposexg  5791  dftpos4  5796  tposfo2  5800  tposf2  5801  tposf12  5802  2pwuninelg  5816  iunon  5817  issmo2  5822  smoeq  5823  smores  5825  smores2  5827  smodm2  5828  smoiso  5835  tfrlem1  5841  tfrlem5  5848  tfrlem6  5850  tfrlem8  5852  tfrlem9  5853  tfrlemisucaccv  5856  tfrlemibfn  5859  tfrlemiubacc  5861  tfrlemiex  5862  tfrlemi14  5865  tfrexlem  5866  tfri2d  5868  tfri3  5871  rdgeq1  5875  rdgeq2  5876  rdgruledefgg  5878  rdgivallem  5884  rdgss  5886  rdgisuc1  5887  frectfr  5896  frecfnom  5897  frecsuclem1  5899  frecsuclemdm  5900  frecsuclem2  5901  frecsuclem3  5902  frecrdg  5904  2oconcl  5933  sucinc2  5937  omfnex  5940  omv  5946  oeiv  5947  oeicl  5953  oav2  5954  oasuc  5955  oa1suc  5958  oawordi  5960  nna0  5964  nnm0  5965  nnacom  5974  nnaass  5975  nndi  5976  nnmass  5977  nnmsucr  5978  nnsucelsuc  5981  nnsucsssuc  5982  nntri3or  5983  nntri1  5985  nndceq  5986  nndcel  5987  nnaordi  5988  nnaord  5989  nnaword  5991  nnaordex  6007  nnm00  6009  ecexr  6018  ercl  6024  ersym  6025  ertr  6028  erref  6033  erssxp  6036  iserd  6039  brdifun  6040  swoer  6041  swoord1  6042  eceq1d  6049  ecss  6054  ereldm  6056  erth  6057  ecelqsg  6066  ecopqsi  6068  uniqs  6071  uniqs2  6073  elqsn0  6082  xpiderm  6084  iinerm  6085  riinerm  6086  ecinxp  6088  ecoptocl  6100  erovlem  6105  eroprf  6106  ecopovsym  6109  ecopover  6111  ecopovsymg  6112  ecopoverg  6114  th3qlem2  6116  th3q  6118  pion  6164  piord  6165  elni2  6168  addpiord  6170  mulpiord  6171  mulidpi  6172  ltsopi  6174  mulclpi  6182  addnidpig  6190  dfplpq2  6207  addcmpblnq  6220  mulcmpblnq  6221  dmaddpqlem  6230  nqpi  6231  dmaddpq  6232  dmmulpq  6233  mulcanenq  6238  distrnqg  6240  recex  6243  ltdcnq  6250  ltexnqq  6260  halfnq  6262  nsmallnqq  6263  nsmallnq  6264  subhalfnqq  6265  ltbtwnnqq  6266  archnqq  6268  prarloclemarch  6269  prarloclemarch2  6270  ltrnqg  6271  ltrnqi  6272  enq0sym  6281  enq0ref  6282  enq0tr  6283  nqnq0pi  6287  nqnq0  6290  nq0nn  6291  addcmpblnq0  6292  mulcmpblnq0  6293  mulcanenq0ec  6294  addnq0mo  6296  mulnq0mo  6297  addnnnq0  6298  mulnnnq0  6299  nqpnq0nq  6302  nqnq0a  6303  nqnq0m  6304  nq0m0r  6305  nq0a0  6306  distrnq0  6308  addassnq0  6311  nq02m  6313  preqlu  6320  elinp  6322  prop  6323  prnmaddl  6338  prarloclemlt  6341  prarloclemlo  6342  prarloclem3  6345  prarloclemn  6347  prarloclem5  6348  prarloclemcalc  6350  prarloc  6351  genpml  6366  genpmu  6367  genprndl  6370  genprndu  6371  genpdisj  6372  genpassl  6373  genpassu  6374  addnqprllem  6376  addnqprulem  6377  addnqprl  6378  addnqpru  6379  addlocprlemlt  6380  addlocprlemeqgt  6381  addlocprlemeq  6382  addlocprlemgt  6383  addlocprlem  6384  nqprm  6391  nqprloc  6394  appdivnq  6401  appdiv0nq  6402  prmuloclemcalc  6403  mulnqprl  6406  mulnqpru  6407  mullocprlem  6408  mullocpr  6409  ltprordil  6422  1idprl  6423  1idpru  6424  ltaddpr  6428  ltexprlemm  6431  ltexprlemlol  6433  ltexprlemopu  6434  ltexprlemupu  6435  ltexprlemdisj  6437  ltexprlemloc  6438  ltexprlemfl  6440  ltexprlemrl  6441  ltexprlemfu  6442  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  recexprlemell  6450  recexprlemelu  6451  recexprlemm  6452  recexprlemdisj  6458  recexprlemloc  6459  recexprlem1ssl  6461  recexprlem1ssu  6462  recexprlemss1l  6463  recexprlemss1u  6464  addcmpblnr  6480  addsrmo  6484  mulsrmo  6485  addsrpr  6486  mulsrpr  6487  recexsrlem  6514  addgt0sr  6515  elreal2  6536  mulresr  6543  addcnsrec  6547  mulcnsrec  6548  axaddcl  6554  axmulcl  6556  axrnegex  6567  mulid1  6620  mulid1d  6640  mulid2d  6641  recnd  6649  renepnfd  6671  renemnfd  6672  xrlenlt  6679  ltxrlt  6680  ltnrd  6718  readdcan  6740  addid1d  6749  addid2d  6750  cnegexlem3  6775  cnegex  6776  addcan  6778  addcan2  6779  subval  6790  negeqd  6793  subcl  6797  negcld  6895  subidd  6896  subid1d  6897  negidd  6898  negnegd  6899  negeq0d  6900  negrebd  6907  renegcld  6964  mul02lem2  6971  mul02d  6975  mul01d  6976  mulm1d  6993  lt0ne0d  7086  leidd  7087  lt0neg1d  7088  lt0neg2d  7089  le0neg1d  7090  le0neg2d  7091  elabgft1  7163  bj-rspgt  7171  bj-nalset  7257  bj-inex  7269  bj-sels  7276  bj-unexg  7283  peano5set  7301  speano5  7305  findset  7306  bj-bdfindisg  7309  bj-nn0suc  7321  bj-inf2vnlem1  7327  bj-inf2vn  7331  bj-inf2vn2  7332  bj-findis  7336  bj-findisg  7337
  Copyright terms: Public domain W3C validator