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:  nicodraw 949  ax5o 971  ax67to6 1017  ax467 1019  ax467to6 1021  19.9d 1033  hbs1f 1185  aev 1204  hbsb4 1243  dvelimdf 1246  sbcom 1253  a12stdy3 1367  mo 1386  eupickb 1428  euor2 1430  2mo 1440  2eu2 1443  hbabd 1461  rgen2a 1691  hbsbc1gd 1973  hbsbcgd 1974  npss0 2299  iununi 2606  opthwiener 2796  elpwunsn 2902  onin 2968  ssorduni 2983  onelsst 2990  onssneli 3091  onuninsuc 3098  limsuc 3110  xpexg 3249  dmsnop 3317  dmexg 3344  rnexg 3345  relfld 3501  unixp0 3504  fununi 3549  resfunexg 3565  fn0 3591  fssxp 3622  fabexg 3638  foima 3661  f1imacnv 3690  f1ococnv2 3693  f1dmex 3695  fo00 3700  fvres 3719  cbvfo 3870  isomin 3884  isoini 3885  isofrlem 3886  isowe 3888  canth 3892  tfrlem10 3905  tfrlem11 3906  tfrlem13 3908  tz7.44-2 3914  tz7.44-3 3915  rdglem2 3923  hboprd 3967  1stcof 4085  eloprabi 4102  omv 4135  oev 4137  oe1m 4163  oaord 4165  oawordeulem 4172  oalimcl 4178  oarec 4180  om00 4190  oen0 4197  oelim2 4206  nnacom 4217  oaabs 4236  qsexg 4278  eceqopreq 4297  map0 4328  f1imaen 4403  en1 4407  xpdom3 4425  sbthlem1 4427  sbthlem2 4428  sbth 4437  2pwuninel 4465  mapenlem2 4470  phplem4 4491  php3 4495  php4 4496  0sdom1dom 4504  ssnn 4514  unblem1 4517  unfilem1 4524  unifi 4532  fiint 4534  fodomfi 4540  inf3lem7 4591  tz9.12lem3 4633  r1val3 4651  rankxplim2 4685  rankxplim3 4686  rankxpsuc 4687  scott0 4689  aceq5lem4 4710  ac6lem 4726  numthlem 4755  numth 4756  zorn2lem2 4761  zorn2lem7 4766  fodom 4770  brdom3 4773  brdom5 4774  brdom4 4775  oncard 4801  sucdom 4814  unxpdomlem 4815  sucxpdom 4818  cardlim 4823  ondomon 4828  carduni 4830  cardaleph 4857  iscard3 4860  alephfp 4872  dominf 4876  cdadom2 4906  nd3 4912  mulidpi 4986  ltsopi 4988  mulcanpi 4999  enqeceq 5019  addclpq 5030  mulclpq 5032  1qec 5040  ltapq 5048  halfpq 5054  prnmadd 5072  addclprlem2 5091  1idpr 5105  prlem934a 5109  prlem934 5111  ltaddpr 5112  ltexprlem3 5116  ltexprlem4 5117  ltexprlem6 5119  prlem936a 5125  prlem936 5127  reclem1pr 5128  suplem2pr 5134  enreceq 5149  addclsr 5164  mulclsr 5165  suppsr 5194  suppsr2 5195  supsrlem2 5198  ltpnft 5515  mnfltt 5516  ledivp1 5854  ltdivp1 5855  nnleltp1t 5901  lbcl 5993  lbinfm 5995  infmrcl 6016  supxr 6028  supxrre1 6040  supxrre2 6041  nn0ltp1let 6074  zeot 6146  uzwo3lem2 6165  zbtwnre 6169  flget 6178  flidt 6180  fladdzt 6187  flhalft 6189  ceiclt 6190  ceiget 6191  ceim1lt 6192  ceilet 6193  zqt 6198  qbtwnre 6216  om2uzlt 6235  om2uzf1o 6238  uzrdgsuc 6241  seq1val 6249  icoshftf1oi 6342  peano2uzr 6380  eluzfz2t 6421  elfzp1 6442  fzneuzt 6450  seq1seq02t 6475  seqzp1 6480  seq0p1 6483  sumsqne0 6565  discrlem2 6587  discrlem3 6588  nnesq 6592  sqrlem12 6614  recjt 6753  absdivz 6794  releabst 6824  cjdiv 6826  seq1bnd 6847  facwordit 6881  faclbnd 6882  faclbnd2 6883  faclbnd4lem3 6887  faclbnd6 6891  facavgt 6892  bccmplt 6900  bcpasc 6907  fsum1 6943  fsump1 6944  fsum3 6962  fsum4 6963  fsumrev 6967  fsum0 6977  ser1ser0 6986  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem5 7008  bcxmas 7014  climunii 7035  climshft 7041  climrecl 7047  climge0 7049  climaddlem3 7052  climcmplem 7073  climabslem 7084  climcj 7086  climsup 7091  fnsmntlem 7160  fnsmnt 7161  cvgratlem2ALT 7183  cvgratlem4 7188  abscncflem 7209  cjcncf 7213  dsupivthlem 7226  efcltlem1 7246  efaddlem2 7281  efaddlem5 7284  efaddlem6 7285  efaddlem13 7292  efaddlem14 7293  efaddlem16 7295  efaddlem17 7296  efne0t 7311  eftabs 7317  ef01tllem2 7326  eirrlem2 7331  efgt0 7345  absefm1le 7352  efcnlem4 7362  efcn 7363  sinclt 7373  cosclt 7374  sin01bndlem2 7410  cos01bndlem2 7412  sin02gt0 7420  abseft 7425  demoivre 7426  znnen 7445  infxpidmlem11 7505  infdif 7511  infxp 7515  infmap1 7516  infmap2 7523  alephexp2 7528  tgvalt 7558  cctop 7594  ntrfval 7609  clsfval 7610  neifval 7655  lpfval 7683  cnpfval 7697  cnpco 7708  iscncl 7709  ismet 7737  dfms2 7738  meteq0 7751  metres 7763  blfval 7775  metcnss 7837  metcnss2 7838  lmfval 7863  caufval 7864  caun0 7880  lmle 7895  bcthlem33 7965  grpidval 7992  grpinvval 8001  resgrprn 8030  resgrprnOLD 8031  issubg 8053  subgres 8054  ringid 8082  ring2 8086  nvgf 8177  nvs 8229  nvz 8236  imsba 8259  ipcl 8299  ip1cnilem1 8307  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem4 8310  ip1cnilem5 8311  sspba 8320  sspg 8321  ssps 8323  sspmlem 8325  sspn 8329  sspival 8331  nmogtmnf 8365  nmblore 8378  0oo 8381  phop 8408  cnph 8409  pilem1 8590  sinperlem2 8606  sinmpi 8613  cosmpi 8614  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  sinq12gt0t 8625  cosh111lem1 8629  efif 8636  efifolem6 8642  efif1lem3 8647  efif1lem4 8648  efielcircOLD 8655  efielcirc 8659  eff1i 8665  effoi 8666  effoiOLD 8667  efper 8669  hhph 8966  hlimunii 9029  occllem6 9094  projlem1 9102  projlem8 9109  projlem10 9111  projlem12 9113  projlem13 9114  projlem15 9116  projlem24 9125  projlem25 9126  projlem26 9127  pjthlem2 9135  pjthlem7 9140  pjthlem8 9141  dfch2 9164  ococint 9212  spanssoc 9234  spansncht 9399  osumlem3 9497  osumlem5 9499  5oalem5 9520  pjige0 9552  pjocin 9560  eigre 9677  nmopgtmnf 9712  nmopret 9714  nmopge0t 9751  unopadjt 9759  unoplint 9760  nmfnge0t 9767  adjadjt 9776  unopadj2t 9778  eigvalclt 9801  hmopidmchlem 9989  pjsspos 10011  pjclem4 10037  pj2cocl 10043  pj3s 10045  hstlest 10068  strlem1 10087  strlem3a 10089  strlem5 10092  strlem6 10093  hstrlem6 10101  h1dat 10184  atom1d 10188  shatomistic 10196  atoml 10217  mdsymlem1 10238  mdsymlem3 10240  mdsym 10246  sumdmdlem 10252  dmdbr5at 10255  ghomfo 10296  ghomcl 10297  cayleylem2 10317  cayleylem3 10318  f2imacnv 10370  mapdiscn 10398  cmphmp 10408  idhme 10409  hmeogrp 10425  qusp 10430  fgsb 10444  dtt2 10462  mslb1 10473  2wsms 10474  msra3 10475  iintlem1 10476  isalg 10497  algi 10504  rdmob 10525  rcmob 10526  domc 10542  codc 10543  idc 10544  cmppfc 10545  cmpmorp 10556  mrdmcd 10566  eqidob 10567  homib 10568  ismonc 10584  hgrablkne0 10609

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

Copyright terms: Public domain