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  anim12d 556  orim12d 563  pm5.21ni 675  ax11indalem 1345  ax11inda2ALT 1346  eueq2 1890  eueq3 1891  sbc2or 1929  sstrd 2045  ralidm 2328  raaan 2331  sspr 2445  exss 2737  reuuniss 2852  reuuniss2 2854  reuunixfr 2869  ordelord 2933  onfr 2949  onnmin 2978  onminex 2983  onmindif2 3024  ordunel 3047  limsssuc 3084  peano5 3116  unixp 3458  cnvexg 3460  cnvpo 3463  cofunexg 3520  funfni 3528  fnbr 3530  fnresdm 3536  fnex 3547  fimacnvdisj 3588  fconstg 3598  f1ores 3642  fimacnv 3749  dff2 3756  fconst3 3789  f1ocnvfv3 3822  tfrlem10 3859  tfrlem12 3861  oprabex2g 3959  eqop 4042  sbcopeq1a 4049  csbopeq1a 4050  dfoprab4 4054  oesuc 4104  odi 4148  oewordri 4157  oeworde 4158  oelim2 4160  f1oeng 4330  en2d 4335  undom 4372  xpdom1 4377  sbthlem8 4388  limenpsi 4437  limensuci 4438  php3 4447  onomeneq 4450  unblem4 4472  unbnn 4473  unifi 4484  fodomfi 4492  iunfi 4495  pwfilem 4496  supub 4506  suplub 4507  suppr 4514  noinfep 4564  r1ord 4579  rankr1 4598  rankxplim3 4638  fodom 4722  unidom 4732  uniimadom 4734  unxpdomlem 4766  unxpdom2 4768  cardalephex 4809  alephval2 4825  alephval3 4826  cfsuc 4838  cdafi 4859  axrepnd 4869  indpi 4957  halfpq 5005  ltaddpr 5063  ltexprlem2 5066  negexsr 5134  mulgt0sr 5137  axmulopr 5189  axcnre 5209  cnegext 5271  nnncan1t 5390  mulsubt 5400  pm2.61ltle 5458  lecase 5546  posdift 5578  recextlem2 5607  recext 5608  muleqaddt 5620  recid2t 5650  divrec2t 5654  div23t 5656  div12t 5658  divsubdirt 5682  divcan5t 5688  divdivdivt 5692  divcan6t 5698  divdiv23t 5699  divdivmult 5702  conjmult 5704  lemul1t 5739  ltmul12it 5748  lt2mul2divt 5773  lemuldivt 5775  lt2msq 5780  lediv2t 5790  ltdiv23t 5791  lediv23t 5792  lediv12it 5795  lediv2it 5796  recp1lt1 5800  recrecltt 5801  ledivp1t 5804  ledivp1 5805  ltdivp1 5806  nnge1t 5842  nngt1ne1t 5843  nndivtrt 5858  halfaddsubt 5939  lt2halvest 5940  avglet 5942  lbinfm 5946  infm3lem 5951  suprub 5954  infmrcl 5967  nnreclt 5970  xrub 5978  supxrre 5981  supxrunb1 5987  supxrbnd 5989  supxrub 5996  nn0ltp1let 6025  zltp1let 6079  z2get 6086  gtndivt 6091  uzindOLD 6107  flidt 6131  flval2t 6132  flval3t 6133  fladdzt 6138  flhalft 6140  qaddclt 6158  qmulclt 6160  qbtwnxr 6168  rpdivclt 6180  seq1lem2 6198  ser1mono 6225  shftval2t 6235  shftval5t 6238  2shft 6240  shftcan2t 6241  iooint 6260  iccsupr 6282  icoshft 6292  icoshftf1oi 6293  uznegit 6312  uzind4 6333  infmssuzcl 6349  eluzfz1t 6370  eluzfz2t 6372  fznn0sub2t 6382  fzelp1t 6391  elfzp1 6393  fzrev2it 6396  fzrev3t 6397  fzneuzt 6401  fsequb 6406  fsequb2 6407  fseqsupub 6409  seqzp1 6431  seqzfveq 6437  seqzres 6443  seqzres2 6444  expeq0t 6468  expgt0t 6471  mulexpt 6476  recexpt 6477  expaddt 6478  expsubt 6480  expordit 6482  expwordit 6485  expord2t 6486  expmwordit 6488  exple1t 6489  expubndt 6490  sqlecant 6523  subsqt 6524  bernneq 6534  expnbndt 6536  rpsqrclt 6596  cjclt 6647  imret 6661  reim0t 6662  cjexpt 6703  recjt 6704  imcjt 6705  cj11t 6716  absclt 6719  absvalsqt 6721  absreimt 6743  absdivz 6745  absexpt 6754  absrelet 6755  absimlet 6756  recvalz 6776  cjdiv 6777  absidmt 6781  abssubge0t 6784  abs3dift 6787  abs2difabst 6791  seq1ub 6800  cvg2 6810  caubnd 6814  ser1absdiflem 6817  ser1absdif 6818  facdivt 6830  facndivt 6831  faclbnd 6833  faclbnd2 6834  faclbnd3 6835  faclbnd4lem3 6838  faclbnd5 6841  faclbnd6 6842  facavgt 6843  bcval2t 6848  bccmplt 6851  bcn0t 6852  bcnp11t 6854  bcnp1nt 6855  bccl2t 6860  bcclt 6861  permnnt 6862  dffsum 6887  fsump1s 6902  fsumcllem 6903  fsumsplit 6909  fsumadd 6911  fsumcom 6917  fsumrev 6918  fsumrev2 6919  fsumshft 6920  fsummulc1 6922  fsumdivcALT 6925  fsum0 6928  fsumcmp 6929  fsumcmpndx2 6931  fsumabs 6932  serz1p 6941  serzrelem 6950  binomlem1 6955  binomlem2 6956  binomlem4 6958  binomlem5 6959  bcxmas 6965  clm4le 6970  2climnn 6990  2climnn0 6991  climrecl 6998  climge0 7000  climaddlem3 7003  climaddc1 7005  climmullem1 7007  climmullem2 7008  climmullem3 7009  climmullem4 7010  climmullem5 7011  climmullem8 7014  climmulc2 7016  climsub 7017  climsubc2 7018  climcmplem 7024  clim2serz 7032  climserzle 7034  climcj 7037  climubi 7040  climsup 7042  caucvglem6 7049  caucvg 7050  serzf0 7056  ser1f0 7057  ser1cmp 7061  ser1cmp2 7064  cvgcmp2lem 7067  cvgcmp2clem 7069  isum1p 7092  iserzgt0 7097  isummulc1ALT 7099  reccnv 7104  infcvglem1 7107  infcvglem3 7109  fnsmnt 7112  geoser 7120  georeclim 7126  geoisumr 7129  geoisum1c 7131  0.999... 7132  cvgratlem2ALT 7134  cvgratlem1 7136  cvgratlem2 7137  cvgratlem4 7139  cvgratlem5 7140  fsum0diaglem1 7142  fsum0diaglem2 7143  fsum0diag2 7145  elcncf1d 7156  cjcncf 7164  ivthlem6 7172  ivthlem7 7173  ivthlem6OLD 7181  ivthlem7OLD 7182  efcltlem1 7197  efcltlem2 7198  ef0lem 7203  efseq0ex 7204  erelem1 7212  erelem3 7214  efaddlem3 7233  efaddlem5 7235  efaddlem6 7236  efaddlem10 7240  efaddlem15 7245  efaddlem16 7246  efaddlem17 7247  efaddlem18 7248  efaddlem19 7249  efaddlem23 7253  efaddlem25 7255  efaddlem27 7257  eff2 7263  efsubt 7264  efexpt 7265  eftabs 7268  ef1tllem 7274  ef01tllem1 7276  ef01tllem2 7277  eirrlem4 7284  abspef01tlub 7287  efgt1 7295  absefm1le 7303  eflegeolem1 7304  efcnlem2 7311  efcn 7314  reeff1o 7319  efi4pt 7328  resin4pt 7329  recos4pt 7330  sinnegt 7335  cosnegt 7336  efivalt 7340  efmivalt 7341  efeult 7342  sinsubt 7348  cossubt 7349  addsint 7350  subcost 7353  sincossqt 7354  sin2tt 7355  cos2tt 7356  sinbndt 7358  cosbndt 7359  sin01bndlem2 7361  sin01bndlem3 7362  cos01bndlem2 7363  cos01bndlem3 7364  sin01gt0 7369  cos01gt0 7370  sin02gt0 7371  absefit 7375  abseft 7376  demoivre 7377  acdc3lem 7379  acdc2lem2 7382  acdc5lem2 7385  acdclem 7387  acdcALT 7389  xpnnen 7392  znnenlem 7394  znnenlemOLD 7395  unbenlem 7398  infpnlem2 7401  ruclem4 7407  ruclem13 7416  infxpidmlem1 7446  infxpidmlem11 7456  infxpidmlem12 7457  infunabs 7459  infcdaabs 7460  infcda 7461  infdif 7462  infxp 7466  alephexp1 7477  alephsuc3 7478  tgval3t 7518  topbast 7520  basgen2t 7532  cctop 7545  ntrval 7569  clsval 7570  clsss 7580  elcls 7596  clsndisj 7598  neival 7606  neiss 7612  neips 7616  unnei 7624  lpval 7632  cnpcl 7651  cnco 7655  cnpco 7656  iscncl 7657  cnsscnp 7659  cncnplem2 7662  cnconst 7667  metsym 7703  metge0 7708  metxplem3 7716  metxpdval 7717  metxptval 7718  metxpfval 7719  metxp 7722  bl2in 7731  blex 7737  blss 7741  blssex 7742  ssblex 7744  opnm 7748  opnin 7757  neibl 7765  lpbl 7767  methausi 7768  metcnconst 7772  metcnplem 7773  metcnp 7774  metcnpi3 7779  metcnpi4 7780  metcni2 7782  metcnp3 7783  metcnss 7785  bl2ioo 7798  ioo2bl 7799  blssioo 7800  tgioolem 7801  lmfval 7811  lmconst 7820  lmnn 7821  iscau3 7824  lmuni 7834  lmle 7843  metelcls 7848  metcld 7849  metcnp4 7852  xplmi 7855  xplm 7857  xpcn 7858  bopcnlem2 7864  fsumcnlem 7871  iscms2lem3 7873  lmcau 7878  cmsss 7879  cncms 7880  bcthlem1 7881  bcthlem2 7882  bcthlem7 7887  bcthlem8 7888  bcthlem13 7893  bcthlem14 7894  bcthlem18 7898  bcthlem19 7899  bcthlem20 7900  bcthlem21 7901  bcthlem24 7904  bcthlem25 7905  bcthlem26 7906  bcthlem30 7910  isgrpi 7924  grpidinvlem3 7932  grpidinvlem4 7933  grpidinv 7934  grpidinv2 7942  grpinvval 7949  grpinv 7951  grpinvf 7962  grpinvop 7963  grpdivfval 7964  grppncan 7973  grpnpcan 7974  grppnpcan2 7975  grplactf1o 7982  subgid 8005  subgabl 8008  ghgrpilem3 8020  vcm 8077  nvmul0or 8149  nvpncan2 8153  nvnncan 8160  nvdif 8169  nvpi 8170  nvabs 8177  nvge0 8178  nvgt0 8179  nv1 8180  imsdf 8195  imsmetlem 8198  nvlmle 8205  nmcnilem 8209  va1cnlem 8214  sm1cnilem 8216  ipval2lem2 8223  ipval2 8226  4ipval2 8227  ipval2lem5 8229  4ipval3 8231  ipnm 8233  ipcl 8234  ipcj 8236  ip1cnilem4 8245  ip1cnilem5 8246  ip1cnilem6 8247  sspg 8256  ssps 8258  sspmlem 8260  sspz 8263  sspn 8264  lno0 8286  lnomul 8289  nmosetn0 8295  nmoge0 8297  nmoub3i 8303  nmo0 8318  nmlno0lem 8320  nmlnogt0 8324  nmblolbii 8325  isblo3i 8327  blometi 8329  blocnilem 8330  blocni 8331  phpar 8349  ipasslem1 8356  ipasslem2 8357  ipasslem4 8359  ipasslem8 8363  ipasslem9 8364  ipdi 8369  ipassr 8372  ipsubdir 8374  ipsubdi 8375  ip2eqi 8383  ubthlem3 8397  ubthlem7 8401  ubthlem8 8402  ubthlem9 8403  ubthlem10 8404  ubthlem11 8405  ubthlem12 8406  ubthlem13 8407  ubthlem14 8408  minveclem9 8419  minveclem16 8426  minveclem21 8431  minveclem25 8435  minveclem30 8440  minveclem31 8441  minveclem36 8446  minveclem38 8448  hlipgt0 8480  htthlem7 8490  htthlem9 8492  htthlem11 8494  sincolem 8497  sinperlem1 8518  sinperlem2 8519  efimpi 8528  cosh111lem1 8542  efif 8549  efifolem5 8554  efifolem7 8556  efielcircOLD 8568  circgrpOLD 8571  efielcirc 8572  shftefif1olem 8574  shftefif1olemOLD 8575  eff1lem 8577  eff1i 8578  effoi 8579  effoiOLD 8580  resslogrn 8588  reeflogt 8596  relogeftb 8600  ghomgrpilem2 8653  ghomfo 8658  ghomid 8661  ghomf1olem 8663  cayleylem2 8677  fiv 8731  cdrci 8738  truni1 8743  homeofval 8754  hmeogrp 8776  qusp 8780  fipfil 8788  fipfil2 8789  fgsb 8794  efilcp 8795  fgsb2 8799  efilcp2 8800  cnfilca 8801  dmse1 8817  msr3 8819  mslb1 8823  2wsms 8824  msra3 8825  iintlem1 8826  trran 8830  trnij 8831  cnvtr 8832  rcmob 8876  imonclem 8933  icmpmon 8937  hvpncant 9057  hvsubdistr1t 9065  hvsubdistr2t 9066  hvmulcant 9088  hvmulcan2t 9089  hvsubcan2t 9091  his2subt 9107  his6t 9114  hi2eqt 9120  normf 9138  normge0t 9141  normgt0tOLD 9142  normgt0t 9143  norm-it 9145  hhph 9194  bcsALT 9195  hcau2 9205  hilcau 9217  hhcms 9223  norm1t 9272  norm1ex 9273  chocuni 9302  occllem6 9308  projlem2 9317  projlem25 9340  projlem26 9341  projlem28 9343  projlem30 9345  pjthlem7 9354  pjthlem10 9357  pjpot 9390  hsupval2t 9429  spanssoc 9448  pjspansnt 9631  spanunsn 9633  h1datom 9635  fh1t 9692  fh2t 9693  cm2jt 9694  osumlem6 9714  osumlem7 9715  nonbool 9727  spansncv 9728  5oalem1 9730  5oalem2 9731  3oalem2 9739  pjidt 9771  pjrn 9778  pjft 9784  pjnorm2t 9803  mayete3 9804  hosubcl 9826  hoaddcom 9829  honegsub 9853  homco1t 9858  homulasst 9859  hoadddit 9860  hoadddirt 9861  adjsymt 9890  eigpos 9893  cnvadj 9947  hhlno 9957  nmoplbt 9962  nmopub2tALT 9964  nmopge0t 9965  nmopgt0t 9966  unoplint 9974  hmopret 9977  nmfnlbt 9978  nmfnleub2t 9980  nmfnge0t 9981  adj2t 9988  adjadjt 9990  adjvalvalt 9991  hmoplint 9996  kbpjt 10010  eigvalclt 10015  eighmret 10017  eighmortht 10018  homco2t 10031  hoddi 10043  nmlnop0ALT 10049  lnophs 10055  lnopeq 10062  nmopunt 10068  nmbdoplb 10078  nmcopexlem3 10082  nmcopexlem5 10084  nmcopexlem6 10085  nmcoplb 10087  nmophm 10090  lnopcon 10092  lnopcnbdt 10094  nmbdfnlb 10107  nmcfnexlem3 10111  nmcfnexlem5 10113  nmcfnexlem6 10114  nmcfnlb 10116  lnfncon 10119  lnfncnbdt 10121  riesz3 10124  cnlnadjlem2 10130  cnlnadjlem5 10133  cnlnadjlem6 10134  cnlnadjlem7 10135  adjbdlnt 10145  adjbd1o 10147  adjlnopt 10148  nmopadjlem 10151  nmoptri 10155  nmopco 10156  nmopcoadj 10162  branmfnt 10165  cnvbravalt 10170  kbass2t 10176  leop2t 10183  leop3t 10184  leoprf2t 10186  leopmult 10193  leopmul2it 10194  leoptrit 10195  leopnmidt 10196  nmopleidt 10197  pjnmop 10200  hmopidmchlem 10203  hmopidmch 10204  hmopidmpj 10205  pjsdi 10208  pjddi 10209  pjss2co 10217  pjsspos 10225  pjhmopidm 10234  pjclem4 10251  pj3s 10259  pj3cor1 10261  hstle1t 10277  hstlet 10281  sto2 10288  stadd 10297  stadd3 10299  strlem1 10301  strlem3a 10303  strlem5 10306  str 10308  hstr 10316  jplem1 10319  golem1 10322  stcltrlem1 10327  mdslmd1lem1 10374  csmdsym 10383  cvdmdt 10386  atom1d 10402  superpos 10403  shatomic 10407  cvp 10424  irredlem2 10440  atcvat3 10445  atcvat4 10446  mdsymlem1 10452  mdsymlem2 10453  mdsymlem6 10457  cdj1 10479  cdj3lem2 10481  cdj3 10487

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