Theorem sylanc 471

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 472  sylancom 475  anim12d 558  orim12d 565  pm5.21ni 678  ax11indalem 1368  ax11inda2ALT 1369  eueq2 1918  eueq3 1919  sbc2or 1958  sstrd 2074  ralidm 2357  raaan 2360  sspr 2475  exss 2769  reuuniss 2889  reuuniss2 2891  reuunixfr 2906  ordelord 2970  onfr 2986  onnmin 3015  onminex 3020  onmindif2 3061  ordunel 3084  limsssuc 3121  peano5 3153  unixp 3517  cnvexg 3519  cnvpo 3522  cofunexg 3580  funfni 3588  fnresdm 3596  fnex 3607  fconstg 3659  f1ores 3703  fimacnv 3810  dff2 3817  fconst3 3850  f1ocnvfv3 3883  tfrlem10 3920  tfrlem12 3922  oprabex2g 4020  sbcopeq1a 4111  csbopeq1a 4112  dfoprab4 4116  oesuc 4166  odi 4210  oewordri 4219  oeworde 4220  oelim2 4222  en2d 4399  undom 4436  xpdom1 4441  sbthlem8 4452  2pwuninel 4485  limenpsi 4503  limensuci 4504  php3 4513  unblem4 4538  unbnn 4539  unifi 4550  fodomfi 4558  iunfi 4561  pwfilem 4562  supub 4572  suplub 4573  supmax 4581  suppr 4582  noinfep 4632  r1ord 4647  rankr1 4666  rankxplim3 4706  fodom 4790  unidom 4800  uniimadom 4802  unxpdomlem 4835  unxpdom2 4837  cardalephex 4878  alephval2 4894  alephval3 4895  cfsuc 4907  cdafi 4928  axrepnd 4938  indpi 5026  halfpq 5074  ltaddpr 5132  ltexprlem2 5135  negexsr 5203  mulgt0sr 5206  axmulopr 5258  axcnre 5278  cnegext 5340  nnncan1t 5459  mulsubt 5469  pm2.61ltle 5526  lecase 5613  posdift 5645  recextlem2 5674  recext 5675  muleqaddt 5688  divcan2t 5714  recid2t 5724  divrec2t 5728  div23t 5730  div12t 5732  divsubdirtOLD 5763  divcan5t 5769  divdivdivt 5773  divcan6t 5779  divdiv23t 5780  divdivmult 5783  conjmult 5785  lemul1t 5820  ltmul12it 5829  lediv1t 5839  lt2mul2divt 5860  lemuldivt 5862  lemuldivtOLD 5863  lt2msq 5869  lediv2t 5879  lediv12it 5884  lediv2it 5885  recp1lt1 5889  recrecltt 5890  ledivp1t 5893  ledivp1 5894  ltdivp1 5895  nnge1t 5931  nngt1ne1t 5932  nnrecret 5940  nndivtrt 5948  halfaddsubt 6029  lt2halvest 6030  avglet 6032  lbinfm 6036  infm3lem 6041  suprub 6044  infmrcl 6057  nnreclt 6060  xrub 6068  supxrre 6071  supxrunb1 6077  supxrbnd 6079  supxrub 6086  nn0ltp1let 6115  zltp1let 6169  z2get 6176  gtndivt 6181  flidt 6223  flval2t 6225  flval3t 6226  flbi2t 6228  fladdzt 6231  flhalft 6233  quoremOLD 6238  intfrac 6239  intfracOLD 6240  intfracq 6241  qaddclt 6255  qmulclt 6257  qbtwnxr 6265  rpne0t 6274  rpdivclt 6278  seq1lem2 6296  ser1mono 6323  shftval2t 6333  shftval5t 6336  2shft 6338  shftcan2t 6339  iooint 6358  iccsupr 6384  icoshft 6394  icoshftf1oi 6395  uznegit 6415  uzind4 6436  infmssuzcl 6452  eluzfz1t 6473  eluzfz2t 6475  fznn0sub2t 6485  fzelp1t 6494  elfzp1 6496  fzrev2it 6499  fzrev3t 6500  fzneuzt 6504  fsequb 6509  fsequb2 6510  fseqsupub 6512  seqzp1 6534  seqzfveq 6540  seqzres 6546  seqzres2 6547  expeq0t 6571  expgt0t 6575  mulexpt 6580  recexpt 6581  expaddt 6582  expsubt 6584  expordit 6586  expwordit 6589  expord2t 6590  expmwordit 6592  exple1t 6593  expubndt 6594  sqlecant 6627  subsqt 6628  bernneq 6638  expnbndt 6640  expnlbndt 6641  rpsqrclt 6701  cjclt 6750  imret 6759  reim0t 6760  cjexpt 6802  recjt 6803  imcjt 6804  cj11t 6815  absclt 6818  absvalsqt 6820  absreimt 6842  absdivz 6844  absexpt 6853  absrelet 6854  absimlet 6855  recvalz 6872  cjdiv 6873  absidmt 6877  abssubge0t 6880  abs3dift 6884  abs2difabst 6888  seq1ub 6897  cvg2 6907  caubnd 6911  ser1absdiflem 6914  ser1absdif 6915  facdivt 6927  facndivt 6928  faclbnd 6930  faclbnd2 6931  faclbnd3 6932  faclbnd4lem3 6935  faclbnd5 6938  faclbnd6 6939  facavgt 6940  bcval2t 6944  bccmplt 6947  bcn0t 6948  bcnp11t 6950  bcnp1nt 6951  bccl2t 6956  bcclt 6957  permnnt 6958  dffsum 6983  fsump1s 6998  fsumcllem 6999  fsumsplit 7005  fsumadd 7007  fsumcom 7013  fsumrev 7014  fsumrev2 7015  fsumshft 7016  fsummulc1 7018  fsumdivcALT 7021  fsum0 7024  fsumcmp 7025  fsumcmpndx2 7027  fsumabs 7028  serz1p 7037  serzrelem 7046  binomlem1 7051  binomlem2 7052  binomlem4 7054  binomlem5 7055  bcxmas 7061  clm4le 7066  2climnn 7087  2climnn0 7088  climrecl 7095  climge0 7097  climaddlem3 7101  climaddc1 7103  climmullem1 7105  climmullem2 7106  climmullem3 7107  climmullem4 7108  climmullem5 7109  climmullem8 7112  climmulc2 7114  climsub 7115  climsubc2 7116  climcmplem 7122  clim2serz 7130  climserzle 7132  climcj 7135  climubi 7138  climsup 7140  caucvglem6 7147  caucvg 7148  serzf0 7154  ser1f0 7155  ser1cmp 7159  ser1cmp2 7162  cvgcmp2lem 7165  cvgcmp2clem 7167  isum1p 7191  iserzgt0 7196  isummulc1ALT 7198  reccnv 7203  infcvglem1 7206  infcvglem3 7208  fnsmnt 7211  geoser 7219  georeclim 7225  geoisumr 7228  geoisum1c 7230  0.999... 7231  cvgratlem2ALT 7233  cvgratlem1 7235  cvgratlem2 7236  cvgratlem4 7238  cvgratlem5 7239  fsum0diaglem1 7241  fsum0diaglem2 7242  fsum0diag2 7244  elcncf1d 7255  cjcncf 7263  ivthlem6 7271  ivthlem7 7272  efcltlem1 7289  efcltlem2 7290  ef0lem 7295  efseq0ex 7296  erelem1 7304  erelem3 7306  efaddlem3 7325  efaddlem5 7327  efaddlem6 7328  efaddlem10 7332  efaddlem15 7337  efaddlem16 7338  efaddlem17 7339  efaddlem18 7340  efaddlem19 7341  efaddlem23 7345  efaddlem25 7347  efaddlem27 7349  eff2 7355  efsubt 7356  efexpt 7357  eftabs 7360  ef1tllem 7366  ef01tllem1 7368  ef01tllem2 7369  ef01tllem2OLD 7370  eirrlem4 7377  abspef01tlub 7380  efgt1 7388  absefm1le 7397  eflegeolem1 7398  efcnlem2 7405  efcn 7408  reeff1o 7411  efi4pt 7420  resin4pt 7421  recos4pt 7422  sinnegt 7427  cosnegt 7428  efivalt 7432  efmivalt 7433  efeult 7434  sinsubt 7440  cossubt 7441  addsint 7442  subcost 7445  sincossqt 7446  sin2tt 7447  cos2tt 7448  sinbndt 7450  cosbndt 7451  sin01bndlem2 7453  sin01bndlem3 7454  cos01bndlem2 7455  cos01bndlem3 7456  sin01gt0 7461  cos01gt0 7462  sin02gt0 7463  absefit 7467  abseft 7468  demoivre 7469  acdc3lem 7471  acdc2lem2 7474  acdc5lem2 7477  acdclem 7479  acdcALT 7481  znnenlem 7486  unbenlem 7489  infpnlem2 7492  ruclem4 7498  ruclem13 7507  infxpidmlem1 7537  infxpidmlem11 7547  infxpidmlem12 7548  infunabs 7550  infcdaabs 7551  infcda 7552  infdif 7553  infxp 7557  alephexp1 7569  alephsuc3 7570  tgval3t 7610  topbast 7612  basgen2t 7624  ntrval 7661  clsval 7662  clsss 7672  elcls 7689  clsndisj 7691  neival 7702  neiss 7708  neips 7712  unnei 7720  lpval 7728  iscnp2 7746  cnpcl 7749  cnco 7753  cnpco 7754  iscncl 7755  cnsscnp 7757  cncnplem2 7760  cnconst 7765  metsym 7801  metge0 7804  metxplem3 7813  metxpdval 7814  metxptval 7815  metxpfval 7816  metxp 7819  bl2in 7828  blex 7834  blss 7838  blssex 7839  ssblex 7841  opnm 7845  opnin 7854  neibl 7862  lpbl 7865  methausi 7866  metcnconst 7870  metcnplem 7871  metcnp 7872  metcnpi3 7877  metcnpi4 7878  metcni2 7880  metcnp3 7881  metcnss 7883  bl2ioo 7896  ioo2bl 7897  blssioo 7898  tgioolem 7899  lmfval 7910  lmconst 7919  lmnn 7920  iscau3 7923  iscau4 7925  lmuni 7936  lmle 7945  metelcls 7950  metcld 7952  metcnp4 7955  xplmi 7958  xplm 7960  xpcn 7961  bopcnlem2 7967  fsumcnlem 7974  iscms2lem3 7976  lmcau 7981  cmsss 7982  cncms 7983  bcthlem1 7984  bcthlem2 7985  bcthlem7 7990  bcthlem8 7991  bcthlem13 7996  bcthlem14 7997  bcthlem18 8001  bcthlem19 8002  bcthlem20 8003  bcthlem21 8004  bcthlem24 8007  bcthlem25 8008  bcthlem26 8009  bcthlem30 8013  isgrpi 8027  grpidinvlem3 8035  grpidinvlem4 8036  grpidinv 8037  grpidinv2 8045  grpinvval 8052  grpinv 8054  grpinvf 8064  grpinvop 8065  grpdivfval 8066  grppncan 8075  grpnpcan 8076  grppnpcan2 8077  grplactf1o 8083  subgid 8105  subgabl 8108  ghgrpilem3 8120  vcm 8175  invfval 8246  nvmul0or 8257  nvpncan2 8261  nvnncan 8268  nvdif 8278  nvpi 8279  nvabs 8286  nvge0 8287  nvgt0 8288  nv1 8289  imsdf 8305  imsmetlem 8308  nvlmle 8318  nmcnilem 8322  va1cnlem 8330  sm1cnilem 8332  ipval2lem2 8339  ipval2 8342  4ipval2 8343  ipval2lem5 8345  4ipval3 8347  ipnm 8349  ipcl 8350  ipcj 8352  ip1cnilem4 8361  ip1cnilem5 8362  ip1cnilem6 8363  sspg 8372  ssps 8374  sspmlem 8376  sspz 8379  sspn 8380  lno0 8402  lnomul 8406  nmosetn0 8413  nmoge0 8415  nmoub3i 8421  nmo0 8436  nmlno0lem 8438  nmlnogt0 8442  nmblolbii 8444  isblo3i 8446  blometi 8448  blocnilem 8449  blocni 8450  phpar 8468  ipasslem2 8476  ipasslem4 8478  ipasslem8 8482  ipasslem9 8483  ipdi 8488  ipassr 8491  ipsubdir 8493  ipsubdi 8494  ip2eqi 8502  ubthlem3 8516  ubthlem7 8520  ubthlem8 8521  ubthlem9 8522  ubthlem10 8523  ubthlem11 8524  ubthlem12 8525  ubthlem13 8526  ubthlem14 8527  minveclem9 8538  minveclem16 8545  minveclem21 8550  minveclem25 8554  minveclem30 8559  minveclem31 8560  minveclem36 8565  minveclem38 8567  hlipgt0 8601  htthlem7 8611  htthlem9 8613  htthlem11 8615  spwval2 8638  spwpr3OLD 8647  spwpr4OLD 8648  spwpr4aOLD 8649  sincolem 8650  sinperlem1 8671  sinperlem2 8672  efimpi 8683  sineq0 8698  cosh111lem1 8699  efif 8706  efifolem5 8711  efifolem7 8713  efielcirc 8724  shftefif1olem 8726  eff1lem 8728  eff1i 8729  effoi 8730  resslogrn 8738  reeflogt 8746  relogeftb 8750  h2hcau 8834  hvsubdistr1t 8901  hvsubdistr2t 8902  hvmulcant 8924  hvmulcan2t 8925  hvsubcan2t 8927  his2subt 8943  his6t 8950  hi2eqt 8956  normf 8974  normge0t 8977  normgt0tOLD 8978  normgt0t 8979  norm-it 8981  hhph 9030  bcsALT 9031  hcau2 9040  hhcms 9057  norm1t 9106  norm1ex 9107  hhssnv 9119  hhsscms 9135  chocuni 9157  occllem6 9163  projlem2 9172  projlem25 9195  projlem26 9196  projlem28 9198  projlem30 9200  pjthlem7 9210  pjthlem10 9213  pjpot 9246  hsupval2t 9285  spanssoc 9304  pjspansnt 9485  spanunsn 9487  h1datom 9489  fh1t 9546  fh2t 9547  cm2jt 9548  osumlem6 9568  osumlem7 9569  nonbool 9581  spansncv 9582  5oalem1 9584  5oalem2 9585  3oalem2 9593  pjrn 9632  pjft 9638  pjnorm2t 9657  mayete3 9658  hosubcl 9680  hoaddcom 9683  honegsub 9707  homco1t 9712  homulasst 9713  hoadddit 9714  hoadddirt 9715  adjsymt 9744  eigpos 9747  cnvadj 9801  hhlno 9811  nmoplbt 9816  nmopub2tALT 9818  nmopge0t 9820  nmopgt0t 9821  unoplint 9829  nmfnlbt 9833  nmfnleub2t 9835  nmfnge0t 9836  adj2t 9843  adjadjt 9845  adjvalvalt 9846  hmoplint 9851  kbpjt 9865  eighmret 9872  eighmortht 9873  homco2t 9886  hoddi 9899  nmlnop0ALT 9905  lnophs 9911  lnopeq 9918  nmopunt 9924  nmbdoplb 9934  nmcopexlem3 9938  nmcopexlem5 9940  nmcopexlem6 9941  nmcoplb 9943  nmophm 9946  lnopcon 9948  lnopcnbdt 9950  nmbdfnlb 9963  nmcfnexlem3 9967  nmcfnexlem5 9969  nmcfnexlem6 9970  nmcfnlb 9972  lnfncon 9975  lnfncnbdt 9977  riesz3 9980  cnlnadjlem2 9986  cnlnadjlem5 9989  cnlnadjlem6 9990  cnlnadjlem7 9991  adjbdlnt 10001  adjbd1o 10003  adjlnopt 10004  nmopadjlem 10007  nmoptri 10012  nmopco 10013  nmopcoadj 10019  branmfnt 10023  cnvbravalt 10028  kbass2t 10035  leop2t 10042  leop3t 10043  leoprf2t 10045  leopmult 10052  leopmul2it 10053  leoptrit 10054  leopnmidt 10056  nmopleidt 10057  pjnmop 10060  hmopidmchlem 10063  hmopidmch 10064  hmopidmpj 10065  pjsdi 10068  pjddi 10069  pjss2co 10077  pjsspos 10085  pjhmopidm 10095  pjclem4 10112  pj3s 10120  pj3cor1 10122  hstle1t 10138  hstlet 10142  sto2 10149  stadd 10158  stadd3 10160  strlem1 10162  strlem3a 10164  strlem5 10167  strlem6 10168  str 10169  hstrlem6 10176  hstr 10177  jplem1 10180  golem1 10183  stcltrlem1 10188  dmdbr5 10220  mdslmd1lem1 10237  csmdsym 10246  cvdmdt 10249  atom1d 10265  superpos 10266  shatomic 10270  irredlem2 10303  atcvat3 10308  atcvat4 10309  mdsymlem1 10315  mdsymlem2 10316  mdsymlem6 10320  cdj1 10345  cdj3lem2 10347  cdj3 10353  ghomgrpilem2 10371  ghomfo 10376  ghomid 10379  ghomf1olem 10381  cayleylem2 10395  nnssi3 10405  nndivlub 10407  fiv 10459  cdrci 10466  truni1 10471  homeofval 10488  hmeogrp 10510  qusp 10515  fipfil 10523  fipfil2 10524  fgsb 10529  efilcp 10530  fgsb2 10535  efilcp2 10536  cnfilca 10537  dmse1 10566  msr3 10568  mslb1 10572  2wsms 10573  msra3 10574  iintlem1 10575  trran 10579  trnij 10580  cnvtr 10581  rcmob 10625  imonclem 10682  icmpmon 10686

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