Theorem syl3anc 1217

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
syl111anc.4	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl3anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1162	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl111anc.4	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  syl112anc  1221  syl121anc  1222  syl211anc  1223  syl113anc  1229  syl131anc  1230  syl311anc  1231  syld3an3  1262  3jaod  1283  mpd3an23  1318  stoic4a  1409  rspc3ev  2810  sbciedf  2948  euotd  4184  ordelord  4311  wetriext  4499  releldm  4782  relelrn  4783  f1imass  5683  ovmpodxf  5904  ovmpodf  5910  fovrnd  5923  offval  5997  caoftrn  6015  offval3  6040  fnmpoovd  6120  tfrlemisucaccv  6230  tfrlemiubacc  6235  tfr1onlemsucaccv  6246  tfr1onlembfn  6249  tfrcllemsucaccv  6259  tfrcllembfn  6262  rdgss  6288  rdgisuc1  6289  rdgisucinc  6290  frecrdg  6313  mapsspm  6584  en2d  6670  en3d  6671  dom3d  6676  ssdomg  6680  f1imaen2g  6695  2dom  6707  cnven  6710  mapen  6748  mapxpen  6750  phpelm  6768  fidifsnen  6772  dif1en  6781  dif1enen  6782  diffisn  6795  isinfinf  6799  unfidisj  6818  unfiin  6822  tpfidisj  6824  xpfi  6826  fisseneq  6828  phpeqd  6829  ssfirab  6830  fnfi  6833  f1dmvrnfibi  6840  iunfidisj  6842  f1finf1o  6843  en1eqsn  6844  fidcenumlemr  6851  updjudhcoinlf  6973  updjudhcoinrg  6974  difinfinf  6994  en2eleq  7068  en2other2  7069  dju1en  7086  djuassen  7090  xpdjuen  7091  addcmpblnq  7199  addassnqg  7214  distrnqg  7219  ltsonq  7230  ltanqg  7232  ltmnqg  7233  ltaddnq  7239  ltexnqq  7240  prarloclemarch  7250  ltrnqg  7252  addcmpblnq0  7275  nnanq0  7290  distrnq0  7291  addassnq0  7294  prarloclemlt  7325  prarloclemcalc  7334  addnqprllem  7359  addnqprulem  7360  addnqprl  7361  addnqpru  7362  addlocprlemgt  7366  appdivnq  7395  prmuloclemcalc  7397  mulnqprl  7400  mulnqpru  7401  mullocprlem  7402  distrlem4prl  7416  distrlem4pru  7417  ltprordil  7421  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemloc  7439  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  ltaprlem  7450  ltaprg  7451  addextpr  7453  recexprlem1ssu  7466  aptipr  7473  ltmprr  7474  caucvgprlemcanl  7476  cauappcvgprlemopl  7478  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprprlemloccalc  7516  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemloc  7535  caucvgprprlemexb  7539  caucvgprprlemaddq  7540  caucvgprprlem1  7541  caucvgprprlem2  7542  suplocexprlemmu  7550  suplocexprlemru  7551  addcmpblnr  7571  mulcmpblnrlemg  7572  mulcmpblnr  7573  ltsrprg  7579  distrsrg  7591  lttrsr  7594  ltsosr  7596  1idsr  7600  ltasrg  7602  recexgt0sr  7605  mulgt0sr  7610  mulextsr1lem  7612  srpospr  7615  prsradd  7618  prsrlt  7619  caucvgsrlemoffval  7628  caucvgsrlemoffgt1  7631  caucvgsrlemoffres  7632  caucvgsr  7634  ltpsrprg  7635  map2psrprg  7637  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  pitoregt0  7681  recidpirqlemcalc  7689  axmulass  7705  axdistr  7706  rereceu  7721  recriota  7722  addassd  7812  mulassd  7813  adddid  7814  adddird  7815  lelttr  7876  letrd  7910  lelttrd  7911  lttrd  7912  mul12d  7938  mul32d  7939  mul31d  7940  add12d  7953  add32d  7954  cnegexlem3  7963  addcand  7970  addcan2d  7971  pncan  7992  pncan3  7994  subcan2  8011  subsub2  8014  subsub4  8019  npncan3  8024  pnpcan  8025  pnncan  8027  addsub4  8029  subaddd  8115  subadd2d  8116  addsubassd  8117  addsubd  8118  subadd23d  8119  addsub12d  8120  npncand  8121  nppcand  8122  nppcan2d  8123  nppcan3d  8124  subsubd  8125  subsub2d  8126  subsub3d  8127  subsub4d  8128  sub32d  8129  nnncand  8130  nnncan1d  8131  nnncan2d  8132  npncan3d  8133  pnpcand  8134  pnpcan2d  8135  pnncand  8136  ppncand  8137  subcand  8138  subcan2d  8139  subcanad  8140  subcan2ad  8142  subdid  8200  subdird  8201  ltadd2  8205  ltadd2d  8207  ltletrd  8209  ltsubadd  8218  lesubadd  8220  ltaddsub  8222  leaddsub  8224  le2add  8230  lt2add  8231  ltleadd  8232  lesub1  8242  lesub2  8243  ltsub1  8244  ltsub2  8245  lt2sub  8246  le2sub  8247  subge0  8261  lesub0  8265  ltadd1d  8324  leadd1d  8325  leadd2d  8326  ltsubaddd  8327  lesubaddd  8328  ltsubadd2d  8329  lesubadd2d  8330  ltaddsubd  8331  ltaddsub2d  8332  leaddsub2d  8333  subled  8334  lesubd  8335  ltsub23d  8336  ltsub13d  8337  lesub1d  8338  lesub2d  8339  ltsub1d  8340  ltsub2d  8341  gt0add  8359  apcotr  8393  apadd1  8394  addext  8396  mulext1  8398  mulext  8400  gtapd  8423  leltapd  8425  subap0d  8430  mulap0  8439  mul0eqap  8455  divvalap  8458  divcanap2  8464  diveqap0  8466  divrecap  8472  divassap  8474  divmulassap  8479  divmulasscomap  8480  divdirap  8481  divcanap3  8482  div11ap  8484  rec11ap  8494  divmuldivap  8496  divdivdivap  8497  divmuleqap  8501  dmdcanap  8506  ddcanap  8510  divadddivap  8511  divsubdivap  8512  redivclap  8515  apmul1  8572  divclapd  8574  divcanap1d  8575  divcanap2d  8576  divrecapd  8577  divrecap2d  8578  divcanap3d  8579  divcanap4d  8580  diveqap0d  8581  diveqap1d  8582  diveqap1ad  8583  diveqap0ad  8584  divap0bd  8586  divnegapd  8587  divneg2apd  8588  div2negapd  8589  redivclapd  8618  div2subap  8620  ltmul12a  8642  lemul12b  8643  lt2mul2div  8661  ltdiv2  8669  ltdiv23  8674  avglt1  8982  avglt2  8983  lt2halvesd  8991  div4p1lem1div2  8997  zltp1le  9132  elz2  9146  zdivmul  9165  uztrn  9366  eluzsub  9379  uz3m2nn  9395  qaddcl  9454  elpq  9467  cnref1o  9469  ltdiv2d  9537  lediv2d  9538  divlt1lt  9541  divle1le  9542  ledivge1le  9543  ltmulgt11d  9549  ltmulgt12d  9550  gt0divd  9551  ge0divd  9552  rpgecld  9553  ltmul1d  9555  ltmul2d  9556  lemul1d  9557  lemul2d  9558  ltdiv1d  9559  lediv1d  9560  ltmuldivd  9561  ltmuldiv2d  9562  lemuldivd  9563  lemuldiv2d  9564  ltdivmuld  9565  ltdivmul2d  9566  ledivmuld  9567  ledivmul2d  9568  ltdiv23d  9574  lediv23d  9575  addlelt  9585  xrltso  9612  xrlelttr  9619  xrlttrd  9622  xrlelttrd  9623  xrltletrd  9624  xrletrd  9625  xrre3  9635  xleadd1  9688  xltadd1  9689  xle2add  9692  xlt2add  9693  xlesubadd  9696  xadd4d  9698  ixxss1  9717  ixxss2  9718  ixxss12  9719  iooshf  9765  icoshftf1o  9804  ioodisj  9806  zltaddlt1le  9820  fznlem  9852  fzdifsuc  9892  fzrev  9895  fzrevral2  9917  elfz0fzfz0  9934  elfzmlbp  9940  fzctr  9941  elfzole1  9963  elfzolt2  9964  fzoss2  9980  fzospliti  9984  fzo1fzo0n0  9991  elfzo0z  9992  fzofzim  9996  fzoaddel  10000  eluzgtdifelfzo  10005  elfzodifsumelfzo  10009  ssfzo12bi  10033  elfzonelfzo  10038  fvinim0ffz  10049  rebtwn2zlemstep  10061  rebtwn2z  10063  qbtwnxr  10066  flqge  10086  2tnp1ge0ge0  10105  intfracq  10124  flqdiv  10125  modqval  10128  modqcld  10132  modqmulnn  10146  zmodcl  10148  zmodfz  10150  modqid  10153  zmodid2  10156  modqabs  10161  modqcyc  10163  modqadd1  10165  modqaddabs  10166  modqaddmod  10167  mulp1mod1  10169  modqmuladd  10170  modqmuladdim  10171  modqmuladdnn0  10172  m1modnnsub1  10174  modqltm1p1mod  10180  modqmul1  10181  modqsubmod  10186  modqsubmodmod  10187  q2txmodxeq0  10188  modaddmodup  10191  modqmulmod  10193  modqaddmulmod  10195  modqdi  10196  modqsubdir  10197  addmodlteq  10202  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  frecfzen2  10231  seq3val  10262  seqvalcd  10263  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  monoord  10280  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemmo  10296  iseqf1olemqk  10298  seq3f1olemqsumkj  10302  seq3f1olemstep  10305  expnnval  10327  expnegap0  10332  rpexpcl  10343  expnegzap  10358  expgt1  10362  mulexpzap  10364  exprecap  10365  expaddzaplem  10367  expaddzap  10368  expmul  10369  expmulzap  10370  expdivap  10375  ltexp2a  10376  leexp2a  10377  leexp2r  10378  leexp1a  10379  bernneq2  10444  bernneq3  10445  expnbnd  10446  expnlbnd  10447  expnlbnd2  10448  expaddd  10457  expmuld  10458  expclzapd  10460  expap0d  10461  expnegapd  10462  exprecapd  10463  expp1zapd  10464  expm1apd  10465  sqdivapd  10468  mulexpd  10470  expge0d  10473  expge1d  10474  sqoddm1div8  10475  reexpclzapd  10480  leexp2ad  10484  facwordi  10518  faclbnd3  10521  facavg  10524  bcval  10527  bccmpl  10532  bc0k  10534  bcval5  10541  bcpasc  10544  hashfiv01gt1  10560  hashunlem  10582  hashunsng  10585  fiprsshashgt1  10595  hashdifsn  10597  hashdifpr  10598  hashfz  10599  hashxp  10604  hashfacen  10611  zfz1isolemiso  10614  zfz1isolem1  10615  zfz1iso  10616  shftfvalg  10622  seq3shft  10642  mulreap  10668  cjreb  10670  cjap  10710  cnrecnv  10714  cjdivapd  10772  redivapd  10778  imdivapd  10779  resqrexlemdecn  10816  absexpzap  10884  abslt  10892  absle  10893  elicc4abs  10898  abs3lem  10915  fzomaxdiflem  10916  cau3lem  10918  amgm2  10922  abssubge0d  10980  abssuble0d  10981  absdifltd  10982  absdifled  10983  absdivapd  10999  abs3difd  11004  qdenre  11006  maxabslemlub  11011  rexanre  11024  rexico  11025  fimaxre2  11030  lemininf  11037  ltmininf  11038  rpmincl  11041  mul0inf  11044  xrmaxiflemlub  11049  xrmaxltsup  11059  xrmaxaddlem  11061  xrmaxadd  11062  xrltmininf  11071  xrlemininf  11072  xrminltinf  11073  xrminadd  11076  xrbdtri  11077  climshftlemg  11103  climshft2  11107  addcn2  11111  mulcn2  11113  reccn2ap  11114  cn1lem  11115  climadd  11127  climmul  11128  climsub  11129  climsqz  11136  climsqz2  11137  climrecvg1n  11149  climcvg1nlem  11150  fisumss  11193  fsumsplitsn  11211  sumpr  11214  fsumsplitsnun  11220  fsum2dlemstep  11235  fisumcom2  11239  fisum0diag2  11248  fsumconst  11255  modfsummodlemstep  11258  fsumlessfi  11261  fsumabs  11266  fsumiun  11278  hashiun  11279  hash2iun  11280  hash2iun1dif1  11281  binomlem  11284  bcxmas  11290  isumshft  11291  isumlessdc  11297  expcnvap0  11303  expcnvre  11304  geosergap  11307  cvgratnnlembern  11324  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  mertenslemi1  11336  efaddlem  11417  eftlub  11433  efltim  11441  eirraplem  11519  dvdsval3  11533  nndivdvds  11535  summodnegmod  11560  modmulconst  11561  dvds2subd  11565  dvdsmultr1d  11568  dvdsmultr2  11569  dvdsabseq  11581  dvdsfac  11594  dvdsmod  11596  oddge22np1  11614  ltoddhalfle  11626  halfleoddlt  11627  nn0ehalf  11636  nno  11639  nn0oddm1d2  11642  divalglemnn  11651  divalg  11657  divalgmod  11660  fldivndvdslt  11668  flodddiv4lt  11669  flodddiv4t2lthalf  11670  infssuzex  11678  dvdsbnd  11681  gcdneg  11706  gcdaddm  11708  modgcd  11715  gcdmultipled  11717  dvdsgcdidd  11718  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlembi  11729  dvdsgcdb  11737  gcdass  11739  mulgcd  11740  dvdsmulgcd  11749  rpmulgcd  11750  sqgcd  11753  nn0seqcvgd  11758  eucalglt  11774  gcddvdslcm  11790  lcmgcdlem  11794  lcmdvdsb  11801  lcmass  11802  ncoprmgcdne1b  11806  coprmdvds2  11810  mulgcddvds  11811  rpmulgcd2  11812  qredeu  11814  rpdvds  11816  divgcdcoprm0  11818  cncongr1  11820  cncongr2  11821  isprm2lem  11833  prmind2  11837  nprm  11840  dvdsnprmd  11842  exprmfct  11854  prmdvdsfz  11855  divgcdodd  11857  isprm6  11861  prmdvdsexp  11862  prmexpb  11865  prmfac1  11866  rpexp  11867  rpexp12i  11869  pw2dvdseulemle  11881  sqpweven  11889  2sqpwodd  11890  divnumden  11910  numdensq  11916  nonsq  11921  hashdvds  11933  phiprmpw  11934  crth  11936  phimullem  11937  hashgcdlem  11939  ennnfonelemp1  11955  ennnfonelemex  11963  ennnfonelemrn  11968  ctinfom  11977  ctiunct  11989  strsetsid  12031  fvsetsid  12032  setsabsd  12037  setscom  12038  ressid2  12057  ressval2  12058  srngstrd  12120  lmodstrd  12131  ipsstrd  12139  topgrpstrd  12149  difopn  12316  uncld  12321  ntrin  12332  clsss2  12337  ntrcls0  12339  topssnei  12370  neissex  12373  restbasg  12376  tgrest  12377  resttopon  12379  restabs  12383  restopnb  12389  cnpfval  12403  cnprcl2k  12414  tgcnp  12417  iscnp4  12426  cnpnei  12427  cnptopco  12430  cncnpi  12436  cncnp  12438  cnconst2  12441  cnrest  12443  cnrest2  12444  cnrest2r  12445  cnptopresti  12446  cnptoprest  12447  cnptoprest2  12448  lmss  12454  lmtopcnp  12458  txvalex  12462  txval  12463  txbasval  12475  txcnp  12479  txcnmpt  12481  txcn  12483  txdis1cn  12486  lmcn2  12488  cnmptc  12490  cnmpt11  12491  cnmpt1t  12493  cnmpt12  12495  cnmpt21  12499  cnmpt2t  12501  cnmpt22  12502  cnmpt22f  12503  cnmptcom  12506  hmeores  12523  txhmeo  12527  psmettri  12538  xmettri  12580  metrtri  12585  xmetres2  12587  blfvalps  12593  bldisj  12609  blgt0  12610  xblss2ps  12612  xblss2  12613  blhalf  12616  blininf  12632  blssps  12635  blss  12636  blssexps  12637  blssex  12638  blin2  12640  xmeter  12644  blnei  12700  blsscls2  12701  metss2lem  12705  bdmetval  12708  bdxmet  12709  bdbl  12711  xmetxp  12715  xmetxpbl  12716  xmettxlem  12717  xmettx  12718  metcnp3  12719  metcnp  12720  metcnp2  12721  metcnpi  12723  metcnpi2  12724  metcnpi3  12725  txmetcnp  12726  metcnpd  12728  tgqioo  12755  addcncntoplem  12759  fsumcncntop  12764  mulc1cncf  12784  cncfco  12786  mulcncflem  12798  mulcncf  12799  suplociccreex  12810  suplociccex  12811  dedekindicc  12819  ivthinclemlm  12820  ivthinclemum  12821  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthinclemloc  12827  ivthdec  12830  limccl  12836  ellimc3apf  12837  limcimolemlt  12841  cnplimclemle  12845  cnplimclemr  12846  limccnpcntop  12852  limccnp2lem  12853  limccnp2cntop  12854  reldvg  12856  eldvap  12859  dvbssntrcntop  12861  dvcnp2cntop  12871  dvmulxxbr  12874  dvrecap  12885  dveflem  12895  reeff1o  12902  efltlemlt  12903  sin0pilem2  12911  ptolemy  12953  sinq12gt0  12959  cxprec  13039  rpcxproot  13042  cxpmuld  13064  rpabscxpbnd  13067  rplogbval  13070  rplogbchbase  13075  relogbval  13076  relogbzcl  13077  rplogbreexp  13078  rprelogbmul  13080  rprelogbdiv  13082  nnlogbexp  13084  relogbcxpbap  13090  logbgt0b  13091  logbgcd1irr  13092  logbgcd1irraplemexp  13093  logbgcd1irraplemap  13094  logbprmirr  13097  apdifflemr  13415  apdiff  13416