Theorem syl3anc 856

Description: A syllogism inference combined with contraction.

Hypotheses

Ref	Expression
syl3anc.1	|- ((ph /\ ps /\ ch) -> th)
syl3anc.2	|- (ta -> ph)
syl3anc.3	|- (ta -> ps)
syl3anc.4	|- (ta -> ch)

Assertion

Ref	Expression
syl3anc	|- (ta -> th)

Proof of Theorem syl3anc

Step	Hyp	Ref	Expression
1		syl3anc.2	. . 3 |- (ta -> ph)
2		syl3anc.3	. . 3 |- (ta -> ps)
3		syl3anc.4	. . 3 |- (ta -> ch)
4	1, 2, 3	3jca 817	. 2 |- (ta -> (ph /\ ps /\ ch))
5		syl3anc.1	. 2 |- ((ph /\ ps /\ ch) -> th)
6	4, 5	syl 10	1 |- (ta -> th)

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  syl3dan3 868  3jaod 885  mpd3an23 915  3anandis 917  3anandirs 918  csbnestglem 2025  csbnest1g 2027  fvelimab 3750  oaass 4179  omwordri 4187  oewordri 4203  oeordsuc 4205  2dom 4408  fodomr 4463  halfpq 5054  cnegextlem1 5317  cnegextlem3 5319  cnegext 5320  pncan3t 5349  npncant 5372  nppcant 5373  muladdt 5393  subdit 5399  ppncant 5453  letrd 5499  lelttrd 5500  ltletrd 5501  lttrd 5502  ltleaddt 5619  ltsubpost 5626  subge0t 5647  recextlem1 5655  recext 5657  divmuldivt 5736  divadddivt 5740  divdivdivt 5741  divdiv23t 5748  conjmult 5753  ltmul12it 5797  lemul12ait 5798  lediv12it 5844  recp1lt1 5849  ledivp1t 5853  xrmaxltt 5861  xrltmint 5862  maxlet 5866  lemint 5869  maxltt 5870  supxrun 6032  supxrmnf 6034  uzindOLD 6156  flval3t 6182  flwordit 6183  flhalft 6189  ceilet 6193  qaddclt 6207  qbtwnxr 6217  ser1add2 6275  ser1add 6276  uztrn 6360  infmssuzle 6397  elfzle3 6417  fzrevt 6443  fzrevral2t 6452  fsequb 6455  fseqsupcl 6457  seqzm1 6481  expaddt 6527  expmult 6528  expsubt 6529  divexpt 6530  expordit 6531  subsqt 6573  subsq2t 6574  bernneq 6583  bernneq2 6584  expnbndt 6585  reim0t 6711  imcjt 6754  absimlet 6805  seq1bnd 6847  cvg2 6859  cvganz 6861  caubnd 6863  caure 6864  cauim 6865  ser1absdiflem 6866  facdivt 6879  facwordit 6881  faclbnd 6882  faclbnd3 6884  faclbnd6 6891  facavgt 6892  bcval3t 6898  bccmplt 6900  bccl2t 6909  permnnt 6911  fsum1ps 6956  fsumsplit 6958  fsumcom 6966  fsumrev 6967  fsumshft 6969  fsummulc1 6971  fsumdivc 6973  fsumdivcALT 6974  fsumcmp 6978  fsumcmpndx2 6980  fsumabs 6981  ser1ser0 6986  binomlem1 7004  binomlem4 7007  binomlem5 7008  bcxmas 7014  2climnn 7039  2climnn0 7040  climmullem3 7058  climmullem4 7059  climmullem5 7060  climsqueeze 7076  climsqueeze2 7077  clim2serz 7081  climserzle 7083  climcau 7092  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  ser1cmp 7110  ser1cmp2lem 7112  ser1cmp2 7113  cvgcmp3c 7122  iserzgt0 7146  reccnv 7153  georeclim 7175  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag3 7195  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  eftclt 7245  efseq0ex 7253  reefcl 7259  efcj 7278  efaddlem3 7282  efaddlem6 7285  efaddlem14 7293  efaddlem17 7296  efaddlem19 7298  efaddlem23 7302  efaddlem25 7304  reeftclt 7316  eftabs 7317  eftlubclt 7318  reeftlclt 7322  ef01tllem1 7325  ef01tllem2 7326  absefm1le 7352  efcnlem2 7360  efcn 7363  efi4pt 7377  efivalt 7389  addsint 7399  subsint 7400  addcost 7401  subcost 7402  sin01bndlem3 7411  cos01bndlem3 7413  acdc3lem 7428  acdc2lem1 7430  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  tgss2t 7579  subbas2 7587  retopbas 7597  clscld 7625  elcls 7646  ntrcls0 7649  neissex 7679  clslp 7689  dnsconst 7727  blval 7777  blelrn 7788  blss 7793  opnuni 7808  tgbl 7811  blbas 7812  lpbl 7819  methausi 7820  metcnp 7826  metcnp2 7827  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metdnsconst 7840  ioo2bl 7851  tgioolem 7853  lmnn 7873  iscau3 7876  lmuni 7886  lmle 7895  metelcls 7900  metcnp4 7904  metcn4 7905  xplmi 7907  lmcau 7930  cmsss 7931  bcthlem2 7934  bcthlem11 7943  bcthlem21 7953  bcthlem24 7956  bcthlem25 7957  grpinvop 8015  grpdivdiv 8022  grpmuldivass 8023  grppnpcan2 8027  abldivdiv4 8046  subgres 8054  nvzs 8205  nvmf 8206  nvmdi 8210  nvpncan2 8216  nvaddsub4 8221  nvdif 8232  nvmtri2 8239  nvabs 8240  nv1 8243  imsdval 8255  imsmetlem 8261  nvcni 8266  nmcnilem 8272  ipval2lem2 8288  ipval2 8291  ipval2lem5 8294  sspn 8329  lnomul 8354  nvcnpi4 8355  nmoge0 8362  nmoubi 8367  nmoub3i 8368  nmblolbii 8390  isblo3i 8392  blocnilem 8395  blocni 8396  cnph 8409  ipasslem2 8422  ipasslem4 8424  ipasslem5 8425  ipdi 8434  ipassr 8437  ipsubdi 8440  siii 8444  ipblnfi 8447  ip2eqi 8448  ubthlem5 8464  ubthlem8 8467  ubthlem10 8469  ubthlem13 8472  minveclem18 8493  minveclem25 8500  minveclem27 8502  psasym 8576  sinq12gt0t 8625  efifolem7 8643  effoi 8666  effoiOLD 8667  hvmul0ort 8815  hvaddsub4t 8866  hcau2 8976  pjpjtht 9173  pjopt 9175  pjpot 9176  shscl 9196  shlej1t 9270  chabs1t 9354  spansncol 9407  normcant 9416  pjspansnt 9417  spanunsn 9419  spanpr 9420  pjoml5t 9473  pjot 9533  pjoi0t 9579  hods 9618  hoaddass 9619  hoadddit 9646  nmopubt 9749  nmopub2tALT 9750  cnvunopt 9758  unoplint 9760  nmfnleubt 9765  nmfnleub2t 9766  unopadj2t 9778  hmopadjt 9779  hmoplint 9782  bralnfnt 9788  kbmult 9795  kbpjt 9796  eigvalclt 9801  eighmortht 9804  lnopeq 9848  hmopst 9860  hmopmt 9861  hmopcot 9863  nmbdoplb 9864  nmcoplb 9873  nmophm 9876  lnopcon 9878  nmbdfnlb 9893  nmcfnlb 9902  lnfncon 9905  nlelch 9909  riesz3 9910  riesz4 9911  cnlnadjlem6 9920  adjlnopt 9934  adjmult 9939  adjaddt 9940  branmfnt 9951  kbass2t 9962  kbass3t 9963  kbass4t 9964  kbass5t 9965  leop2t 9969  leopsqt 9974  leopaddt 9977  leopmulit 9978  leopmult 9979  leopnmidt 9982  hmopidmch 9990  hmopidmpj 9991  pjsspos 10011  pjclem4 10037  pj3s 10045  hstpytht 10066  hstlet 10067  hstoht 10069  stadd 10083  stadd3 10085  strlem1 10087  golem1 10108  mdbr2 10133  dmdbr2 10140  mdslmd1lem1 10160  mdslmd1lem2 10161  superpos 10189  irredlem2 10226  irred 10229  atcvat3 10231  cdj1 10265  cdj3lem2b 10269  elo 10345  fine 10348  hmeogrp 10425  cnfilca 10451  msr3 10469  msr4 10470  mslb1 10473  2wsms 10474  msra3 10475  aidm 10527  aidmold 10528  imonclem 10583  ismonc 10584  cmpmon 10585  icmpmon 10587  idmon 10588

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  df-3an 775

Copyright terms: Public domain