Theorem sylanc 471

Description: A syllogism inference combined with contraction.

Hypotheses

Ref	Expression
sylanc.1	⊢ ((φ ⋀ ψ) → χ)
sylanc.2	⊢ (θ → φ)
sylanc.3	⊢ (θ → ψ)

Assertion

Ref	Expression
sylanc	⊢ (θ → χ)

Proof of Theorem sylanc

Step	Hyp	Ref	Expression
1		sylanc.1	. . 3 ⊢ ((φ ⋀ ψ) → χ)
2	1	ex 373	. 2 ⊢ (φ → (ψ → χ))
3		sylanc.2	. 2 ⊢ (θ → φ)
4		sylanc.3	. 2 ⊢ (θ → ψ)
5	2, 3, 4	sylc 68	1 ⊢ (θ → χ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  syl2anc 472  sylancom 475  anim12d 557  orim12d 564  pm5.21ni 677  ax11indalem 1367  ax11inda2ALT 1368  eueq2 1915  eueq3 1916  sbc2or 1955  sstrd 2071  ralidm 2354  raaan 2357  sspr 2472  exss 2765  reuuniss 2885  reuuniss2 2887  reuunixfr 2902  ordelord 2966  onfr 2982  onnmin 3011  onminex 3016  onmindif2 3057  ordunel 3080  limsssuc 3117  peano5 3149  unixp 3513  cnvexg 3515  cnvpo 3518  cofunexg 3576  funfni 3584  fnresdm 3592  fnex 3603  fconstg 3654  f1ores 3698  fimacnv 3805  dff2 3812  fconst3 3845  f1ocnvfv3 3878  tfrlem10 3915  tfrlem12 3917  oprabex2g 4015  sbcopeq1a 4104  csbopeq1a 4105  dfoprab4 4109  oesuc 4159  odi 4203  oewordri 4212  oeworde 4213  oelim2 4215  en2d 4390  undom 4427  xpdom1 4432  sbthlem8 4443  2pwuninel 4476  limenpsi 4494  limensuci 4495  php3 4504  unblem4 4529  unbnn 4530  unifi 4541  fodomfi 4549  iunfi 4552  pwfilem 4553  supub 4563  suplub 4564  supmax 4572  suppr 4573  noinfep 4623  r1ord 4638  rankr1 4657  rankxplim3 4697  fodom 4781  unidom 4791  uniimadom 4793  unxpdomlem 4826  unxpdom2 4828  cardalephex 4869  alephval2 4885  alephval3 4886  cfsuc 4898  cdafi 4919  axrepnd 4929  indpi 5017  halfpq 5065  ltaddpr 5123  ltexprlem2 5126  negexsr 5194  mulgt0sr 5197  axmulopr 5249  axcnre 5269  cnegext 5331  nnncan1t 5450  mulsubt 5460  pm2.61ltle 5517  lecase 5605  posdift 5637  recextlem2 5666  recext 5667  muleqaddt 5679  recid2t 5709  divrec2t 5713  div23t 5715  div12t 5717  divsubdirt 5741  divcan5t 5747  divdivdivt 5751  divcan6t 5757  divdiv23t 5758  divdivmult 5761  conjmult 5763  lemul1t 5798  ltmul12it 5807  lt2mul2divt 5832  lemuldivt 5834  lt2msq 5839  lediv2t 5849  lediv12it 5854  lediv2it 5855  recp1lt1 5859  recrecltt 5860  ledivp1t 5863  ledivp1 5864  ltdivp1 5865  nnge1t 5901  nngt1ne1t 5902  nndivtrt 5917  halfaddsubt 5998  lt2halvest 5999  avglet 6001  lbinfm 6005  infm3lem 6010  suprub 6013  infmrcl 6026  nnreclt 6029  xrub 6037  supxrre 6040  supxrunb1 6046  supxrbnd 6048  supxrub 6055  nn0ltp1let 6084  zltp1let 6138  z2get 6145  gtndivt 6150  flidt 6192  flval2t 6194  flval3t 6195  fladdzt 6199  flhalft 6201  qaddclt 6219  qmulclt 6221  qbtwnxr 6229  rpne0t 6238  rpdivclt 6242  seq1lem2 6260  ser1mono 6287  shftval2t 6297  shftval5t 6300  2shft 6302  shftcan2t 6303  iooint 6322  iccsupr 6344  icoshft 6354  icoshftf1oi 6355  uznegit 6374  uzind4 6395  infmssuzcl 6411  eluzfz1t 6432  eluzfz2t 6434  fznn0sub2t 6444  fzelp1t 6453  elfzp1 6455  fzrev2it 6458  fzrev3t 6459  fzneuzt 6463  fsequb 6468  fsequb2 6469  fseqsupub 6471  seqzp1 6493  seqzfveq 6499  seqzres 6505  seqzres2 6506  expeq0t 6530  expgt0t 6534  mulexpt 6539  recexpt 6540  expaddt 6541  expsubt 6543  expordit 6545  expwordit 6548  expord2t 6549  expmwordit 6551  exple1t 6552  expubndt 6553  sqlecant 6586  subsqt 6587  bernneq 6597  expnbndt 6599  expnlbndt 6600  rpsqrclt 6660  cjclt 6711  imret 6725  reim0t 6726  cjexpt 6767  recjt 6768  imcjt 6769  cj11t 6780  absclt 6783  absvalsqt 6785  absreimt 6807  absdivz 6809  absexpt 6818  absrelet 6819  absimlet 6820  recvalz 6840  cjdiv 6841  absidmt 6845  abssubge0t 6848  abs3dift 6851  abs2difabst 6855  seq1ub 6864  cvg2 6874  caubnd 6878  ser1absdiflem 6881  ser1absdif 6882  facdivt 6894  facndivt 6895  faclbnd 6897  faclbnd2 6898  faclbnd3 6899  faclbnd4lem3 6902  faclbnd5 6905  faclbnd6 6906  facavgt 6907  bcval2t 6912  bccmplt 6915  bcn0t 6916  bcnp11t 6918  bcnp1nt 6919  bccl2t 6924  bcclt 6925  permnnt 6926  dffsum 6951  fsump1s 6966  fsumcllem 6967  fsumsplit 6973  fsumadd 6975  fsumcom 6981  fsumrev 6982  fsumrev2 6983  fsumshft 6984  fsummulc1 6986  fsumdivcALT 6989  fsum0 6992  fsumcmp 6993  fsumcmpndx2 6995  fsumabs 6996  serz1p 7005  serzrelem 7014  binomlem1 7019  binomlem2 7020  binomlem4 7022  binomlem5 7023  bcxmas 7029  clm4le 7034  2climnn 7055  2climnn0 7056  climrecl 7063  climge0 7065  climaddlem3 7069  climaddc1 7071  climmullem1 7073  climmullem2 7074  climmullem3 7075  climmullem4 7076  climmullem5 7077  climmullem8 7080  climmulc2 7082  climsub 7083  climsubc2 7084  climcmplem 7090  clim2serz 7098  climserzle 7100  climcj 7103  climubi 7106  climsup 7108  caucvglem6 7115  caucvg 7116  serzf0 7122  ser1f0 7123  ser1cmp 7127  ser1cmp2 7130  cvgcmp2lem 7133  cvgcmp2clem 7135  isum1p 7158  iserzgt0 7163  isummulc1ALT 7165  reccnv 7170  infcvglem1 7173  infcvglem3 7175  fnsmnt 7178  geoser 7186  georeclim 7192  geoisumr 7195  geoisum1c 7197  0.999... 7198  cvgratlem2ALT 7200  cvgratlem1 7202  cvgratlem2 7203  cvgratlem4 7205  cvgratlem5 7206  fsum0diaglem1 7208  fsum0diaglem2 7209  fsum0diag2 7211  elcncf1d 7222  cjcncf 7230  ivthlem6 7238  ivthlem7 7239  ivthlem6OLD 7247  ivthlem7OLD 7248  efcltlem1 7263  efcltlem2 7264  ef0lem 7269  efseq0ex 7270  erelem1 7278  erelem3 7280  efaddlem3 7299  efaddlem5 7301  efaddlem6 7302  efaddlem10 7306  efaddlem15 7311  efaddlem16 7312  efaddlem17 7313  efaddlem18 7314  efaddlem19 7315  efaddlem23 7319  efaddlem25 7321  efaddlem27 7323  eff2 7329  efsubt 7330  efexpt 7331  eftabs 7334  ef1tllem 7340  ef01tllem1 7342  ef01tllem2 7343  eirrlem4 7350  abspef01tlub 7353  efgt1 7361  absefm1le 7369  eflegeolem1 7370  efcnlem2 7377  efcn 7380  reeff1o 7385  efi4pt 7394  resin4pt 7395  recos4pt 7396  sinnegt 7401  cosnegt 7402  efivalt 7406  efmivalt 7407  efeult 7408  sinsubt 7414  cossubt 7415  addsint 7416  subcost 7419  sincossqt 7420  sin2tt 7421  cos2tt 7422  sinbndt 7424  cosbndt 7425  sin01bndlem2 7427  sin01bndlem3 7428  cos01bndlem2 7429  cos01bndlem3 7430  sin01gt0 7435  cos01gt0 7436  sin02gt0 7437  absefit 7441  abseft 7442  demoivre 7443  acdc3lem 7445  acdc2lem2 7448  acdc5lem2 7451  acdclem 7453  acdcALT 7455  znnenlem 7460  znnenlemOLD 7461  unbenlem 7464  infpnlem2 7467  ruclem4 7473  ruclem13 7482  infxpidmlem1 7512  infxpidmlem11 7522  infxpidmlem12 7523  infunabs 7525  infcdaabs 7526  infcda 7527  infdif 7528  infxp 7532  alephexp1 7544  alephsuc3 7545  tgval3t 7585  topbast 7587  basgen2t 7599  ntrval 7636  clsval 7637  clsss 7647  elcls 7664  clsndisj 7666  neival 7677  neiss 7683  neips 7687  unnei 7695  lpval 7703  iscnp2 7721  cnpcl 7724  cnco 7728  cnpco 7729  iscncl 7730  cnsscnp 7732  cncnplem2 7735  cnconst 7740  metsym 7776  metge0 7781  metxplem3 7790  metxpdval 7791  metxptval 7792  metxpfval 7793  metxp 7796  bl2in 7805  blex 7811  blss 7815  blssex 7816  ssblex 7818  opnm 7822  opnin 7831  neibl 7839  lpbl 7842  methausi 7843  metcnconst 7847  metcnplem 7848  metcnp 7849  metcnpi3 7854  metcnpi4 7855  metcni2 7857  metcnp3 7858  metcnss 7860  bl2ioo 7873  ioo2bl 7874  blssioo 7875  tgioolem 7876  lmfval 7887  lmconst 7896  lmnn 7897  iscau3 7900  iscau4 7902  lmuni 7913  lmle 7922  metelcls 7927  metcld 7929  metcnp4 7932  xplmi 7935  xplm 7937  xpcn 7938  bopcnlem2 7944  fsumcnlem 7951  iscms2lem3 7953  lmcau 7958  cmsss 7959  cncms 7960  bcthlem1 7961  bcthlem2 7962  bcthlem7 7967  bcthlem8 7968  bcthlem13 7973  bcthlem14 7974  bcthlem18 7978  bcthlem19 7979  bcthlem20 7980  bcthlem21 7981  bcthlem24 7984  bcthlem25 7985  bcthlem26 7986  bcthlem30 7990  isgrpi 8004  grpidinvlem3 8012  grpidinvlem4 8013  grpidinv 8014  grpidinv2 8022  grpinvval 8029  grpinv 8031  grpinvf 8041  grpinvop 8042  grpdivfval 8043  grppncan 8052  grpnpcan 8053  grppnpcan2 8054  grplactf1o 8061  subgid 8084  subgabl 8087  ghgrpilem3 8099  vcm 8154  invfval 8225  nvmul0or 8236  nvpncan2 8240  nvnncan 8247  nvdif 8257  nvpi 8258  nvabs 8265  nvge0 8266  nvgt0 8267  nv1 8268  imsdf 8284  imsmetlem 8287  nvlmle 8296  nmcnilem 8300  va1cnlem 8307  sm1cnilem 8309  ipval2lem2 8316  ipval2 8319  4ipval2 8320  ipval2lem5 8322  4ipval3 8324  ipnm 8326  ipcl 8327  ipcj 8329  ip1cnilem4 8338  ip1cnilem5 8339  ip1cnilem6 8340  sspg 8349  ssps 8351  sspmlem 8353  sspz 8356  sspn 8357  lno0 8379  lnomul 8382  nmosetn0 8388  nmoge0 8390  nmoub3i 8396  nmo0 8411  nmlno0lem 8413  nmlnogt0 8417  nmblolbii 8418  isblo3i 8420  blometi 8422  blocnilem 8423  blocni 8424  phpar 8442  ipasslem2 8450  ipasslem4 8452  ipasslem8 8456  ipasslem9 8457  ipdi 8462  ipassr 8465  ipsubdir 8467  ipsubdi 8468  ip2eqi 8476  ubthlem3 8490  ubthlem7 8494  ubthlem8 8495  ubthlem9 8496  ubthlem10 8497  ubthlem11 8498  ubthlem12 8499  ubthlem13 8500  ubthlem14 8501  minveclem9 8512  minveclem16 8519  minveclem21 8524  minveclem25 8528  minveclem30 8533  minveclem31 8534  minveclem36 8539  minveclem38 8541  hlipgt0 8574  htthlem7 8584  htthlem9 8586  htthlem11 8588  spwval2 8610  sincolem 8619  sinperlem1 8640  sinperlem2 8641  efimpi 8650  cosh111lem1 8664  efif 8671  efifolem5 8676  efifolem7 8678  efielcircOLD 8690  circgrpOLD 8693  efielcirc 8694  shftefif1olem 8696  eff1lem 8698  eff1i 8699  effoi 8700  resslogrn 8708  reeflogt 8716  relogeftb 8720  h2hcau 8804  hvsubdistr1t 8871  hvsubdistr2t 8872  hvmulcant 8894  hvmulcan2t 8895  hvsubcan2t 8897  his2subt 8913  his6t 8920  hi2eqt 8926  normf 8944  normge0t 8947  normgt0tOLD 8948  normgt0t 8949  norm-it 8951  hhph 9000  bcsALT 9001  hcau2 9010  hhcms 9027  norm1t 9076  norm1ex 9077  hhssnv 9089  hhsscms 9105  chocuni 9127  occllem6 9133  projlem2 9142  projlem25 9165  projlem26 9166  projlem28 9168  projlem30 9170  pjthlem7 9180  pjthlem10 9183  pjpot 9216  hsupval2t 9255  spanssoc 9274  pjspansnt 9457  spanunsn 9459  h1datom 9461  fh1t 9518  fh2t 9519  cm2jt 9520  osumlem6 9540  osumlem7 9541  nonbool 9553  spansncv 9554  5oalem1 9556  5oalem2 9557  3oalem2 9565  pjrn 9604  pjft 9610  pjnorm2t 9629  mayete3 9630  hosubcl 9652  hoaddcom 9655  honegsub 9679  homco1t 9684  homulasst 9685  hoadddit 9686  hoadddirt 9687  adjsymt 9716  eigpos 9719  cnvadj 9773  hhlno 9783  nmoplbt 9788  nmopub2tALT 9790  nmopge0t 9792  nmopgt0t 9793  unoplint 9801  nmfnlbt 9805  nmfnleub2t 9807  nmfnge0t 9808  adj2t 9815  adjadjt 9817  adjvalvalt 9818  hmoplint 9823  kbpjt 9837  eighmret 9844  eighmortht 9845  homco2t 9858  hoddi 9870  nmlnop0ALT 9876  lnophs 9882  lnopeq 9889  nmopunt 9895  nmbdoplb 9905  nmcopexlem3 9909  nmcopexlem5 9911  nmcopexlem6 9912  nmcoplb 9914  nmophm 9917  lnopcon 9919  lnopcnbdt 9921  nmbdfnlb 9934  nmcfnexlem3 9938  nmcfnexlem5 9940  nmcfnexlem6 9941  nmcfnlb 9943  lnfncon 9946  lnfncnbdt 9948  riesz3 9951  cnlnadjlem2 9957  cnlnadjlem5 9960  cnlnadjlem6 9961  cnlnadjlem7 9962  adjbdlnt 9972  adjbd1o 9974  adjlnopt 9975  nmopadjlem 9978  nmoptri 9983  nmopco 9984  nmopcoadj 9990  branmfnt 9994  cnvbravalt 9999  kbass2t 10006  leop2t 10013  leop3t 10014  leoprf2t 10016  leopmult 10023  leopmul2it 10024  leoptrit 10025  leopnmidt 10027  nmopleidt 10028  pjnmop 10031  hmopidmchlem 10034  hmopidmch 10035  hmopidmpj 10036  pjsdi 10039  pjddi 10040  pjss2co 10048  pjsspos 10056  pjhmopidm 10066  pjclem4 10083  pj3s 10091  pj3cor1 10093  hstle1t 10109  hstlet 10113  sto2 10120  stadd 10129  stadd3 10131  strlem1 10133  strlem3a 10135  strlem5 10138  strlem6 10139  str 10140  hstrlem6 10147  hstr 10148  jplem1 10151  golem1 10154  stcltrlem1 10159  dmdbr5 10191  mdslmd1lem1 10208  csmdsym 10217  cvdmdt 10220  atom1d 10236  superpos 10237  shatomic 10241  irredlem2 10274  atcvat3 10279  atcvat4 10280  mdsymlem1 10286  mdsymlem2 10287  mdsymlem6 10291  cdj1 10316  cdj3lem2 10318  cdj3 10324  ghomgrpilem2 10342  ghomfo 10347  ghomid 10350  ghomf1olem 10352  cayleylem2 10366  gelsupvalOLD 10376  nnssi3 10378  nndivlub 10380  fiv 10433  cdrci 10440  truni1 10445  homeofval 10462  hmeogrp 10484  qusp 10489  fipfil 10497  fipfil2 10498  fgsb 10503  efilcp 10504  fgsb2 10508  efilcp2 10509  cnfilca 10510  dmse1 10539  msr3 10541  mslb1 10545  2wsms 10546  msra3 10547  iintlem1 10548  trran 10552  trnij 10553  cnvtr 10554  rcmob 10598  imonclem 10655  icmpmon 10659

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