Theorem syl3anc 857

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 818	. 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 774

This theorem is referenced by:  syl3dan3 869  3jaod 886  mpd3an23 916  3anandis 918  3anandirs 919  csbnestglem 2031  csbnest1g 2033  fvelimab 3756  oaass 4185  omwordri 4193  oewordri 4209  oeordsuc 4211  2dom 4414  fodomr 4469  halfpq 5062  cnegextlem1 5325  cnegextlem3 5327  cnegext 5328  pncan3t 5357  npncant 5380  nppcant 5381  muladdt 5401  subdit 5407  ppncant 5461  letrd 5507  lelttrd 5508  ltletrd 5509  lttrd 5510  ltleaddt 5627  ltsubpost 5634  subge0t 5655  recextlem1 5663  recext 5665  divmuldivt 5744  divadddivt 5748  divdivdivt 5749  divdiv23t 5756  conjmult 5761  ltmul12it 5805  lemul12ait 5806  lediv12it 5852  recp1lt1 5857  ledivp1t 5861  xrmaxltt 5869  xrltmint 5870  maxlet 5874  lemint 5877  maxltt 5878  supxrun 6040  supxrmnf 6042  uzindOLD 6164  flval3t 6190  flwordit 6191  flhalft 6197  ceilet 6201  qaddclt 6215  qbtwnxr 6225  ser1add2 6283  ser1add 6284  uztrn 6368  infmssuzle 6405  elfzle3 6425  fzrevt 6451  fzrevral2t 6460  fsequb 6463  fseqsupcl 6465  seqzm1 6489  expaddt 6535  expmult 6536  expsubt 6537  divexpt 6538  expordit 6539  subsqt 6581  subsq2t 6582  bernneq 6591  bernneq2 6592  expnbndt 6593  reim0t 6719  imcjt 6762  absimlet 6813  seq1bnd 6855  cvg2 6867  cvganz 6869  caubnd 6871  caure 6872  cauim 6873  ser1absdiflem 6874  facdivt 6887  facwordit 6889  faclbnd 6890  faclbnd3 6892  faclbnd6 6899  facavgt 6900  bcval3t 6906  bccmplt 6908  bccl2t 6917  permnnt 6919  fsum1ps 6964  fsumsplit 6966  fsumcom 6974  fsumrev 6975  fsumshft 6977  fsummulc1 6979  fsumdivc 6981  fsumdivcALT 6982  fsumcmp 6986  fsumcmpndx2 6988  fsumabs 6989  ser1ser0 6994  binomlem1 7012  binomlem4 7015  binomlem5 7016  bcxmas 7022  2climnn 7047  2climnn0 7048  climmullem3 7066  climmullem4 7067  climmullem5 7068  climsqueeze 7084  climsqueeze2 7085  clim2serz 7089  climserzle 7091  climcau 7100  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp 7118  ser1cmp2lem 7120  ser1cmp2 7121  cvgcmp3c 7130  iserzgt0 7154  reccnv 7161  georeclim 7183  cvgratlem1ALT 7190  cvgratlem1 7193  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag2 7202  fsum0diag3 7203  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  eftclt 7253  efseq0ex 7261  reefcl 7267  efcj 7286  efaddlem3 7290  efaddlem6 7293  efaddlem14 7301  efaddlem17 7304  efaddlem19 7306  efaddlem23 7310  efaddlem25 7312  reeftclt 7324  eftabs 7325  eftlubclt 7326  reeftlclt 7330  ef01tllem1 7333  ef01tllem2 7334  absefm1le 7360  efcnlem2 7368  efcn 7371  efi4pt 7385  efivalt 7397  addsint 7407  subsint 7408  addcost 7409  subcost 7410  sin01bndlem3 7419  cos01bndlem3 7421  acdc3lem 7436  acdc2lem1 7438  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  tgss2t 7587  subbas2 7595  retopbas 7605  clscld 7633  elcls 7654  ntrcls0 7657  neissex 7688  clslp 7698  dnsconst 7738  blval 7789  blelrn 7800  blss 7805  opnuni 7820  tgbl 7823  blbas 7824  lpbl 7832  methausi 7833  metcnp 7839  metcnp2 7840  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metdnsconst 7853  ioo2bl 7864  tgioolem 7866  lmnn 7887  iscau3 7890  iscau4 7892  lmuni 7902  lmle 7911  metelcls 7916  metcnp4 7920  metcn4 7921  xplmi 7923  lmcau 7946  cmsss 7947  bcthlem2 7950  bcthlem11 7959  bcthlem21 7969  bcthlem24 7972  bcthlem25 7973  grpinvop 8030  grpdivdiv 8037  grpmuldivass 8038  grppnpcan2 8042  abldivdiv4 8061  subgres 8069  nvzs 8217  nvmf 8218  nvmdi 8222  nvpncan2 8228  nvaddsub4 8233  nvdif 8245  nvmtri2 8252  nvabs 8253  nv1 8256  imsdval 8268  imsmetlem 8274  nvcni 8279  nmcnilem 8285  ipval2lem2 8301  ipval2 8304  ipval2lem5 8307  sspn 8342  lnomul 8367  nvcnpi4 8368  nmoge0 8375  nmoubi 8380  nmoub3i 8381  nmblolbii 8403  isblo3i 8405  blocnilem 8408  blocni 8409  cnph 8422  ipasslem2 8435  ipasslem4 8437  ipasslem5 8438  ipdi 8447  ipassr 8450  ipsubdi 8453  siii 8457  ipblnfi 8460  ip2eqi 8461  ubthlem5 8477  ubthlem8 8480  ubthlem10 8482  ubthlem13 8485  minveclem18 8506  minveclem25 8513  minveclem27 8515  psasym 8593  pstr 8594  sinq12gt0t 8644  efifolem7 8662  effoi 8684  hvmul0ort 8833  hvaddsub4t 8884  hcau2 8994  pjpjtht 9196  pjopt 9198  pjpot 9199  shscl 9219  shlej1t 9293  chabs1t 9377  spansncol 9430  normcant 9439  pjspansnt 9440  spanunsn 9442  spanpr 9443  pjoml5t 9496  pjot 9556  pjoi0t 9602  hods 9641  hoaddass 9642  hoadddit 9669  nmopubt 9772  nmopub2tALT 9773  cnvunopt 9781  unoplint 9783  nmfnleubt 9788  nmfnleub2t 9789  unopadj2t 9801  hmopadjt 9802  hmoplint 9805  bralnfnt 9811  kbmult 9818  kbpjt 9819  eigvalclt 9824  eighmortht 9827  lnopeq 9871  hmopst 9883  hmopmt 9884  hmopcot 9886  nmbdoplb 9887  nmcoplb 9896  nmophm 9899  lnopcon 9901  nmbdfnlb 9916  nmcfnlb 9925  lnfncon 9928  nlelch 9932  riesz3 9933  riesz4 9934  cnlnadjlem6 9943  adjlnopt 9957  adjmult 9963  adjaddt 9964  branmfnt 9976  kbass2t 9988  kbass3t 9989  kbass4t 9990  kbass5t 9991  leop2t 9995  leopsqt 10000  leopaddt 10003  leopmulit 10004  leopmult 10005  leopnmidt 10009  hmopidmch 10017  hmopidmpj 10018  pjsspos 10038  pjclem4 10065  pj3s 10073  hstpytht 10094  hstlet 10095  hstoht 10097  stadd 10111  stadd3 10113  strlem1 10115  golem1 10136  mdbr2 10161  dmdbr2 10168  mdslmd1lem1 10189  mdslmd1lem2 10190  superpos 10218  irredlem2 10255  irred 10258  atcvat3 10260  cdj1 10294  cdj3lem2b 10298  elo 10381  fine 10384  hmeogrp 10461  cnfilca 10487  msr3 10505  msr4 10506  mslb1 10509  2wsms 10510  msra3 10511  aidm 10563  aidmold 10564  imonclem 10619  ismonc 10620  cmpmon 10621  icmpmon 10623  idmon 10624

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 776

Copyright terms: Public domain