Theorem 3syl 24

Description: Inference chaining two syllogisms.

Hypotheses

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

Assertion

Ref	Expression
3syl	|- (ph -> th)

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- (ph -> ps)
2		3syl.2	. . 3 |- (ps -> ch)
3	1, 2	syl 12	. 2 |- (ph -> ch)
4		3syl.3	. 2 |- (ch -> th)
5	3, 4	syl 12	1 |- (ph -> th)

Syntax hints:   -> wi 3

This theorem is referenced by:  nic-ax 1239  ax5o 1320  ax67to6 1368  ax467 1370  ax467to6 1372  19.9d 1384  hbs1fOLD 1556  aev 1577  aevOLD 1578  hbsb4 1620  dvelimdf 1624  sbcom 1632  cbvald 1702  a12stdy3 1765  mo 1787  eupickb 1836  euor2OLD 1840  2mo 1851  2eu2 1854  hbabd 1876  rgen2aOLD 2161  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  npss0OLD 2912  iununi 3331  iununiOLD 3332  opthwiener 3554  onin 3690  onelssOLD 3706  onssneli 3779  euexeqOLD 3826  euexaleq 3827  elpwunsn 3856  ssorduniOLD 3871  onsucuni2 3914  onuninsuci 3921  limsuc 3933  ordom 3960  xpexg 4095  dmexg 4206  rnexg 4207  dmsnopOLD 4368  relfld 4419  unixp0 4423  fununi 4481  resfunexg 4500  fn0OLD 4533  fssxp 4575  fssxpOLD 4576  fabexg 4596  foima 4622  f1imacnv 4656  foimacnv 4657  f1ococnv2 4662  f1dmex 4664  fvres 4691  dffv2 4734  cbvfo 4861  isomin 4876  isoini 4877  isofrlem 4878  isowe 4880  hboprdOLD 4906  1stcof 5040  eloprabi 5060  canth 5112  tfrlem10 5128  tfrlem11 5129  tfrlem13 5131  tz7.44-2 5137  tz7.44-3 5138  rdglem2 5146  omv 5196  oev 5198  oe1m 5226  oaord 5228  oawordeulem 5236  oalimcl 5242  oarec 5244  om00 5254  oen0 5261  oelim2 5270  nnacom 5288  oaabs 5309  qsexg 5352  eceqopreq 5372  map0 5403  f1imaen 5481  en1 5485  xpdom3 5504  ac6sfilem2 5507  ac6sfi 5509  sbthlem1 5510  sbthlem2 5511  sbth 5520  mapenlem2 5584  phplem4 5605  php3 5609  php4 5610  0sdom1dom 5618  ssnnfi 5629  unblem1 5633  unfilem1 5641  unifi 5648  fiint 5650  fodomfi 5656  pwfi 5661  ordiso 5683  ordtypelem2 5685  hartoglem 5692  hartog 5693  onsdom 5694  inf3lem7 5725  tz9.12lem3 5772  r1val3 5790  rankxplim2 5824  rankxplim3 5825  rankxpsuc 5826  scott0 5847  aceq5lem4 5900  ac6lem 5916  numthlem 5945  numth 5946  zorn2lem2 5951  zorn2lem7 5956  fodom 5960  brdom3 5963  brdom5 5964  brdom4 5965  oncard 5978  ficardom 5979  sucdom 5994  unxpdomlem 5995  sucxpdom 5998  cardlim 6003  ondomon 6008  carduni 6010  cardaleph 6033  iscard3 6036  alephfp 6048  dominf 6052  cdadom2 6084  nnacda 6088  nd3 6092  mulidpi 6166  ltsopi 6168  mulcanpi 6179  enqeceq 6199  addclpq 6210  mulclpq 6212  1qec 6220  ltapq 6228  halfpq 6234  prnmadd 6252  addclprlem2 6271  1idpr 6285  prlem934a 6289  prlem934 6291  ltaddpr 6292  ltexprlem3 6296  ltexprlem4 6297  ltexprlem6 6299  prlem936a 6305  prlem936 6307  reclem1pr 6308  suplem2pr 6314  enreceq 6329  addclsr 6344  mulclsr 6345  suppsr 6374  suppsr2 6375  supsrlem2 6378  ltpnf 6717  mnflt 6718  ledivp1i 7089  ltdivp1i 7090  nnleltp1 7138  lbcl 7255  lbinfm 7257  infmrcl 7278  supxr 7290  supxrre1 7302  supxrre2 7303  nn0ltp1le 7336  zeo 7411  uzwo3lem2 7430  zbtwnre 7434  zq 7440  qbtwnre 7459  flhalf 7487  ceicl 7488  ceim1l 7490  ceile 7491  icoshftf1oii 7578  peano2uzr 7617  eluzfz2 7659  elfzp1 7683  fzneuz 7697  om2uzlti 7709  om2uzf1oi 7712  uzrdgsuci 7716  seq1val 7725  seq1seq02 7786  seqzp1 7791  seq0p1 7794  sumsqne0i 7879  discrlem2 7907  discrlem3 7908  nnesqi 7912  nn0opthlem2 7915  sqrlem12 7934  recj 8068  releabs 8138  cjdivi 8140  seq1bndi 8162  facwordi 8196  faclbnd 8197  faclbnd2 8198  faclbnd4lem3 8202  faclbnd6 8206  facavg 8207  bccmpl 8214  bcpasci 8221  fsum1i 8265  fsump1i 8266  fsum3 8284  fsum4 8285  fsumrev 8289  fsum0 8299  ser1ser0i 8308  binomlem1 8326  binomlem2 8327  binomlem3 8328  binomlem4 8329  binomlem5 8330  bcxmas 8336  climunii 8358  climshfti 8364  climrecl 8370  climge0 8372  climaddlem3 8376  climcmplem 8397  climabslem 8408  climcji 8410  climsupi 8415  arisumilem 8486  arisumi 8487  cvgratlem4 8515  abscncflem 8536  cjcncf 8540  dsupivthlem 8553  efcltlem1 8566  efaddlem2 8601  efaddlem6 8605  efaddlem13 8612  efaddlem14 8613  efaddlem16 8615  efaddlem17 8616  efne0 8631  eftabsi 8637  ef01tllem2 8646  ef01tllem2OLD 8647  eirrlem2 8652  efgt0i 8669  absefm1lei 8677  efcnlem4 8687  efcn 8688  sincl 8696  coscl 8697  sin01bndlem2 8734  cos01bndlem2 8736  sin02gt0 8744  absef 8749  demoivre 8752  znnen 8771  infxpidmlem11 8831  infdif 8837  infxp 8841  infmap1 8842  infmap2 8850  alephexp2 8855  tgval 8886  cctop 8922  ntrfval 8943  clsfval 8944  neifval 8990  lpfval 9018  cnpfval 9033  cnpco 9046  iscncl 9047  ismet 9075  dfms2 9076  meteq0 9089  metn0 9098  metres 9100  blfval 9112  metcnss 9176  metcnss2 9177  lmfval 9203  caufval 9204  caun0 9223  lmle 9238  bcthlem33 9309  grpinvval 9351  gxneg 9389  gxsuc 9395  resgrprn 9403  issubg 9425  subgres 9426  isgalem 9449  isga 9450  gaid 9454  ssga 9455  gagrpid 9458  ringid 9469  ring2 9474  nvgf 9569  nvs 9622  nvz 9629  imsba 9653  vacnlem3 9669  vacnlem6 9672  ipcl 9704  ip1cnilem1 9712  ip1cnilem2 9713  ip1cnilem3 9714  ip1cnilem4 9715  ip1cnilem5 9716  sspba 9725  sspg 9726  ssps 9728  sspmlem 9730  sspn 9734  sspival 9736  nmogtmnf 9772  nmounbseqi 9779  nmblore 9786  0oo 9789  phop 9818  cnph 9819  pilem1 10020  sinperlem2 10036  sinmpi 10043  cosmpi 10044  sinppi 10045  cosppi 10046  sincosq2sgn 10054  sincosq3sgn 10055  sincosq4sgn 10056  sinq12gt0t 10057  sinkpi 10063  cosh111lem1 10068  efif 10075  efifolem6 10081  efif1lem3 10086  efif1lem4 10087  efielcirc 10093  effoi 10099  efper 10101  grothpw 10134  grothpwex 10135  twpar2 10149  dif1enOLD 10173  indexfi 10174  tx1cn 10223  tx2cn 10224  uptx 10226  subtopmet 10256  fbssint 10279  fgf 10283  filrn 10293  sfvlim 10296  elfilmap 10312  idrval 10374  ismnd2 10392  rnplrnml0 10402  ringidmlem 10409  on1el3 10412  hhph 10678  hlimuniii 10741  occllem6 10811  projlem1 10819  projlem8 10826  projlem10 10828  projlem12 10830  projlem13 10831  projlem15 10833  projlem24 10842  projlem25 10843  projlem26 10844  pjthlem2 10853  pjthlem7 10858  pjthlem8 10859  dfch2 10882  ococin 10930  spanssoc 10952  spansnch 11116  osumlem3 11215  osumlem5 11217  5oalem5 11238  pjige0i 11270  pjocini 11278  eigrei 11397  nmopgtmnf 11432  nmopre 11434  nmopge0 11472  unopadj 11480  unoplin 11481  nmfnge0 11488  adjadj 11497  unopadj2 11499  eigvalcl 11522  opsqrlem3 11713  opsqrlem6 11716  hmopidmchlem 11722  pjssposi 11744  pjclem4 11772  pj2cocli 11778  pj3si 11780  hstles 11803  strlem1 11822  strlem3a 11824  strlem5 11827  hstrlem6 11836  dmdbr5 11880  h1da 11921  atom1d 11925  shatomistici 11933  atomli 11954  mdsymlem1 11975  mdsymlem3 11977  mdsymi 11983  sumdmdlem 11990  dmdbr5ati 11994  bnj214 12508  bnj512 12519  bnj529 12535  bnj566 12544  bnj1098 12917  bnj65 13202  bnj72 13208  bnj522 13261  bnj535 13265  bnj545 13271  bnj546 13272  bnj548 13274  bnj578 13291  bnj605 13292  bnj583 13296  bnj594 13300  bnj580 13301  bnj607 13304  bnj849 13318  bnj900 13325  bnj916 13332  bnj944 13340  bnj966 13348  bnj967 13349  bnj1001 13366  bnj1018 13378  bnj1053 13396  bnj1071 13402  bnj1118 13420  bnj1171 13439  bnj1172 13440  bnj1321 13498  bnj1412 13522  bnj1408 13524  bnj1450 13541  ghomfo 13634  ghomcl 13635  cayleylem2 13642  nn0seqcvgd 13659  alzdvds 13695  divalglem4 13699  gcdcllem1 13718  algfx 13748  eucalg 13755  mulgcdlem2 13757  mulgcdlem7 13762  1idssfct 13770  trcleq3 13928  wfrlem5 13961  axfelem2 14032  axfelem10 14040  axfelem15 14045  altopeq2 14088  altxpexg 14101  naim1 14134  naim2 14135  nabi1 14139  nabi2 14140  merco2 14203  meran1 14235  lukshef-ax2 14239  arg-ax 14240  nandsym1 14246  f2imacnv 14355  f1ofi 14376  njtlc 14389  resrelfld 14448  fldrels 14449  surjsec 14462  inpreima2 14468  mapmapmap 14486  injsurinj 14487  repfuntw 14502  prl2 14514  prjmapcp2 14515  islatalg 14531  domrancur1c 14550  sege 14595  mxlmnl2 14612  defse3 14614  inposet 14620  dutos1 14626  istoset2 14628  fprod1i 14673  fprodp1i 14674  resgcom 14712  ltlga 14729  symgfo 14730  rngapm 14733  curgrpact 14735  fprodneg 14741  rnplrnml3 14768  rnginvcl 14770  zerdivemp1 14785  zintdom 14787  vecval1b 14794  vec2inv 14804  sum2vv 14805  addnull2 14807  addvecass 14808  invaddvec 14810  vecsrcan 14812  vecslcan 14813  vecrcan 14818  veclcan 14819  svli2 14826  svs2 14829  vri 14834  mapdiscnlem 14870  osneisi 14875  cmphmp 14878  idhme 14879  hmeogrp 14892  qusp 14908  intcont 14914  usptoplem 14917  prtoptop 14919  fgsb 14921  rcfpfillem3 14930  limfilnei 14943  dtt2 14951  stfincomp 14959  topgrpsubcnlem 14981  trhom 14983  cntrsetlem 14999  msr4 15004  mslb1 15007  2wsms 15008  msra3 15009  iintlem1 15010  lvsovso 15038  lvsovso2 15039  supnuf 15041  isalg 15068  algi 15074  rdmob 15095  rcmob 15096  domc 15112  codc 15113  idc 15114  cmppfc 15115  cmpmorp 15126  dualded 15132  dualcat2 15133  mrdmcd 15143  eqidob 15144  homib 15145  ismonc 15163  isepic 15173  idfisf 15189  idsubidsup 15205  cptarc 15242  sexptrt 15243  partarelt2 15274  eltintpar 15276  inttaror 15277  fnctartar 15284  fnctartar2 15285  trer 15361  finminlem 15367  inficlALT 15372  finsschain 15373  ordisoOLD 15374  ordtypelem2OLD 15376  hartoglemOLD 15383  hartogOLD 15384  onsdomOLD 15385  opncldf3 15404  cncls 15419  cnntr 15420  cnsubsp 15426  cptclsscpt 15432  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  cnconn 15444  reconnlem3 15448  reconnlem4 15449  ivthALT 15454  locfincomp 15514  topjoin 15527  fnejoin1 15530  isufil2 15565  ufileulem 15572  ufileu 15573  filufint 15574  uffixfr 15575  ufinffr 15578  filcon 15580  flimcls 15588  rnelfmlem 15592  fmfnfmlem3 15596  sfcls 15604  filclus 15605  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscomplem 15620  fcluscomp 15621  isfclusf 15625  tailf 15633  tailmap 15636  tailfb 15639  filnetlem4 15643  filnetlem5 15644  filnet 15645  difxp 15690  cocnv 15716  f1ocan2fv 15718  eropreu 15733  findcard2 15745  indexfiOLD 15755  welb 15759  fisup2g 15768  rdr 15781  uzp1 15785  fzfi 15786  absrdbnd 15799  negmod0 15801  sdc 15811  fdc 15812  seqpo 15814  incsequz 15815  incsequz2 15816  seq1eq2 15817  fsum00 15820  fsumltisumii 15822  fsumleisumii 15825  fsumlt1 15831  mettrifi 15847  mettrifi2 15848  lmclim2 15850  caushft 15851  iccst 15875  cnimass 15888  cnres 15889  hmeocld 15900  sstotbnd 15936  ismtyhmeolem 15950  heiborlem1 15955  heiborlem8 15962  heiborlem11 15965  heiborlem12 15966  heiborlem16 15970  heiborlem23 15977  heiborlem27 15981  heiborlem28 15982  heiborlem30 15984  heiborlem32 15986  heiborlem33 15987  heiborlem35 15989  heiborlem36 15990  heiborlem38 15992  heiborlem41 15995  bfplem9 16006  recms 16010  rrnmet 16016  rrndstprj1 16017  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  iccbnd 16026  exidreslem 16030  isgrpda 16033  phtpycom 16050  phtpycolem3 16053  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1f 16093  pi1gp 16095  zerdivemp1x 16108  keridl 16180  hgrablkne0 16295  ax4567 16359  ax4567to5 16361  ax4567to6 16362  ax4567to7 16363  ax10ext 16364  ax10-16 16365  euunianOLD 16396  ralbidar 16422  rexbidar 16423  smores2 16447  smoiso 16453  hlhght2 17038  divrngidlemNEW 17165  polcon3 17330

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

Copyright terms: Public domain