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 557  orim12d 564  pm5.21ni 677  ax11indalem 1366  ax11inda2ALT 1367  eueq2 1914  eueq3 1915  sbc2or 1954  sstrd 2070  ralidm 2353  raaan 2356  sspr 2471  exss 2764  reuuniss 2884  reuuniss2 2886  reuunixfr 2901  ordelord 2965  onfr 2981  onnmin 3010  onminex 3015  onmindif2 3056  ordunel 3079  limsssuc 3116  peano5 3148  unixp 3509  cnvexg 3511  cnvpo 3514  cofunexg 3572  funfni 3580  fnresdm 3588  fnex 3599  fconstg 3650  f1ores 3694  fimacnv 3801  dff2 3808  fconst3 3841  f1ocnvfv3 3874  tfrlem10 3911  tfrlem12 3913  oprabex2g 4011  sbcopeq1a 4101  csbopeq1a 4102  dfoprab4 4106  oesuc 4156  odi 4200  oewordri 4209  oeworde 4210  oelim2 4212  en2d 4387  undom 4424  xpdom1 4429  sbthlem8 4440  2pwuninel 4473  limenpsi 4491  limensuci 4492  php3 4501  unblem4 4526  unbnn 4527  unifi 4538  fodomfi 4546  iunfi 4549  pwfilem 4550  supub 4560  suplub 4561  supmax 4569  suppr 4570  noinfep 4620  r1ord 4635  rankr1 4654  rankxplim3 4694  fodom 4778  unidom 4788  uniimadom 4790  unxpdomlem 4823  unxpdom2 4825  cardalephex 4866  alephval2 4882  alephval3 4883  cfsuc 4895  cdafi 4916  axrepnd 4926  indpi 5014  halfpq 5062  ltaddpr 5120  ltexprlem2 5123  negexsr 5191  mulgt0sr 5194  axmulopr 5246  axcnre 5266  cnegext 5328  nnncan1t 5447  mulsubt 5457  pm2.61ltle 5515  lecase 5603  posdift 5635  recextlem2 5664  recext 5665  muleqaddt 5677  recid2t 5707  divrec2t 5711  div23t 5713  div12t 5715  divsubdirt 5739  divcan5t 5745  divdivdivt 5749  divcan6t 5755  divdiv23t 5756  divdivmult 5759  conjmult 5761  lemul1t 5796  ltmul12it 5805  lt2mul2divt 5830  lemuldivt 5832  lt2msq 5837  lediv2t 5847  lediv12it 5852  lediv2it 5853  recp1lt1 5857  recrecltt 5858  ledivp1t 5861  ledivp1 5862  ltdivp1 5863  nnge1t 5899  nngt1ne1t 5900  nndivtrt 5915  halfaddsubt 5996  lt2halvest 5997  avglet 5999  lbinfm 6003  infm3lem 6008  suprub 6011  infmrcl 6024  nnreclt 6027  xrub 6035  supxrre 6038  supxrunb1 6044  supxrbnd 6046  supxrub 6053  nn0ltp1let 6082  zltp1let 6136  z2get 6143  gtndivt 6148  flidt 6188  flval2t 6189  flval3t 6190  fladdzt 6195  flhalft 6197  qaddclt 6215  qmulclt 6217  qbtwnxr 6225  rpdivclt 6237  seq1lem2 6255  ser1mono 6282  shftval2t 6292  shftval5t 6295  2shft 6297  shftcan2t 6298  iooint 6317  iccsupr 6339  icoshft 6349  icoshftf1oi 6350  uznegit 6369  uzind4 6390  infmssuzcl 6406  eluzfz1t 6427  eluzfz2t 6429  fznn0sub2t 6439  fzelp1t 6448  elfzp1 6450  fzrev2it 6453  fzrev3t 6454  fzneuzt 6458  fsequb 6463  fsequb2 6464  fseqsupub 6466  seqzp1 6488  seqzfveq 6494  seqzres 6500  seqzres2 6501  expeq0t 6525  expgt0t 6528  mulexpt 6533  recexpt 6534  expaddt 6535  expsubt 6537  expordit 6539  expwordit 6542  expord2t 6543  expmwordit 6545  exple1t 6546  expubndt 6547  sqlecant 6580  subsqt 6581  bernneq 6591  expnbndt 6593  rpsqrclt 6653  cjclt 6704  imret 6718  reim0t 6719  cjexpt 6760  recjt 6761  imcjt 6762  cj11t 6773  absclt 6776  absvalsqt 6778  absreimt 6800  absdivz 6802  absexpt 6811  absrelet 6812  absimlet 6813  recvalz 6833  cjdiv 6834  absidmt 6838  abssubge0t 6841  abs3dift 6844  abs2difabst 6848  seq1ub 6857  cvg2 6867  caubnd 6871  ser1absdiflem 6874  ser1absdif 6875  facdivt 6887  facndivt 6888  faclbnd 6890  faclbnd2 6891  faclbnd3 6892  faclbnd4lem3 6895  faclbnd5 6898  faclbnd6 6899  facavgt 6900  bcval2t 6905  bccmplt 6908  bcn0t 6909  bcnp11t 6911  bcnp1nt 6912  bccl2t 6917  bcclt 6918  permnnt 6919  dffsum 6944  fsump1s 6959  fsumcllem 6960  fsumsplit 6966  fsumadd 6968  fsumcom 6974  fsumrev 6975  fsumrev2 6976  fsumshft 6977  fsummulc1 6979  fsumdivcALT 6982  fsum0 6985  fsumcmp 6986  fsumcmpndx2 6988  fsumabs 6989  serz1p 6998  serzrelem 7007  binomlem1 7012  binomlem2 7013  binomlem4 7015  binomlem5 7016  bcxmas 7022  clm4le 7027  2climnn 7047  2climnn0 7048  climrecl 7055  climge0 7057  climaddlem3 7060  climaddc1 7062  climmullem1 7064  climmullem2 7065  climmullem3 7066  climmullem4 7067  climmullem5 7068  climmullem8 7071  climmulc2 7073  climsub 7074  climsubc2 7075  climcmplem 7081  clim2serz 7089  climserzle 7091  climcj 7094  climubi 7097  climsup 7099  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp 7118  ser1cmp2 7121  cvgcmp2lem 7124  cvgcmp2clem 7126  isum1p 7149  iserzgt0 7154  isummulc1ALT 7156  reccnv 7161  infcvglem1 7164  infcvglem3 7166  fnsmnt 7169  geoser 7177  georeclim 7183  geoisumr 7186  geoisum1c 7188  0.999... 7189  cvgratlem2ALT 7191  cvgratlem1 7193  cvgratlem2 7194  cvgratlem4 7196  cvgratlem5 7197  fsum0diaglem1 7199  fsum0diaglem2 7200  fsum0diag2 7202  elcncf1d 7213  cjcncf 7221  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  efcltlem1 7254  efcltlem2 7255  ef0lem 7260  efseq0ex 7261  erelem1 7269  erelem3 7271  efaddlem3 7290  efaddlem5 7292  efaddlem6 7293  efaddlem10 7297  efaddlem15 7302  efaddlem16 7303  efaddlem17 7304  efaddlem18 7305  efaddlem19 7306  efaddlem23 7310  efaddlem25 7312  efaddlem27 7314  eff2 7320  efsubt 7321  efexpt 7322  eftabs 7325  ef1tllem 7331  ef01tllem1 7333  ef01tllem2 7334  eirrlem4 7341  abspef01tlub 7344  efgt1 7352  absefm1le 7360  eflegeolem1 7361  efcnlem2 7368  efcn 7371  reeff1o 7376  efi4pt 7385  resin4pt 7386  recos4pt 7387  sinnegt 7392  cosnegt 7393  efivalt 7397  efmivalt 7398  efeult 7399  sinsubt 7405  cossubt 7406  addsint 7407  subcost 7410  sincossqt 7411  sin2tt 7412  cos2tt 7413  sinbndt 7415  cosbndt 7416  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  absefit 7432  abseft 7433  demoivre 7434  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  acdcALT 7446  znnenlem 7451  znnenlemOLD 7452  unbenlem 7455  infpnlem2 7458  ruclem4 7464  ruclem13 7473  infxpidmlem1 7503  infxpidmlem11 7513  infxpidmlem12 7514  infunabs 7516  infcdaabs 7517  infcda 7518  infdif 7519  infxp 7523  alephexp1 7534  alephsuc3 7535  tgval3t 7575  topbast 7577  basgen2t 7589  ntrval 7626  clsval 7627  clsss 7637  elcls 7654  clsndisj 7656  neival 7667  neiss 7673  neips 7677  unnei 7685  lpval 7693  iscnp2 7711  cnpcl 7714  cnco 7718  cnpco 7719  iscncl 7720  cnsscnp 7722  cncnplem2 7725  cnconst 7730  metsym 7766  metge0 7771  metxplem3 7780  metxpdval 7781  metxptval 7782  metxpfval 7783  metxp 7786  bl2in 7795  blex 7801  blss 7805  blssex 7806  ssblex 7808  opnm 7812  opnin 7821  neibl 7829  lpbl 7832  methausi 7833  metcnconst 7837  metcnplem 7838  metcnp 7839  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metcnp3 7848  metcnss 7850  bl2ioo 7863  ioo2bl 7864  blssioo 7865  tgioolem 7866  lmfval 7877  lmconst 7886  lmnn 7887  iscau3 7890  iscau4 7892  lmuni 7902  lmle 7911  metelcls 7916  metcld 7917  metcnp4 7920  xplmi 7923  xplm 7925  xpcn 7926  bopcnlem2 7932  fsumcnlem 7939  iscms2lem3 7941  lmcau 7946  cmsss 7947  cncms 7948  bcthlem1 7949  bcthlem2 7950  bcthlem7 7955  bcthlem8 7956  bcthlem13 7961  bcthlem14 7962  bcthlem18 7966  bcthlem19 7967  bcthlem20 7968  bcthlem21 7969  bcthlem24 7972  bcthlem25 7973  bcthlem26 7974  bcthlem30 7978  isgrpi 7992  grpidinvlem3 8000  grpidinvlem4 8001  grpidinv 8002  grpidinv2 8010  grpinvval 8017  grpinv 8019  grpinvf 8029  grpinvop 8030  grpdivfval 8031  grppncan 8040  grpnpcan 8041  grppnpcan2 8042  grplactf1o 8049  subgid 8072  subgabl 8075  ghgrpilem3 8087  vcm 8142  invfval 8213  nvmul0or 8224  nvpncan2 8228  nvnncan 8235  nvdif 8245  nvpi 8246  nvabs 8253  nvge0 8254  nvgt0 8255  nv1 8256  imsdf 8271  imsmetlem 8274  nvlmle 8281  nmcnilem 8285  va1cnlem 8292  sm1cnilem 8294  ipval2lem2 8301  ipval2 8304  4ipval2 8305  ipval2lem5 8307  4ipval3 8309  ipnm 8311  ipcl 8312  ipcj 8314  ip1cnilem4 8323  ip1cnilem5 8324  ip1cnilem6 8325  sspg 8334  ssps 8336  sspmlem 8338  sspz 8341  sspn 8342  lno0 8364  lnomul 8367  nmosetn0 8373  nmoge0 8375  nmoub3i 8381  nmo0 8396  nmlno0lem 8398  nmlnogt0 8402  nmblolbii 8403  isblo3i 8405  blometi 8407  blocnilem 8408  blocni 8409  phpar 8427  ipasslem2 8435  ipasslem4 8437  ipasslem8 8441  ipasslem9 8442  ipdi 8447  ipassr 8450  ipsubdir 8452  ipsubdi 8453  ip2eqi 8461  ubthlem3 8475  ubthlem7 8479  ubthlem8 8480  ubthlem9 8481  ubthlem10 8482  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  minveclem9 8497  minveclem16 8504  minveclem21 8509  minveclem25 8513  minveclem30 8518  minveclem31 8519  minveclem36 8524  minveclem38 8526  hlipgt0 8559  htthlem7 8569  htthlem9 8571  htthlem11 8573  spwval2 8595  sincolem 8603  sinperlem1 8624  sinperlem2 8625  efimpi 8634  cosh111lem1 8648  efif 8655  efifolem5 8660  efifolem7 8662  efielcircOLD 8674  circgrpOLD 8677  efielcirc 8678  shftefif1olem 8680  eff1lem 8682  eff1i 8683  effoi 8684  resslogrn 8692  reeflogt 8700  relogeftb 8704  h2hcau 8788  hvsubdistr1t 8855  hvsubdistr2t 8856  hvmulcant 8878  hvmulcan2t 8879  hvsubcan2t 8881  his2subt 8897  his6t 8904  hi2eqt 8910  normf 8928  normge0t 8931  normgt0tOLD 8932  normgt0t 8933  norm-it 8935  hhph 8984  bcsALT 8985  hcau2 8994  hhcms 9011  norm1t 9060  norm1ex 9061  hhssnv 9073  hhsscms 9089  chocuni 9111  occllem6 9117  projlem2 9126  projlem25 9149  projlem26 9150  projlem28 9152  projlem30 9154  pjthlem7 9163  pjthlem10 9166  pjpot 9199  hsupval2t 9238  spanssoc 9257  pjspansnt 9440  spanunsn 9442  h1datom 9444  fh1t 9501  fh2t 9502  cm2jt 9503  osumlem6 9523  osumlem7 9524  nonbool 9536  spansncv 9537  5oalem1 9539  5oalem2 9540  3oalem2 9548  pjrn 9587  pjft 9593  pjnorm2t 9612  mayete3 9613  hosubcl 9635  hoaddcom 9638  honegsub 9662  homco1t 9667  homulasst 9668  hoadddit 9669  hoadddirt 9670  adjsymt 9699  eigpos 9702  cnvadj 9756  hhlno 9766  nmoplbt 9771  nmopub2tALT 9773  nmopge0t 9774  nmopgt0t 9775  unoplint 9783  nmfnlbt 9787  nmfnleub2t 9789  nmfnge0t 9790  adj2t 9797  adjadjt 9799  adjvalvalt 9800  hmoplint 9805  kbpjt 9819  eighmret 9826  eighmortht 9827  homco2t 9840  hoddi 9852  nmlnop0ALT 9858  lnophs 9864  lnopeq 9871  nmopunt 9877  nmbdoplb 9887  nmcopexlem3 9891  nmcopexlem5 9893  nmcopexlem6 9894  nmcoplb 9896  nmophm 9899  lnopcon 9901  lnopcnbdt 9903  nmbdfnlb 9916  nmcfnexlem3 9920  nmcfnexlem5 9922  nmcfnexlem6 9923  nmcfnlb 9925  lnfncon 9928  lnfncnbdt 9930  riesz3 9933  cnlnadjlem2 9939  cnlnadjlem5 9942  cnlnadjlem6 9943  cnlnadjlem7 9944  adjbdlnt 9954  adjbd1o 9956  adjlnopt 9957  nmopadjlem 9960  nmoptri 9965  nmopco 9966  nmopcoadj 9972  branmfnt 9976  cnvbravalt 9981  kbass2t 9988  leop2t 9995  leop3t 9996  leoprf2t 9998  leopmult 10005  leopmul2it 10006  leoptrit 10007  leopnmidt 10009  nmopleidt 10010  pjnmop 10013  hmopidmchlem 10016  hmopidmch 10017  hmopidmpj 10018  pjsdi 10021  pjddi 10022  pjss2co 10030  pjsspos 10038  pjhmopidm 10048  pjclem4 10065  pj3s 10073  pj3cor1 10075  hstle1t 10091  hstlet 10095  sto2 10102  stadd 10111  stadd3 10113  strlem1 10115  strlem3a 10117  strlem5 10120  str 10122  hstr 10130  jplem1 10133  golem1 10136  stcltrlem1 10141  mdslmd1lem1 10189  csmdsym 10198  cvdmdt 10201  atom1d 10217  superpos 10218  shatomic 10222  irredlem2 10255  atcvat3 10260  atcvat4 10261  mdsymlem1 10267  mdsymlem2 10268  mdsymlem6 10272  cdj1 10294  cdj3lem2 10296  cdj3 10302  ghomgrpilem2 10320  ghomfo 10325  ghomid 10328  ghomf1olem 10330  cayleylem2 10344  gelsupvalOLD 10354  nnssi3 10356  nndivlub 10358  fiv 10410  cdrci 10417  truni1 10422  homeofval 10439  hmeogrp 10461  qusp 10466  fipfil 10474  fipfil2 10475  fgsb 10480  efilcp 10481  fgsb2 10485  efilcp2 10486  cnfilca 10487  dmse1 10503  msr3 10505  mslb1 10509  2wsms 10510  msra3 10511  iintlem1 10512  trran 10516  trnij 10517  cnvtr 10518  rcmob 10562  imonclem 10619  icmpmon 10623

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