Theorem syl3anc 1216

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 1161	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl111anc.4	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 962

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 964

This theorem is referenced by:  syl112anc  1220  syl121anc  1221  syl211anc  1222  syl113anc  1228  syl131anc  1229  syl311anc  1230  syld3an3  1261  3jaod  1282  mpd3an23  1317  stoic4a  1408  rspc3ev  2806  sbciedf  2944  euotd  4176  ordelord  4303  wetriext  4491  releldm  4774  relelrn  4775  f1imass  5675  ovmpodxf  5896  ovmpodf  5902  fovrnd  5915  offval  5989  caoftrn  6007  offval3  6032  fnmpoovd  6112  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfr1onlemsucaccv  6238  tfr1onlembfn  6241  tfrcllemsucaccv  6251  tfrcllembfn  6254  rdgss  6280  rdgisuc1  6281  rdgisucinc  6282  frecrdg  6305  mapsspm  6576  en2d  6662  en3d  6663  dom3d  6668  ssdomg  6672  f1imaen2g  6687  2dom  6699  cnven  6702  mapen  6740  mapxpen  6742  phpelm  6760  fidifsnen  6764  dif1en  6773  dif1enen  6774  diffisn  6787  isinfinf  6791  unfidisj  6810  unfiin  6814  tpfidisj  6816  xpfi  6818  fisseneq  6820  phpeqd  6821  ssfirab  6822  fnfi  6825  f1dmvrnfibi  6832  iunfidisj  6834  f1finf1o  6835  en1eqsn  6836  fidcenumlemr  6843  updjudhcoinlf  6965  updjudhcoinrg  6966  difinfinf  6986  en2eleq  7051  en2other2  7052  dju1en  7069  djuassen  7073  xpdjuen  7074  addcmpblnq  7175  addassnqg  7190  distrnqg  7195  ltsonq  7206  ltanqg  7208  ltmnqg  7209  ltaddnq  7215  ltexnqq  7216  prarloclemarch  7226  ltrnqg  7228  addcmpblnq0  7251  nnanq0  7266  distrnq0  7267  addassnq0  7270  prarloclemlt  7301  prarloclemcalc  7310  addnqprllem  7335  addnqprulem  7336  addnqprl  7337  addnqpru  7338  addlocprlemgt  7342  appdivnq  7371  prmuloclemcalc  7373  mulnqprl  7376  mulnqpru  7377  mullocprlem  7378  distrlem4prl  7392  distrlem4pru  7393  ltprordil  7397  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemloc  7415  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  ltaprlem  7426  ltaprg  7427  addextpr  7429  recexprlem1ssu  7442  aptipr  7449  ltmprr  7450  caucvgprlemcanl  7452  cauappcvgprlemopl  7454  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprprlemloccalc  7492  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemloc  7511  caucvgprprlemexb  7515  caucvgprprlemaddq  7516  caucvgprprlem1  7517  caucvgprprlem2  7518  suplocexprlemmu  7526  suplocexprlemru  7527  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  ltsrprg  7555  distrsrg  7567  lttrsr  7570  ltsosr  7572  1idsr  7576  ltasrg  7578  recexgt0sr  7581  mulgt0sr  7586  mulextsr1lem  7588  srpospr  7591  prsradd  7594  prsrlt  7595  caucvgsrlemoffval  7604  caucvgsrlemoffgt1  7607  caucvgsrlemoffres  7608  caucvgsr  7610  ltpsrprg  7611  map2psrprg  7613  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  pitoregt0  7657  recidpirqlemcalc  7665  axmulass  7681  axdistr  7682  rereceu  7697  recriota  7698  addassd  7788  mulassd  7789  adddid  7790  adddird  7791  lelttr  7852  letrd  7886  lelttrd  7887  lttrd  7888  mul12d  7914  mul32d  7915  mul31d  7916  add12d  7929  add32d  7930  cnegexlem3  7939  addcand  7946  addcan2d  7947  pncan  7968  pncan3  7970  subcan2  7987  subsub2  7990  subsub4  7995  npncan3  8000  pnpcan  8001  pnncan  8003  addsub4  8005  subaddd  8091  subadd2d  8092  addsubassd  8093  addsubd  8094  subadd23d  8095  addsub12d  8096  npncand  8097  nppcand  8098  nppcan2d  8099  nppcan3d  8100  subsubd  8101  subsub2d  8102  subsub3d  8103  subsub4d  8104  sub32d  8105  nnncand  8106  nnncan1d  8107  nnncan2d  8108  npncan3d  8109  pnpcand  8110  pnpcan2d  8111  pnncand  8112  ppncand  8113  subcand  8114  subcan2d  8115  subcanad  8116  subcan2ad  8118  subdid  8176  subdird  8177  ltadd2  8181  ltadd2d  8183  ltletrd  8185  ltsubadd  8194  lesubadd  8196  ltaddsub  8198  leaddsub  8200  le2add  8206  lt2add  8207  ltleadd  8208  lesub1  8218  lesub2  8219  ltsub1  8220  ltsub2  8221  lt2sub  8222  le2sub  8223  subge0  8237  lesub0  8241  ltadd1d  8300  leadd1d  8301  leadd2d  8302  ltsubaddd  8303  lesubaddd  8304  ltsubadd2d  8305  lesubadd2d  8306  ltaddsubd  8307  ltaddsub2d  8308  leaddsub2d  8309  subled  8310  lesubd  8311  ltsub23d  8312  ltsub13d  8313  lesub1d  8314  lesub2d  8315  ltsub1d  8316  ltsub2d  8317  gt0add  8335  apcotr  8369  apadd1  8370  addext  8372  mulext1  8374  mulext  8376  gtapd  8399  leltapd  8401  subap0d  8406  mulap0  8415  mul0eqap  8431  divvalap  8434  divcanap2  8440  diveqap0  8442  divrecap  8448  divassap  8450  divmulassap  8455  divmulasscomap  8456  divdirap  8457  divcanap3  8458  div11ap  8460  rec11ap  8470  divmuldivap  8472  divdivdivap  8473  divmuleqap  8477  dmdcanap  8482  ddcanap  8486  divadddivap  8487  divsubdivap  8488  redivclap  8491  apmul1  8548  divclapd  8550  divcanap1d  8551  divcanap2d  8552  divrecapd  8553  divrecap2d  8554  divcanap3d  8555  divcanap4d  8556  diveqap0d  8557  diveqap1d  8558  diveqap1ad  8559  diveqap0ad  8560  divap0bd  8562  divnegapd  8563  divneg2apd  8564  div2negapd  8565  redivclapd  8594  div2subap  8596  ltmul12a  8618  lemul12b  8619  lt2mul2div  8637  ltdiv2  8645  ltdiv23  8650  avglt1  8958  avglt2  8959  lt2halvesd  8967  div4p1lem1div2  8973  zltp1le  9108  elz2  9122  zdivmul  9141  uztrn  9342  eluzsub  9355  uz3m2nn  9368  qaddcl  9427  cnref1o  9440  ltdiv2d  9507  lediv2d  9508  divlt1lt  9511  divle1le  9512  ledivge1le  9513  ltmulgt11d  9519  ltmulgt12d  9520  gt0divd  9521  ge0divd  9522  rpgecld  9523  ltmul1d  9525  ltmul2d  9526  lemul1d  9527  lemul2d  9528  ltdiv1d  9529  lediv1d  9530  ltmuldivd  9531  ltmuldiv2d  9532  lemuldivd  9533  lemuldiv2d  9534  ltdivmuld  9535  ltdivmul2d  9536  ledivmuld  9537  ledivmul2d  9538  ltdiv23d  9544  lediv23d  9545  addlelt  9555  xrltso  9582  xrlelttr  9589  xrlttrd  9592  xrlelttrd  9593  xrltletrd  9594  xrletrd  9595  xrre3  9605  xleadd1  9658  xltadd1  9659  xle2add  9662  xlt2add  9663  xlesubadd  9666  xadd4d  9668  ixxss1  9687  ixxss2  9688  ixxss12  9689  iooshf  9735  icoshftf1o  9774  ioodisj  9776  zltaddlt1le  9789  fznlem  9821  fzdifsuc  9861  fzrev  9864  fzrevral2  9886  elfz0fzfz0  9903  elfzmlbp  9909  fzctr  9910  elfzole1  9932  elfzolt2  9933  fzoss2  9949  fzospliti  9953  fzo1fzo0n0  9960  elfzo0z  9961  fzofzim  9965  fzoaddel  9969  eluzgtdifelfzo  9974  elfzodifsumelfzo  9978  ssfzo12bi  10002  elfzonelfzo  10007  fvinim0ffz  10018  rebtwn2zlemstep  10030  rebtwn2z  10032  qbtwnxr  10035  flqge  10055  2tnp1ge0ge0  10074  intfracq  10093  flqdiv  10094  modqval  10097  modqcld  10101  modqmulnn  10115  zmodcl  10117  zmodfz  10119  modqid  10122  zmodid2  10125  modqabs  10130  modqcyc  10132  modqadd1  10134  modqaddabs  10135  modqaddmod  10136  mulp1mod1  10138  modqmuladd  10139  modqmuladdim  10140  modqmuladdnn0  10141  m1modnnsub1  10143  modqltm1p1mod  10149  modqmul1  10150  modqsubmod  10155  modqsubmodmod  10156  q2txmodxeq0  10157  modaddmodup  10160  modqmulmod  10162  modqaddmulmod  10164  modqdi  10165  modqsubdir  10166  addmodlteq  10171  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgsuctlem  10196  frecfzen2  10200  seq3val  10231  seqvalcd  10232  seqf  10234  seq3p1  10235  seqovcd  10236  seqp1cd  10239  monoord  10249  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemmo  10265  iseqf1olemqk  10267  seq3f1olemqsumkj  10271  seq3f1olemstep  10274  expnnval  10296  expnegap0  10301  rpexpcl  10312  expnegzap  10327  expgt1  10331  mulexpzap  10333  exprecap  10334  expaddzaplem  10336  expaddzap  10337  expmul  10338  expmulzap  10339  expdivap  10344  ltexp2a  10345  leexp2a  10346  leexp2r  10347  leexp1a  10348  bernneq2  10413  bernneq3  10414  expnbnd  10415  expnlbnd  10416  expnlbnd2  10417  expaddd  10426  expmuld  10427  expclzapd  10429  expap0d  10430  expnegapd  10431  exprecapd  10432  expp1zapd  10433  expm1apd  10434  sqdivapd  10437  mulexpd  10439  expge0d  10442  expge1d  10443  sqoddm1div8  10444  reexpclzapd  10449  leexp2ad  10453  facwordi  10486  faclbnd3  10489  facavg  10492  bcval  10495  bccmpl  10500  bc0k  10502  bcval5  10509  bcpasc  10512  hashfiv01gt1  10528  hashunlem  10550  hashunsng  10553  fiprsshashgt1  10563  hashdifsn  10565  hashdifpr  10566  hashfz  10567  hashxp  10572  hashfacen  10579  zfz1isolemiso  10582  zfz1isolem1  10583  zfz1iso  10584  shftfvalg  10590  seq3shft  10610  mulreap  10636  cjreb  10638  cjap  10678  cnrecnv  10682  cjdivapd  10740  redivapd  10746  imdivapd  10747  resqrexlemdecn  10784  absexpzap  10852  abslt  10860  absle  10861  elicc4abs  10866  abs3lem  10883  fzomaxdiflem  10884  cau3lem  10886  amgm2  10890  abssubge0d  10948  abssuble0d  10949  absdifltd  10950  absdifled  10951  absdivapd  10967  abs3difd  10972  qdenre  10974  maxabslemlub  10979  rexanre  10992  rexico  10993  fimaxre2  10998  lemininf  11005  ltmininf  11006  rpmincl  11009  mul0inf  11012  xrmaxiflemlub  11017  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  xrltmininf  11039  xrlemininf  11040  xrminltinf  11041  xrminadd  11044  xrbdtri  11045  climshftlemg  11071  climshft2  11075  addcn2  11079  mulcn2  11081  reccn2ap  11082  cn1lem  11083  climadd  11095  climmul  11096  climsub  11097  climsqz  11104  climsqz2  11105  climrecvg1n  11117  climcvg1nlem  11118  fisumss  11161  fsumsplitsn  11179  sumpr  11182  fsumsplitsnun  11188  fsum2dlemstep  11203  fisumcom2  11207  fisum0diag2  11216  fsumconst  11223  modfsummodlemstep  11226  fsumlessfi  11229  fsumabs  11234  fsumiun  11246  hashiun  11247  hash2iun  11248  hash2iun1dif1  11249  binomlem  11252  bcxmas  11258  isumshft  11259  isumlessdc  11265  expcnvap0  11271  expcnvre  11272  geosergap  11275  cvgratnnlembern  11292  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  mertenslemi1  11304  efaddlem  11380  eftlub  11396  efltim  11404  eirraplem  11483  dvdsval3  11497  nndivdvds  11499  summodnegmod  11524  modmulconst  11525  dvds2subd  11529  dvdsmultr1d  11532  dvdsmultr2  11533  dvdsabseq  11545  dvdsfac  11558  dvdsmod  11560  oddge22np1  11578  ltoddhalfle  11590  halfleoddlt  11591  nn0ehalf  11600  nno  11603  nn0oddm1d2  11606  divalglemnn  11615  divalg  11621  divalgmod  11624  fldivndvdslt  11632  flodddiv4lt  11633  flodddiv4t2lthalf  11634  infssuzex  11642  dvdsbnd  11645  gcdneg  11670  gcdaddm  11672  modgcd  11679  gcdmultipled  11681  dvdsgcdidd  11682  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlembi  11693  dvdsgcdb  11701  gcdass  11703  mulgcd  11704  dvdsmulgcd  11713  rpmulgcd  11714  sqgcd  11717  nn0seqcvgd  11722  eucalglt  11738  gcddvdslcm  11754  lcmgcdlem  11758  lcmdvdsb  11765  lcmass  11766  ncoprmgcdne1b  11770  coprmdvds2  11774  mulgcddvds  11775  rpmulgcd2  11776  qredeu  11778  rpdvds  11780  divgcdcoprm0  11782  cncongr1  11784  cncongr2  11785  isprm2lem  11797  prmind2  11801  nprm  11804  dvdsnprmd  11806  exprmfct  11818  prmdvdsfz  11819  divgcdodd  11821  isprm6  11825  prmdvdsexp  11826  prmexpb  11829  prmfac1  11830  rpexp  11831  rpexp12i  11833  pw2dvdseulemle  11845  sqpweven  11853  2sqpwodd  11854  divnumden  11874  numdensq  11880  nonsq  11885  hashdvds  11897  phiprmpw  11898  crth  11900  phimullem  11901  hashgcdlem  11903  ennnfonelemp1  11919  ennnfonelemex  11927  ennnfonelemrn  11932  ctinfom  11941  ctiunct  11953  strsetsid  11992  fvsetsid  11993  setsabsd  11998  setscom  11999  ressid2  12018  ressval2  12019  srngstrd  12081  lmodstrd  12092  ipsstrd  12100  topgrpstrd  12110  difopn  12277  uncld  12282  ntrin  12293  clsss2  12298  ntrcls0  12300  topssnei  12331  neissex  12334  restbasg  12337  tgrest  12338  resttopon  12340  restabs  12344  restopnb  12350  cnpfval  12364  cnprcl2k  12375  tgcnp  12378  iscnp4  12387  cnpnei  12388  cnptopco  12391  cncnpi  12397  cncnp  12399  cnconst2  12402  cnrest  12404  cnrest2  12405  cnrest2r  12406  cnptopresti  12407  cnptoprest  12408  cnptoprest2  12409  lmss  12415  lmtopcnp  12419  txvalex  12423  txval  12424  txbasval  12436  txcnp  12440  txcnmpt  12442  txcn  12444  txdis1cn  12447  lmcn2  12449  cnmptc  12451  cnmpt11  12452  cnmpt1t  12454  cnmpt12  12456  cnmpt21  12460  cnmpt2t  12462  cnmpt22  12463  cnmpt22f  12464  cnmptcom  12467  hmeores  12484  txhmeo  12488  psmettri  12499  xmettri  12541  metrtri  12546  xmetres2  12548  blfvalps  12554  bldisj  12570  blgt0  12571  xblss2ps  12573  xblss2  12574  blhalf  12577  blininf  12593  blssps  12596  blss  12597  blssexps  12598  blssex  12599  blin2  12601  xmeter  12605  blnei  12661  blsscls2  12662  metss2lem  12666  bdmetval  12669  bdxmet  12670  bdbl  12672  xmetxp  12676  xmetxpbl  12677  xmettxlem  12678  xmettx  12679  metcnp3  12680  metcnp  12681  metcnp2  12682  metcnpi  12684  metcnpi2  12685  metcnpi3  12686  txmetcnp  12687  metcnpd  12689  tgqioo  12716  addcncntoplem  12720  fsumcncntop  12725  mulc1cncf  12745  cncfco  12747  mulcncflem  12759  mulcncf  12760  suplociccreex  12771  suplociccex  12772  dedekindicc  12780  ivthinclemlm  12781  ivthinclemum  12782  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthinclemloc  12788  ivthdec  12791  limccl  12797  ellimc3apf  12798  limcimolemlt  12802  cnplimclemle  12806  cnplimclemr  12807  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  reldvg  12817  eldvap  12820  dvbssntrcntop  12822  dvcnp2cntop  12832  dvmulxxbr  12835  dvrecap  12846  dveflem  12855  sin0pilem2  12863  ptolemy  12905  sinq12gt0  12911