Theorem sylanc 473

Description: A syllogism inference combined with contraction.

Hypotheses

Ref	Expression
sylanc.1	|- ((ph /\ ps) -> ch)
sylanc.2	|- (th -> ph)
sylanc.3	|- (th -> ps)

Assertion

Ref	Expression
sylanc	|- (th -> ch)

Proof of Theorem sylanc

Step	Hyp	Ref	Expression
1		sylanc.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	ex 373	. 2 |- (ph -> (ps -> ch))
3		sylanc.2	. 2 |- (th -> ph)
4		sylanc.3	. 2 |- (th -> ps)
5	2, 3, 4	sylc 68	1 |- (th -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  syl2anc 474  sylancom 477  anim12d 560  orim12d 567  pm5.21ni 680  ax11indalem 1370  ax11inda2ALT 1371  eueq2 1921  eueq3 1922  sbc2or 1961  sstrd 2077  ralidm 2361  raaan 2364  sspr 2479  exss 2775  reuuniss 2895  reuuniss2 2897  reuunixfr 2912  ordelord 2976  onfr 2992  onnmin 3021  onminex 3026  onmindif2 3067  ordunel 3090  limsssuc 3127  peano5 3159  unixp 3523  cnvexg 3525  cnvpo 3528  cofunexg 3586  funfni 3594  fnresdm 3602  fnex 3613  fconstg 3665  f1ores 3709  fimacnv 3816  dff2 3823  fconst3 3856  f1ocnvfv3 3889  tfrlem10 3926  tfrlem12 3928  oprabex2g 4026  sbcopeq1a 4117  csbopeq1a 4118  dfoprab4 4122  oesuc 4172  odi 4216  oewordri 4225  oeworde 4226  oelim2 4228  en2d 4406  undom 4444  xpdom1 4449  sbthlem8 4460  2pwuninel 4493  limenpsi 4511  limensuci 4512  php3 4521  php3OLD 4522  unblem4 4554  unbnn 4555  unifiOLD 4570  fodomfi 4575  fodomfiOLD 4576  pwfilem 4577  pwfilemOLD 4578  supub 4589  suplub 4590  supmax 4598  suppr 4599  noinfep 4650  r1ord 4665  rankr1 4684  rankxplim3 4724  fodom 4808  unidom 4818  uniimadom 4820  unxpdomlem 4854  unxpdom2 4856  cardalephex 4897  alephval2 4913  alephval3 4914  cfsuc 4927  cdafi 4948  axrepnd 4958  indpi 5046  halfpq 5094  ltaddpr 5152  ltexprlem2 5155  negexsr 5223  mulgt0sr 5226  axmulopr 5278  axcnre 5298  cnegext 5360  nnncan1t 5479  mulsubt 5489  pm2.61ltle 5546  lecase 5633  posdift 5666  recextlem2 5695  recext 5696  muleqaddt 5712  divcan2t 5733  recid2t 5743  divrec2t 5747  div23t 5749  div12t 5751  divsubdirt 5776  divsubdirtOLD 5777  divcan5t 5783  divdivdivt 5787  divcan6t 5793  divdiv23t 5794  divdivmult 5797  conjmult 5799  lemul1t 5834  ltmul12it 5843  lediv1t 5853  lt2mul2divt 5874  lemuldivt 5876  lemuldivtOLD 5877  lt2msq 5883  lediv2t 5893  lediv12it 5898  lediv2it 5899  recp1lt1 5903  recrecltt 5904  ledivp1t 5907  ledivp1 5908  ltdivp1 5909  nnge1t 5945  nngt1ne1t 5946  nnrecret 5954  nndivtrt 5962  halfaddsubt 6043  lt2halvest 6044  avglet 6046  lbinfm 6050  infm3lem 6055  suprub 6058  infmrcl 6071  nnreclt 6074  xrub 6082  supxrre 6085  supxrunb1 6091  supxrbnd 6093  supxrub 6100  nn0ltp1let 6129  zltp1let 6183  z2get 6190  gtndivt 6195  flidt 6237  flval2t 6240  flval3t 6241  flbi2t 6243  fladdzt 6246  flhalft 6248  quoremz 6253  intfrac 6254  intfracq 6255  fldivt 6256  qaddclt 6270  qmulclt 6272  qbtwnxr 6280  rpne0t 6289  rpdivclt 6293  seq1lem2 6311  ser1mono 6338  shftval2t 6348  shftval5t 6351  2shft 6353  shftcan2t 6354  iooint 6373  iccsupr 6399  icoshft 6409  icoshftf1oi 6410  uznegit 6430  uzind4 6451  infmssuzcl 6467  eluzfz1t 6488  eluzfz2t 6490  fznn0sub2t 6500  fzelp1t 6509  elfzp1 6511  fzrev2it 6514  fzrev3t 6515  fzneuzt 6519  fsequb 6524  fsequb2 6525  fseqsupub 6527  seqzp1 6549  seqzfveq 6555  seqzres 6561  seqzres2 6562  expeq0t 6586  expgt0t 6590  mulexpt 6595  recexpt 6596  expaddt 6597  expsubt 6599  expordit 6601  expwordit 6604  expord2t 6605  expmwordit 6607  exple1t 6608  expubndt 6609  sqlecant 6642  subsqt 6643  bernneq 6653  expnbndt 6655  expnlbndt 6656  rpsqrclt 6716  cjclt 6765  imret 6774  reim0t 6775  cjexpt 6817  recjt 6818  imcjt 6819  cj11t 6830  absclt 6833  absvalsqt 6835  absreimt 6857  absdivz 6859  absexpt 6868  absrelet 6869  absimlet 6870  recvalz 6887  cjdiv 6888  absidmt 6892  abssubge0t 6895  abs3dift 6899  abs2difabst 6903  seq1ub 6912  cvg2 6922  caubnd 6926  ser1absdiflem 6929  ser1absdif 6930  facdivt 6942  facndivt 6943  faclbnd 6945  faclbnd2 6946  faclbnd3 6947  faclbnd4lem3 6950  faclbnd5 6953  faclbnd6 6954  facavgt 6955  bcval2t 6959  bccmplt 6962  bcn0t 6963  bcnp11t 6965  bcnp1nt 6966  bccl2t 6971  bcclt 6972  permnnt 6973  dffsum 6998  fsump1s 7013  fsumcllem 7014  fsumsplit 7020  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsumrev2 7030  fsumshft 7031  fsummulc1 7033  fsumdivcALT 7036  fsum0 7039  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  serz1p 7052  serzrelem 7061  binomlem1 7066  binomlem2 7067  binomlem4 7069  binomlem5 7070  bcxmas 7076  clm4le 7081  2climnn 7102  2climnn0 7103  climrecl 7110  climge0 7112  climaddlem3 7116  climaddc1 7118  climmullem1 7120  climmullem2 7121  climmullem3 7122  climmullem4 7123  climmullem5 7124  climmullem8 7127  climmulc2 7129  climsub 7130  climsubc2 7131  climcmplem 7137  clim2serz 7145  climserzle 7147  climcj 7150  climubi 7153  climsup 7155  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  ser1cmp 7174  ser1cmp2 7177  cvgcmp2lem 7180  cvgcmp2clem 7182  isum1p 7206  iserzgt0 7211  isummulc1ALT 7213  reccnv 7218  infcvglem1 7221  infcvglem3 7223  fnsmnt 7226  geoser 7234  georeclim 7240  geoisumr 7243  geoisum1c 7245  0.999... 7246  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem2 7251  cvgratlem4 7253  cvgratlem5 7254  fsum0diaglem1 7256  fsum0diaglem2 7257  fsum0diag2 7259  elcncf1d 7270  cjcncf 7278  ivthlem6 7286  ivthlem7 7287  efcltlem1 7304  efcltlem2 7305  ef0lem 7310  efseq0ex 7311  erelem1 7319  erelem3 7321  efaddlem3 7340  efaddlem5 7342  efaddlem6 7343  efaddlem10 7347  efaddlem15 7352  efaddlem16 7353  efaddlem17 7354  efaddlem18 7355  efaddlem19 7356  efaddlem23 7360  efaddlem25 7362  efaddlem27 7364  eff2 7370  efsubt 7371  efexpt 7372  eftabs 7375  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  eirrlem4 7392  abspef01tlub 7395  efgt1 7403  absefm1le 7412  eflegeolem1 7413  efcnlem2 7420  efcn 7423  reeff1o 7426  efi4pt 7435  resin4pt 7436  recos4pt 7437  sinnegt 7442  cosnegt 7443  efivalt 7447  efmivalt 7448  efeult 7449  sinsubt 7455  cossubt 7456  addsint 7457  subcost 7460  sincossqt 7461  sin2tt 7462  cos2tt 7463  cos2tsint 7464  sinbndt 7466  cosbndt 7467  sin01bndlem2 7469  sin01bndlem3 7470  cos01bndlem2 7471  cos01bndlem3 7472  sin01gt0 7477  cos01gt0 7478  sin02gt0 7479  absefit 7483  abseft 7484  demoivre 7485  acdc3lem 7487  acdc2lem2 7490  acdc5lem2 7493  acdclem 7495  acdcALT 7497  znnenlem 7502  unbenlem 7505  infpnlem2 7508  ruclem4 7514  ruclem13 7523  infxpidmlem1 7553  infxpidmlem11 7563  infxpidmlem12 7564  infunabs 7566  infcdaabs 7567  infcda 7568  infdif 7569  infxp 7573  alephexp1 7586  alephsuc3 7587  tgval3t 7624  topbast 7626  basgen2t 7638  ntrval 7673  clsval 7674  clsss 7684  elcls 7701  clsndisj 7703  neival 7714  neiss 7720  neips 7724  unnei 7732  lpval 7740  iscnp2 7758  cnpcl 7761  cnco 7765  cnpco 7766  iscncl 7767  cnsscnp 7769  cncnplem2 7772  cnconst 7777  metsym 7813  metge0 7816  metxplem3 7825  metxpdval 7826  metxptval 7827  metxpfval 7828  metxp 7831  bl2in 7840  blex 7846  blss 7850  blssex 7851  ssblex 7853  opnm 7857  opnin 7866  neibl 7874  lpbl 7877  methausi 7878  metcnconst 7882  metcnplem 7883  metcnp 7884  metcnpi3 7889  metcnpi4 7890  metcni2 7892  metcnp3 7893  metcnss 7895  bl2ioo 7908  ioo2bl 7909  blssioo 7910  tgioolem 7911  lmfval 7922  lmconst 7931  lmnn 7932  iscau3 7935  iscau4 7937  lmuni 7948  lmle 7957  metelcls 7962  metcld 7964  metcnp4 7967  xplmi 7970  xplm 7972  xpcn 7973  bopcnlem2 7979  fsumcnlem 7986  iscms2lem3 7988  lmcau 7993  cmsss 7994  cncms 7995  bcthlem1 7996  bcthlem2 7997  bcthlem7 8002  bcthlem8 8003  bcthlem13 8008  bcthlem14 8009  bcthlem18 8013  bcthlem19 8014  bcthlem20 8015  bcthlem21 8016  bcthlem24 8019  bcthlem25 8020  bcthlem26 8021  bcthlem30 8025  isgrpi 8039  grpidinvlem3 8047  grpidinvlem4 8048  grpidinv 8049  grpidinv2 8056  grpinvval 8063  grpinv 8065  grpinvf 8075  grpinvop 8076  grpdivfval 8077  grppncan 8086  grpnpcan 8087  grppnpcan2 8088  grplactf1o 8094  subgid 8116  subgabl 8119  ghgrpilem3 8131  vcm 8186  invfval 8257  nvmul0or 8268  nvpncan2 8272  nvnncan 8279  nvdif 8289  nvpi 8290  nvabs 8297  nvge0 8298  nvgt0 8299  nv1 8300  imsdf 8316  imsmetlem 8319  nvlmle 8329  nmcnilem 8333  va1cnlem 8341  sm1cnilem 8343  ipval2lem2 8350  ipval2 8353  4ipval2 8354  ipval2lem5 8356  4ipval3 8358  ipnm 8360  ipcl 8361  ipcj 8363  ip1cnilem4 8372  ip1cnilem5 8373  ip1cnilem6 8374  sspg 8383  ssps 8385  sspmlem 8387  sspz 8390  sspn 8391  lno0 8413  lnomul 8417  nmosetn0 8424  nmoge0 8426  nmoub3i 8432  nmo0 8447  nmlno0lem 8449  nmlnogt0 8453  nmblolbii 8455  isblo3i 8457  blometi 8459  blocnilem 8460  blocni 8461  phpar 8479  ipasslem2 8487  ipasslem4 8489  ipasslem8 8493  ipasslem9 8494  ipdi 8499  ipassr 8502  ipsubdir 8504  ipsubdi 8505  ip2eqi 8513  ubthlem3 8527  ubthlem7 8531  ubthlem8 8532  ubthlem9 8533  ubthlem10 8534  ubthlem11 8535  ubthlem12 8536  ubthlem13 8537  ubthlem14 8538  minveclem9 8549  minveclem16 8556  minveclem21 8561  minveclem25 8565  minveclem30 8570  minveclem31 8571  minveclem36 8576  minveclem38 8578  hlipgt0 8612  htthlem7 8622  htthlem9 8624  htthlem11 8626  spwval2 8649  spwpr4OLD 8658  spwpr4aOLD 8659  sincolem 8660  sinperlem1 8681  sinperlem2 8682  efimpi 8693  sineq0 8708  cosh111lem1 8709  efif 8716  efifolem5 8721  efifolem7 8723  efielcirc 8734  shftefif1olem 8736  eff1lem 8738  eff1i 8739  effoi 8740  resslogrn 8748  reeflogt 8756  relogeftb 8760  h2hcau 8844  hvsubdistr1t 8911  hvsubdistr2t 8912  hvmulcant 8934  hvmulcan2t 8935  hvsubcan2t 8937  his2subt 8953  his6t 8960  hi2eqt 8966  normf 8984  normge0t 8987  normgt0tOLD 8988  normgt0t 8989  norm-it 8991  hhph 9040  bcsALT 9041  hcau2 9050  hhcms 9067  norm1t 9116  norm1ex 9117  hhssnv 9129  hhsscms 9145  chocuni 9167  occllem6 9173  projlem2 9182  projlem25 9205  projlem26 9206  projlem28 9208  projlem30 9210  pjthlem7 9220  pjthlem10 9223  pjpot 9256  hsupval2t 9295  spanssoc 9314  pjspansnt 9495  spanunsn 9497  h1datom 9499  fh1t 9556  fh2t 9557  cm2jt 9558  osumlem6 9578  osumlem7 9579  nonbool 9591  spansncv 9592  5oalem1 9594  5oalem2 9595  3oalem2 9603  pjrn 9642  pjft 9648  pjnorm2t 9667  mayete3 9668  hosubcl 9690  hoaddcom 9693  honegsub 9717  homco1t 9722  homulasst 9723  hoadddit 9724  hoadddirt 9725  adjsymt 9754  eigpos 9757  cnvadj 9811  hhlno 9821  nmoplbt 9826  nmopub2tALT 9828  nmopge0t 9830  nmopgt0t 9831  unoplint 9839  nmfnlbt 9843  nmfnleub2t 9845  nmfnge0t 9846  adj2t 9853  adjadjt 9855  adjvalvalt 9856  hmoplint 9861  kbpjt 9875  eighmret 9882  eighmortht 9883  homco2t 9896  hoddi 9909  nmlnop0ALT 9915  lnophs 9921  lnopeq 9928  nmopunt 9934  nmbdoplb 9944  nmcopexlem3 9948  nmcopexlem5 9950  nmcopexlem6 9951  nmcoplb 9953  nmophm 9956  lnopcon 9958  lnopcnbdt 9960  nmbdfnlb 9973  nmcfnexlem3 9977  nmcfnexlem5 9979  nmcfnexlem6 9980  nmcfnlb 9982  lnfncon 9985  lnfncnbdt 9987  riesz3 9990  cnlnadjlem2 9996  cnlnadjlem5 9999  cnlnadjlem6 10000  cnlnadjlem7 10001  adjbdlnt 10011  adjbd1o 10013  adjlnopt 10014  nmopadjlem 10017  nmoptri 10022  nmopco 10023  nmopcoadj 10029  branmfnt 10033  cnvbravalt 10038  kbass2t 10045  leop2t 10052  leop3t 10053  leoprf2t 10055  leopmult 10062  leopmul2it 10063  leoptrit 10064  leopnmidt 10066  nmopleidt 10067  pjnmop 10070  hmopidmchlem 10073  hmopidmch 10074  hmopidmpj 10075  pjsdi 10078  pjddi 10079  pjss2co 10087  pjsspos 10095  pjhmopidm 10105  pjclem4 10122  pj3s 10130  pj3cor1 10132  hstle1t 10148  hstlet 10152  sto2 10159  stadd 10168  stadd3 10170  strlem1 10172  strlem3a 10174  strlem5 10177  strlem6 10178  str 10179  hstrlem6 10186  hstr 10187  jplem1 10190  golem1 10193  stcltrlem1 10198  dmdbr5 10230  mdslmd1lem1 10247  csmdsym 10256  cvdmdt 10259  atom1d 10275  superpos 10276  shatomic 10280  irredlem2 10313  atcvat3 10318  atcvat4 10319  mdsymlem1 10325  mdsymlem2 10326  mdsymlem6 10330  cdj1 10355  cdj3lem2 10357  cdj3 10363  ghomgrpilem2 10381  ghomfo 10386  ghomid 10389  ghomf1olem 10391  cayleylem2 10405  nnssi3 10415  nndivlub 10417  fiv 10470  cdrci 10480  truni1 10485  homeofval 10502  hmeogrp 10524  homindlem3 10537  qusp 10541  fipfil 10549  fipfil2 10550  fgsb 10555  efilcp 10556  fgsb2 10560  efilcp2 10561  cnfilca 10562  sfvlim 10576  dmse1 10594  msr3 10596  mslb1 10600  2wsms 10601  msra3 10602  iintlem1 10603  trran 10607  trnij 10608  cnvtr 10609  rcmob 10653  imonclem 10712  icmpmon 10715

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain