Theorem 3syl 20

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 10	. 2 |- (ph -> ch)
4		3syl.3	. 2 |- (ch -> th)
5	3, 4	syl 10	1 |- (ph -> th)

Syntax hints:   -> wi 3

This theorem is referenced by:  nicodrawOLD 966  nic-ax 975  ax5o 1015  ax67to6 1062  ax467 1064  ax467to6 1066  19.9d 1078  hbs1f 1231  aev 1250  hbsb4 1290  dvelimdf 1293  sbcom 1300  a12stdy3 1416  mo 1435  eupickb 1478  euor2 1480  2mo 1490  2eu2 1493  hbabd 1514  rgen2a 1746  hbsbc1gd 2033  hbsbcgd 2034  npss0 2361  iununi 2671  opthwiener 2863  elpwunsn 2969  onin 3035  ssorduni 3050  onelss 3057  onssneli 3158  onuninsuci 3165  limsuc 3177  xpexg 3316  dmsnop 3385  dmexg 3415  rnexg 3416  relfld 3572  unixp0 3575  fununi 3620  resfunexg 3636  fn0 3662  fssxp 3694  fabexg 3710  foima 3733  f1imacnv 3762  f1ococnv2 3765  f1dmex 3767  fo00 3772  fvres 3791  cbvfo 3943  isomin 3957  isoini 3958  isofrlem 3959  isowe 3961  canth 3965  tfrlem10 3978  tfrlem11 3979  tfrlem13 3981  tz7.44-2 3987  tz7.44-3 3988  rdglem2 3996  hboprd 4040  1stcof 4159  eloprabi 4176  omv 4209  oev 4211  oe1m 4237  oaord 4239  oawordeulem 4246  oalimcl 4252  oarec 4254  om00 4264  oen0 4271  oelim2 4280  nnacom 4291  oaabs 4310  qsexg 4354  eceqopreq 4374  map0 4405  f1imaen 4483  en1 4487  xpdom3 4508  sbthlem1 4510  sbthlem2 4511  sbth 4520  mapenlem2 4555  phplem4 4576  php3 4580  php4 4581  0sdom1dom 4589  ssnnfi 4600  unblem1 4603  unfilem1 4611  unifi 4618  fiint 4620  fodomfi 4626  pwfi 4631  inf3lem7 4681  tz9.12lem3 4723  r1val3 4741  rankxplim2 4775  rankxplim3 4776  rankxpsuc 4777  scott0 4779  aceq5lem4 4800  ac6lem 4816  numthlem 4845  numth 4846  zorn2lem2 4851  zorn2lem7 4856  fodom 4860  brdom3 4863  brdom5 4864  brdom4 4865  oncard 4892  sucdom 4907  unxpdomlem 4908  sucxpdom 4911  cardlim 4916  ondomon 4921  carduni 4923  cardaleph 4950  iscard3 4953  alephfp 4965  dominf 4969  cdadom2 4999  nd3 5005  mulidpi 5079  ltsopi 5081  mulcanpi 5092  enqeceq 5112  addclpq 5123  mulclpq 5125  1qec 5133  ltapq 5141  halfpq 5147  prnmadd 5165  addclprlem2 5184  1idpr 5198  prlem934a 5202  prlem934 5204  ltaddpr 5205  ltexprlem3 5209  ltexprlem4 5210  ltexprlem6 5212  prlem936a 5218  prlem936 5220  reclem1pr 5221  suplem2pr 5227  enreceq 5242  addclsr 5257  mulclsr 5258  suppsr 5287  suppsr2 5288  supsrlem2 5291  ltpnf 5607  mnflt 5608  ledivp1i 5966  ltdivp1i 5967  nnleltp1 6015  lbcl 6128  lbinfm 6130  infmrcl 6151  supxr 6163  supxrre1 6175  supxrre2 6176  nn0ltp1le 6209  zeo 6284  uzwo3lem2 6302  zbtwnre 6306  zq 6312  qbtwnre 6331  flhalf 6358  ceicl 6359  ceim1l 6361  ceile 6362  icoshftf1oii 6435  peano2uzr 6474  eluzfz2 6515  elfzp1 6536  fzneuz 6544  om2uzlti 6556  om2uzf1oi 6559  uzrdgsuci 6563  seq1val 6571  seq1seq02 6632  seqzp1 6637  seq0p1 6640  sumsqne0i 6723  discrlem2 6747  discrlem3 6748  nnesqi 6752  sqrlem12 6774  recj 6908  absdivzi 6949  releabs 6976  cjdivi 6978  seq1bndi 7000  facwordi 7034  faclbnd 7035  faclbnd2 7036  faclbnd4lem3 7040  faclbnd6 7044  facavg 7045  bccmpl 7052  bcpasci 7059  fsum1i 7095  fsump1i 7096  fsum3 7114  fsum4 7115  fsumrev 7119  fsum0 7129  ser1ser0i 7138  binomlem1 7156  binomlem2 7157  binomlem3 7158  binomlem4 7159  binomlem5 7160  bcxmas 7166  climunii 7188  climshfti 7194  climrecl 7200  climge0 7202  climaddlem3 7206  climcmplem 7227  climabslem 7238  climcji 7240  climsupi 7245  arisumilem 7315  arisumi 7316  cvgratlem2ALT 7338  cvgratlem4 7343  abscncflem 7364  cjcncf 7368  dsupivthlem 7381  efcltlem1 7394  efaddlem2 7429  efaddlem5 7432  efaddlem6 7433  efaddlem13 7440  efaddlem14 7441  efaddlem16 7443  efaddlem17 7444  efne0 7459  eftabsi 7465  ef01tllem2 7474  ef01tllem2OLD 7475  eirrlem2 7480  efgt0i 7495  absefm1lei 7503  efcnlem4 7513  efcn 7514  sincl 7522  coscl 7523  sin01bndlem2 7560  cos01bndlem2 7562  sin02gt0 7570  absef 7575  demoivre 7576  znnen 7594  infxpidmlem11 7654  infdif 7660  infxp 7664  infmap1 7665  infmap2 7673  alephexp2 7678  tgval 7705  cctop 7737  ntrfval 7752  clsfval 7753  neifval 7799  lpfval 7827  cnpfval 7842  cnpco 7854  iscncl 7855  ismet 7883  dfms2 7884  meteq0 7897  metne0 7906  metres 7908  blfval 7920  metcnss 7983  metcnss2 7984  lmfval 8010  caufval 8011  caun0 8030  lmle 8045  bcthlem33 8116  grpidval 8142  grpinvval 8151  resgrprn 8179  issubg 8200  subgres 8201  ringid 8229  ring2 8233  nvgf 8321  nvs 8374  nvz 8381  imsba 8405  ipcl 8449  ip1cnilem1 8457  ip1cnilem2 8458  ip1cnilem3 8459  ip1cnilem4 8460  ip1cnilem5 8461  sspba 8470  sspg 8471  ssps 8473  sspmlem 8475  sspn 8479  sspival 8481  nmogtmnf 8517  nmblore 8530  0oo 8533  phop 8561  cnph 8562  pilem1 8754  sinperlem2 8770  sinmpi 8777  cosmpi 8778  sinppi 8779  sincosq2sgn 8788  sincosq3sgn 8789  sincosq4sgn 8790  sinq12gt0t 8791  cosh111lem1 8797  efif 8804  efifolem6 8810  efif1lem3 8815  efif1lem4 8816  efielcirc 8822  eff1i 8827  effoi 8828  efper 8830  hhph 9128  hlimuniii 9191  occllem6 9261  projlem1 9269  projlem8 9276  projlem10 9278  projlem12 9280  projlem13 9281  projlem15 9283  projlem24 9292  projlem25 9293  projlem26 9294  pjthlem2 9303  pjthlem7 9308  pjthlem8 9309  dfch2 9332  ococin 9380  spanssoc 9402  spansnch 9566  osumlem3 9663  osumlem5 9665  5oalem5 9686  pjige0i 9718  pjocini 9726  eigrei 9843  nmopgtmnf 9878  nmopre 9880  nmopge0 9918  unopadj 9926  unoplin 9927  nmfnge0 9934  adjadj 9943  unopadj2 9945  eigvalcl 9968  hmopidmchlem 10161  pjssposi 10183  pjclem4 10211  pj2cocli 10217  pj3si 10219  hstles 10242  strlem1 10261  strlem3a 10263  strlem5 10266  hstrlem6 10275  dmdbr5 10319  h1da 10360  atom1d 10364  shatomistici 10372  atomli 10393  mdsymlem1 10414  mdsymlem3 10416  mdsymi 10422  sumdmdlem 10429  dmdbr5ati 10433  ghomfo 10476  ghomcl 10477  cayleylem2 10495  cayleylem3 10496  f2imacnv 10555  twpar2 10567  inposet 10578  vri 10583  mapdiscn 10605  cmphmp 10615  idhme 10616  hmeogrp 10632  qusp 10649  fgsb 10663  rcfpfillem3 10673  sfvlim 10684  sfvlimOLD 10685  limfillem2OLD 10687  dtt2 10697  mslb1 10711  2wsms 10712  msra3 10713  iintlem1 10714  isalg 10735  algi 10742  rdmob 10763  rcmob 10764  domc 10780  codc 10781  idc 10782  cmppfc 10783  cmpmorp 10794  mrdmcd 10804  eqidob 10805  homib 10806  ismonc 10824  isepic 10834  idfisf 10844  hgrablkne0 10857

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

Copyright terms: Public domain