HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 sylanc.1 . . 3 |- ((ph /\ ps) -> ch)
21ex 373 . 2 |- (ph -> (ps -> ch))
3 sylanc.2 . 2 |- (th -> ph)
4 sylanc.3 . 2 |- (th -> ps)
52, 3, 4sylc 68 1 |- (th -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  syl2anc 472  anim12d 556  orim12d 563  pm5.21ni 676  ax11indalem 1361  ax11inda2ALT 1362  eueq2 1909  eueq3 1910  sbc2or 1948  sstrd 2064  ralidm 2347  raaan 2350  sspr 2466  exss 2759  reuuniss 2879  reuuniss2 2881  reuunixfr 2896  ordelord 2960  onfr 2976  onnmin 3005  onminex 3010  onmindif2 3051  ordunel 3074  limsssuc 3111  peano5 3143  unixp 3503  cnvexg 3505  cnvpo 3508  cofunexg 3566  funfni 3574  fnbr 3576  fnresdm 3582  fnex 3593  fimacnvdisj 3634  fconstg 3644  f1ores 3688  fimacnv 3795  dff2 3802  fconst3 3835  f1ocnvfv3 3868  tfrlem10 3905  tfrlem12 3907  oprabex2g 4005  eqop 4088  sbcopeq1a 4095  csbopeq1a 4096  dfoprab4 4100  oesuc 4150  odi 4194  oewordri 4203  oeworde 4204  oelim2 4206  f1oeng 4376  en2d 4381  undom 4418  xpdom1 4423  sbthlem8 4434  limenpsi 4485  limensuci 4486  php3 4495  onomeneq 4498  unblem4 4520  unbnn 4521  unifi 4532  fodomfi 4540  iunfi 4543  pwfilem 4544  supub 4554  suplub 4555  suppr 4562  noinfep 4612  r1ord 4627  rankr1 4646  rankxplim3 4686  fodom 4770  unidom 4780  uniimadom 4782  unxpdomlem 4815  unxpdom2 4817  cardalephex 4858  alephval2 4874  alephval3 4875  cfsuc 4887  cdafi 4908  axrepnd 4918  indpi 5006  halfpq 5054  ltaddpr 5112  ltexprlem2 5115  negexsr 5183  mulgt0sr 5186  axmulopr 5238  axcnre 5258  cnegext 5320  nnncan1t 5439  mulsubt 5449  pm2.61ltle 5507  lecase 5595  posdift 5627  recextlem2 5656  recext 5657  muleqaddt 5669  recid2t 5699  divrec2t 5703  div23t 5705  div12t 5707  divsubdirt 5731  divcan5t 5737  divdivdivt 5741  divcan6t 5747  divdiv23t 5748  divdivmult 5751  conjmult 5753  lemul1t 5788  ltmul12it 5797  lt2mul2divt 5822  lemuldivt 5824  lt2msq 5829  lediv2t 5839  ltdiv23t 5840  lediv23t 5841  lediv12it 5844  lediv2it 5845  recp1lt1 5849  recrecltt 5850  ledivp1t 5853  ledivp1 5854  ltdivp1 5855  nnge1t 5891  nngt1ne1t 5892  nndivtrt 5907  halfaddsubt 5988  lt2halvest 5989  avglet 5991  lbinfm 5995  infm3lem 6000  suprub 6003  infmrcl 6016  nnreclt 6019  xrub 6027  supxrre 6030  supxrunb1 6036  supxrbnd 6038  supxrub 6045  nn0ltp1let 6074  zltp1let 6128  z2get 6135  gtndivt 6140  uzindOLD 6156  flidt 6180  flval2t 6181  flval3t 6182  fladdzt 6187  flhalft 6189  qaddclt 6207  qmulclt 6209  qbtwnxr 6217  rpdivclt 6229  seq1lem2 6247  ser1mono 6274  shftval2t 6284  shftval5t 6287  2shft 6289  shftcan2t 6290  iooint 6309  iccsupr 6331  icoshft 6341  icoshftf1oi 6342  uznegit 6361  uzind4 6382  infmssuzcl 6398  eluzfz1t 6419  eluzfz2t 6421  fznn0sub2t 6431  fzelp1t 6440  elfzp1 6442  fzrev2it 6445  fzrev3t 6446  fzneuzt 6450  fsequb 6455  fsequb2 6456  fseqsupub 6458  seqzp1 6480  seqzfveq 6486  seqzres 6492  seqzres2 6493  expeq0t 6517  expgt0t 6520  mulexpt 6525  recexpt 6526  expaddt 6527  expsubt 6529  expordit 6531  expwordit 6534  expord2t 6535  expmwordit 6537  exple1t 6538  expubndt 6539  sqlecant 6572  subsqt 6573  bernneq 6583  expnbndt 6585  rpsqrclt 6645  cjclt 6696  imret 6710  reim0t 6711  cjexpt 6752  recjt 6753  imcjt 6754  cj11t 6765  absclt 6768  absvalsqt 6770  absreimt 6792  absdivz 6794  absexpt 6803  absrelet 6804  absimlet 6805  recvalz 6825  cjdiv 6826  absidmt 6830  abssubge0t 6833  abs3dift 6836  abs2difabst 6840  seq1ub 6849  cvg2 6859  caubnd 6863  ser1absdiflem 6866  ser1absdif 6867  facdivt 6879  facndivt 6880  faclbnd 6882  faclbnd2 6883  faclbnd3 6884  faclbnd4lem3 6887  faclbnd5 6890  faclbnd6 6891  facavgt 6892  bcval2t 6897  bccmplt 6900  bcn0t 6901  bcnp11t 6903  bcnp1nt 6904  bccl2t 6909  bcclt 6910  permnnt 6911  dffsum 6936  fsump1s 6951  fsumcllem 6952  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsumrev2 6968  fsumshft 6969  fsummulc1 6971  fsumdivcALT 6974  fsum0 6977  fsumcmp 6978  fsumcmpndx2 6980  fsumabs 6981  serz1p 6990  serzrelem 6999  binomlem1 7004  binomlem2 7005  binomlem4 7007  binomlem5 7008  bcxmas 7014  clm4le 7019  2climnn 7039  2climnn0 7040  climrecl 7047  climge0 7049  climaddlem3 7052  climaddc1 7054  climmullem1 7056  climmullem2 7057  climmullem3 7058  climmullem4 7059  climmullem5 7060  climmullem8 7063  climmulc2 7065  climsub 7066  climsubc2 7067  climcmplem 7073  clim2serz 7081  climserzle 7083  climcj 7086  climubi 7089  climsup 7091  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  ser1cmp 7110  ser1cmp2 7113  cvgcmp2lem 7116  cvgcmp2clem 7118  isum1p 7141  iserzgt0 7146  isummulc1ALT 7148  reccnv 7153  infcvglem1 7156  infcvglem3 7158  fnsmnt 7161  geoser 7169  georeclim 7175  geoisumr 7178  geoisum1c 7180  0.999... 7181  cvgratlem2ALT 7183  cvgratlem1 7185  cvgratlem2 7186  cvgratlem4 7188  cvgratlem5 7189  fsum0diaglem1 7191  fsum0diaglem2 7192  fsum0diag2 7194  elcncf1d 7205  cjcncf 7213  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  efcltlem1 7246  efcltlem2 7247  ef0lem 7252  efseq0ex 7253  erelem1 7261  erelem3 7263  efaddlem3 7282  efaddlem5 7284  efaddlem6 7285  efaddlem10 7289  efaddlem15 7294  efaddlem16 7295  efaddlem17 7296  efaddlem18 7297  efaddlem19 7298  efaddlem23 7302  efaddlem25 7304  efaddlem27 7306  eff2 7312  efsubt 7313  efexpt 7314  eftabs 7317  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  eirrlem4 7333  abspef01tlub 7336  efgt1 7344  absefm1le 7352  eflegeolem1 7353  efcnlem2 7360  efcn 7363  reeff1o 7368  efi4pt 7377  resin4pt 7378  recos4pt 7379  sinnegt 7384  cosnegt 7385  efivalt 7389  efmivalt 7390  efeult 7391  sinsubt 7397  cossubt 7398  addsint 7399  subcost 7402  sincossqt 7403  sin2tt 7404  cos2tt 7405  sinbndt 7407  cosbndt 7408  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  sin01gt0 7418  cos01gt0 7419  sin02gt0 7420  absefit 7424  abseft 7425  demoivre 7426  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  acdcALT 7438  xpnnen 7441  znnenlem 7443  znnenlemOLD 7444  unbenlem 7447  infpnlem2 7450  ruclem4 7456  ruclem13 7465  infxpidmlem1 7495  infxpidmlem11 7505  infxpidmlem12 7506  infunabs 7508  infcdaabs 7509  infcda 7510  infdif 7511  infxp 7515  alephexp1 7526  alephsuc3 7527  tgval3t 7567  topbast 7569  basgen2t 7581  cctop 7594  ntrval 7618  clsval 7619  clsss 7629  elcls 7646  clsndisj 7648  neival 7658  neiss 7664  neips 7668  unnei 7676  lpval 7684  cnpcl 7703  cnco 7707  cnpco 7708  iscncl 7709  cnsscnp 7711  cncnplem2 7714  cnconst 7719  metsym 7755  metge0 7760  metxplem3 7768  metxpdval 7769  metxptval 7770  metxpfval 7771  metxp 7774  bl2in 7783  blex 7789  blss 7793  blssex 7794  ssblex 7796  opnm 7800  opnin 7809  neibl 7817  lpbl 7819  methausi 7820  metcnconst 7824  metcnplem 7825  metcnp 7826  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnp3 7835  metcnss 7837  bl2ioo 7850  ioo2bl 7851  blssioo 7852  tgioolem 7853  lmfval 7863  lmconst 7872  lmnn 7873  iscau3 7876  lmuni 7886  lmle 7895  metelcls 7900  metcld 7901  metcnp4 7904  xplmi 7907  xplm 7909  xpcn 7910  bopcnlem2 7916  fsumcnlem 7923  iscms2lem3 7925  lmcau 7930  cmsss 7931  cncms 7932  bcthlem1 7933  bcthlem2 7934  bcthlem7 7939  bcthlem8 7940  bcthlem13 7945  bcthlem14 7946  bcthlem18 7950  bcthlem19 7951  bcthlem20 7952  bcthlem21 7953  bcthlem24 7956  bcthlem25 7957  bcthlem26 7958  bcthlem30 7962  isgrpi 7976  grpidinvlem3 7984  grpidinvlem4 7985  grpidinv 7986  grpidinv2 7994  grpinvval 8001  grpinv 8003  grpinvf 8014  grpinvop 8015  grpdivfval 8016  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  grplactf1o 8034  subgid 8057  subgabl 8060  ghgrpilem3 8072  vcm 8127  invfval 8201  nvmul0or 8212  nvpncan2 8216  nvnncan 8223  nvdif 8232  nvpi 8233  nvabs 8240  nvge0 8241  nvgt0 8242  nv1 8243  imsdf 8258  imsmetlem 8261  nvlmle 8268  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  ipval2lem2 8288  ipval2 8291  4ipval2 8292  ipval2lem5 8294  4ipval3 8296  ipnm 8298  ipcl 8299  ipcj 8301  ip1cnilem4 8310  ip1cnilem5 8311  ip1cnilem6 8312  sspg 8321  ssps 8323  sspmlem 8325  sspz 8328  sspn 8329  lno0 8351  lnomul 8354  nmosetn0 8360  nmoge0 8362  nmoub3i 8368  nmo0 8383  nmlno0lem 8385  nmlnogt0 8389  nmblolbii 8390  isblo3i 8392  blometi 8394  blocnilem 8395  blocni 8396  phpar 8414  ipasslem1 8421  ipasslem2 8422  ipasslem4 8424  ipasslem8 8428  ipasslem9 8429  ipdi 8434  ipassr 8437  ipsubdir 8439  ipsubdi 8440  ip2eqi 8448  ubthlem3 8462  ubthlem7 8466  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  ubthlem12 8471  ubthlem13 8472  ubthlem14 8473  minveclem9 8484  minveclem16 8491  minveclem21 8496  minveclem25 8500  minveclem30 8505  minveclem31 8506  minveclem36 8511  minveclem38 8513  hlipgt0 8546  htthlem7 8556  htthlem9 8558  htthlem11 8560  spwval2 8577  sincolem 8584  sinperlem1 8605  sinperlem2 8606  efimpi 8615  cosh111lem1 8629  efif 8636  efifolem5 8641  efifolem7 8643  efielcircOLD 8655  circgrpOLD 8658  efielcirc 8659  shftefif1olem 8661  shftefif1olemOLD 8662  eff1lem 8664  eff1i 8665  effoi 8666  effoiOLD 8667  resslogrn 8675  reeflogt 8683  relogeftb 8687  h2hcau 8788  hvpncant 8829  hvsubdistr1t 8837  hvsubdistr2t 8838  hvmulcant 8860  hvmulcan2t 8861  hvsubcan2t 8863  his2subt 8879  his6t 8886  hi2eqt 8892  normf 8910  normge0t 8913  normgt0tOLD 8914  normgt0t 8915  norm-it 8917  hhph 8966  bcsALT 8967  hcau2 8976  hhcms 8993  norm1t 9042  norm1ex 9043  hhssnv 9054  hhsscms 9067  chocuni 9088  occllem6 9094  projlem2 9103  projlem25 9126  projlem26 9127  projlem28 9129  projlem30 9131  pjthlem7 9140  pjthlem10 9143  pjpot 9176  hsupval2t 9215  spanssoc 9234  pjspansnt 9417  spanunsn 9419  h1datom 9421  fh1t 9478  fh2t 9479  cm2jt 9480  osumlem6 9500  osumlem7 9501  nonbool 9513  spansncv 9514  5oalem1 9516  5oalem2 9517  3oalem2 9525  pjidt 9557  pjrn 9564  pjft 9570  pjnorm2t 9589  mayete3 9590  hosubcl 9612  hoaddcom 9615  honegsub 9639  homco1t 9644  homulasst 9645  hoadddit 9646  hoadddirt 9647  adjsymt 9676  eigpos 9679  cnvadj 9733  hhlno 9743  nmoplbt 9748  nmopub2tALT 9750  nmopge0t 9751  nmopgt0t 9752  unoplint 9760  hmopret 9763  nmfnlbt 9764  nmfnleub2t 9766  nmfnge0t 9767  adj2t 9774  adjadjt 9776  adjvalvalt 9777  hmoplint 9782  kbpjt 9796  eigvalclt 9801  eighmret 9803  eighmortht 9804  homco2t 9817  hoddi 9829  nmlnop0ALT 9835  lnophs 9841  lnopeq 9848  nmopunt 9854  nmbdoplb 9864  nmcopexlem3 9868  nmcopexlem5 9870  nmcopexlem6 9871  nmcoplb 9873  nmophm 9876  lnopcon 9878  lnopcnbdt 9880  nmbdfnlb 9893  nmcfnexlem3 9897  nmcfnexlem5 9899  nmcfnexlem6 9900  nmcfnlb 9902  lnfncon 9905  lnfncnbdt 9907  riesz3 9910  cnlnadjlem2 9916  cnlnadjlem5 9919  cnlnadjlem6 9920  cnlnadjlem7 9921  adjbdlnt 9931  adjbd1o 9933  adjlnopt 9934  nmopadjlem 9937  nmoptri 9941  nmopco 9942  nmopcoadj 9948  branmfnt 9951  cnvbravalt 9956  kbass2t 9962  leop2t 9969  leop3t 9970  leoprf2t 9972  leopmult 9979  leopmul2it 9980  leoptrit 9981  leopnmidt 9982  nmopleidt 9983  pjnmop 9986  hmopidmchlem 9989  hmopidmch 9990  hmopidmpj 9991  pjsdi 9994  pjddi 9995  pjss2co 10003  pjsspos 10011  pjhmopidm 10020  pjclem4 10037  pj3s 10045  pj3cor1 10047  hstle1t 10063  hstlet 10067  sto2 10074  stadd 10083  stadd3 10085  strlem1 10087  strlem3a 10089  strlem5 10092  str 10094  hstr 10102  jplem1 10105  golem1 10108  stcltrlem1 10113  mdslmd1lem1 10160  csmdsym 10169  cvdmdt 10172  atom1d 10188  superpos 10189  shatomic 10193  cvp 10210  irredlem2 10226  atcvat3 10231  atcvat4 10232  mdsymlem1 10238  mdsymlem2 10239  mdsymlem6 10243  cdj1 10265  cdj3lem2 10267  cdj3 10273  ghomgrpilem2 10291  ghomfo 10296  ghomid 10299  ghomf1olem 10301  cayleylem2 10317  fiv 10374  cdrci 10381  truni1 10386  homeofval 10403  hmeogrp 10425  qusp 10430  fipfil 10438  fipfil2 10439  fgsb 10444  efilcp 10445  fgsb2 10449  efilcp2 10450  cnfilca 10451  dmse1 10467  msr3 10469  mslb1 10473  2wsms 10474  msra3 10475  iintlem1 10476  trran 10480  trnij 10481  cnvtr 10482  rcmob 10526  imonclem 10583  icmpmon 10587
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