Theorem syl3anc 858

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 819	. 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 775

This theorem is referenced by:  syld3an3 870  3jaod 888  mpd3an23 918  3anandis 920  3anandirs 921  csbnestglem 2033  csbnest1g 2035  fvelimab 3763  oaass 4193  omwordri 4201  oewordri 4217  oeordsuc 4219  2dom 4422  fodomr 4477  halfpq 5070  cnegextlem1 5333  cnegextlem3 5335  cnegext 5336  pncan3t 5365  nppcant 5389  muladdt 5409  subdit 5415  letrd 5514  lelttrd 5515  ltletrd 5516  lttrd 5517  ltleaddt 5633  ltsubpost 5640  subge0t 5661  recextlem1 5669  recext 5671  divmuldivt 5751  divadddivt 5755  divdivdivt 5756  divdiv23t 5763  conjmult 5768  ltmul12it 5812  lemul12ait 5813  ltdivmult 5838  lediv12it 5864  recp1lt1 5869  ledivp1t 5873  xrmaxltt 5881  xrltmint 5882  maxlet 5886  lemint 5889  maxltt 5890  supxrun 6053  supxrmnf 6055  uzindOLD 6176  flwordit 6204  flval3t 6206  flhalft 6213  ceilet 6217  quorem 6218  qaddclt 6233  qbtwnxr 6243  ser1add2 6302  ser1add 6303  uztrn 6388  infmssuzle 6425  elfzle3 6445  fzrevt 6471  fzrevral2t 6480  fsequb 6483  fseqsupcl 6485  seqzm1 6509  expaddt 6556  expmult 6557  expsubt 6558  divexpt 6559  expordit 6560  subsqt 6602  subsq2t 6603  bernneq 6612  bernneq2 6613  expnbndt 6614  expnlbndt 6615  reim0t 6734  imcjt 6777  absimlet 6828  absmaxt 6855  seq1bnd 6868  cvg2 6880  cvganz 6882  caubnd 6884  caure 6885  cauim 6886  ser1absdiflem 6887  facdivt 6900  facwordit 6902  faclbnd 6903  faclbnd3 6905  faclbnd6 6912  facavgt 6913  bcval3t 6918  bccmplt 6920  bccl2t 6929  permnnt 6931  fsum1ps 6976  fsumsplit 6978  fsumcom 6986  fsumrev 6987  fsumshft 6989  fsummulc1 6991  fsumdivc 6993  fsumdivcALT 6994  fsumcmp 6998  fsumcmpndx2 7000  fsumabs 7001  ser1ser0 7006  binomlem1 7024  binomlem4 7027  binomlem5 7028  bcxmas 7034  2climnn 7060  2climnn0 7061  climmullem3 7080  climmullem4 7081  climmullem5 7082  climsqueeze 7098  climsqueeze2 7099  clim2serz 7103  climserzle 7105  climcau 7114  caucvglem6 7120  caucvg 7121  serzf0 7127  ser1f0 7128  ser1cmp 7132  ser1cmp2lem 7134  ser1cmp2 7135  cvgcmp3c 7144  iserzgt0 7169  reccnv 7176  georeclim 7198  cvgratlem1ALT 7205  cvgratlem1 7208  cvgratlem5 7212  fsum0diaglem2 7215  fsum0diag2 7217  fsum0diag3 7218  ivthlem6 7244  ivthlem7 7245  eftclt 7261  efseq0ex 7269  reefcl 7275  efcj 7294  efaddlem3 7298  efaddlem6 7301  efaddlem14 7309  efaddlem17 7312  efaddlem19 7314  efaddlem23 7318  efaddlem25 7320  reeftclt 7332  eftabs 7333  eftlubclt 7334  reeftlclt 7338  ef01tllem1 7341  ef01tllem2 7342  ef01tllem2OLD 7343  absefm1le 7369  efcnlem2 7377  efcn 7380  efi4pt 7392  efivalt 7404  addsint 7414  subsint 7415  addcost 7416  subcost 7417  sin01bndlem3 7426  cos01bndlem3 7428  acdc3lem 7443  acdc2lem1 7445  acdc2lem2 7446  acdc5lem2 7449  acdclem 7451  tgss2t 7594  subbas2 7602  retopbas 7612  clscld 7640  elcls 7661  ntrcls0 7664  neissex 7695  clslp 7705  dnsconst 7745  blval 7794  blelrn 7805  blss 7810  opnuni 7825  tgbl 7828  blbas 7829  lpbl 7837  methausi 7838  metcnp 7844  metcnp2 7845  metcnpi3 7849  metcnpi4 7850  metcni2 7852  metdnsconst 7858  ioo2bl 7869  tgioolem 7871  lmnn 7892  iscau3 7895  iscau4 7897  lmuni 7908  lmle 7917  metelcls 7922  metcnp4 7927  metcn4 7928  xplmi 7930  lmcau 7953  cmsss 7954  bcthlem2 7957  bcthlem11 7966  bcthlem21 7976  bcthlem24 7979  bcthlem25 7980  grpinvop 8037  grpdivdiv 8044  grpmuldivass 8045  grppnpcan2 8049  abldivdiv4 8066  subgres 8074  nvzs 8222  nvmf 8223  nvmdi 8227  nvpncan2 8233  nvaddsub4 8238  nvdif 8250  nvmtri2 8257  nvabs 8258  nv1 8261  imsdval 8274  imsmetlem 8280  nvcni 8286  nvcni2 8287  nmcnilem 8294  ipval2lem2 8311  ipval2 8314  ipval2lem5 8317  sspn 8352  lnomul 8378  nvcnpi3 8379  nvcnpi4 8380  nmoge0 8387  nmoubi 8392  nmoub3i 8393  nmblolbii 8416  isblo3i 8418  blocnilem 8421  blocni 8422  cnph 8435  ipasslem2 8448  ipasslem4 8450  ipasslem5 8451  ipdi 8460  ipassr 8463  ipsubdi 8466  siii 8470  ipblnfi 8473  ip2eqi 8474  ubthlem5 8490  ubthlem8 8493  ubthlem10 8495  ubthlem13 8498  minveclem18 8519  minveclem25 8526  minveclem27 8528  psasym 8608  pstr 8609  spwpr3OLD 8619  spwpr4OLD 8620  spwpr4aOLD 8621  sinq12gt0t 8665  efifolem7 8683  effoi 8700  hvmul0ort 8849  hvaddsub4t 8900  hcau2 9010  pjpjtht 9213  pjopt 9215  pjpot 9216  shscl 9236  shlej1t 9310  chabs1t 9394  spansncol 9446  normcant 9454  pjspansnt 9455  spanunsn 9457  spanpr 9458  pjoml5t 9511  pjot 9571  pjoi0t 9617  hods 9656  hoaddass 9657  hoadddit 9684  nmopubt 9787  nmopub2tALT 9788  cnvunopt 9797  unoplint 9799  nmfnleubt 9804  nmfnleub2t 9805  unopadj2t 9817  hmopadjt 9818  hmoplint 9821  bralnfnt 9827  kbmult 9834  kbpjt 9835  eigvalclt 9840  eighmortht 9843  lnopeq 9888  hmopst 9900  hmopmt 9901  hmopcot 9903  nmbdoplb 9904  nmcoplb 9913  nmophm 9916  lnopcon 9918  nmbdfnlb 9933  nmcfnlb 9942  lnfncon 9945  nlelch 9949  riesz3 9950  riesz4 9951  cnlnadjlem6 9960  adjlnopt 9974  adjmult 9980  adjaddt 9981  branmfnt 9993  kbass2t 10005  kbass3t 10006  kbass4t 10007  kbass5t 10008  leop2t 10012  leopsqt 10017  leopaddt 10020  leopmulit 10021  leopmult 10022  leopnmidt 10026  hmopidmch 10034  hmopidmpj 10035  pjsspos 10055  pjclem4 10082  pj3s 10090  hstpytht 10111  hstlet 10112  hstoht 10114  stadd 10128  stadd3 10130  strlem1 10132  golem1 10153  mdbr2 10178  dmdbr2 10185  mdslmd1lem1 10207  mdslmd1lem2 10208  superpos 10236  irredlem2 10273  irred 10276  atcvat3 10278  cdj1 10315  cdj3lem2b 10319  elo 10399  fine 10402  hmeogrp 10480  cnfilca 10506  rcfpfillem6 10512  msr3 10537  msr4 10538  mslb1 10541  2wsms 10542  msra3 10543  aidm 10595  aidmold 10596  imonclem 10651  ismonc 10652  cmpmon 10653  icmpmon 10655  idmon 10656

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 777

Copyright terms: Public domain