Theorem syl31anc 1366

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

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl31anc.5	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl31anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl31anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1121	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 584	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082

This theorem is referenced by:  syl32anc  1371  stoic4b  1760  elovmpt3rab1  7263  smo11  7853  omeulem2  8059  oeeui  8078  oaabs2  8122  omabs  8124  omxpenlem  8465  map2xp  8534  mapdom2  8535  fsuppsssupp  8695  cantnflt  8981  cnfcom  9009  mapdjuen  9452  pwsdompw  9472  ackbij1lem5  9492  cofsmo  9537  fin1a2lem4  9671  ltmul12a  11344  lt2msq1  11372  ledivp1  11390  lemul1ad  11427  lemul2ad  11428  suprubd  11451  supaddc  11456  supadd  11457  supmul1  11458  supmul  11461  rpnnen1lem3  12228  rpnnen1lem5  12230  lediv2ad  12303  xaddge0  12501  xadddi  12538  xadddi2  12540  supicc  12736  supicclub  12738  difelfznle  12871  flval3  13035  expcan  13383  ltexp2  13384  ltexp2r  13387  expubnd  13391  ltexp2rd  13459  ltexp2d  13464  leexp2d  13465  expcand  13466  hashmap  13644  swrds1  13864  ccatswrd  13866  swrdccat2  13867  pfxfv  13880  swrdccatin2  13927  pfxccatin12lem3  13930  cshwidxmod  14001  wrdl3s3  14160  o1fsum  15001  mertenslem1  15073  eftlub  15295  rpnnen2lem4  15403  ruclem12  15427  dvdsadd  15485  3dvds  15513  divalgmod  15590  bitsmod  15618  bitsinv1lem  15623  bezoutlem4  15719  gcdzeq  15731  rplpwr  15736  sqgcd  15738  rpmulgcd2  15829  rpdvds  15833  coprmproddvdslem  15835  isprm5  15880  divgcdodd  15883  divnumden  15917  crth  15944  phimullem  15945  modprm0  15971  modprmn0modprm0  15973  coprimeprodsq2  15975  pythagtriplem19  15999  pockthlem  16070  prmunb  16079  prmreclem3  16083  prmreclem6  16086  ramub  16178  ramz  16190  pmtrprfv  18312  pmtrprfv3  18313  mndodcong  18401  odngen  18432  pgpfi  18460  sylow2blem3  18477  lsmless1  18514  lsmless2  18515  lsmless12  18516  lsmmod2  18529  pj1id  18552  odadd2  18692  gexexlem  18695  ablfacrplem  18904  ablfacrp  18905  ablfac1b  18909  ablfac1eu  18912  pgpfac1lem2  18914  kerf1ghm  19187  kerf1hrmOLD  19188  lsmssspx  19550  lspsncv0  19608  coe1subfv  20117  coe1fzgsumdlem  20152  znunit  20392  uvcvvcl2  20614  uvcvv1  20615  uvcvv0  20616  scmate  20803  mdetunilem2  20906  pmatcoe1fsupp  20993  mat2pmatlin  21027  decpmatmullem  21063  pmatcollpw1lem1  21066  pmatcollpw1lem2  21067  pm2mpghm  21108  chpscmat  21134  chp0mat  21138  chpidmat  21139  cpmadugsumlemB  21166  cpmadugsumlemC  21167  cpmadugsumlemF  21168  clsndisj  21367  neiptopnei  21424  rnelfm  22245  fmfnfmlem2  22247  fmfnfm  22250  flimss1  22265  isfcf  22326  cnextfun  22356  cnextfvval  22357  cnextf  22358  cnextcn  22359  cnextfres1  22360  ustuqtop1  22533  utopsnneiplem  22539  xblss2ps  22694  xblss2  22695  stdbdxmet  22808  metcnpi3  22839  metustexhalf  22849  nmoi  23020  nmoi2  23022  nmoco  23029  blcvx  23089  icccmplem2  23114  icccmplem3  23115  reconnlem2  23118  xrge0gsumle  23124  metds0  23141  metdstri  23142  metdseq0  23145  lebnumlem3  23250  nmoleub2lem  23401  bcthlem5  23614  csschl  23662  minveclem2  23712  minveclem3b  23714  minveclem4  23718  minveclem6  23720  icombl  23848  cncombf  23942  mbflimsup  23950  itg2monolem1  24034  itg2cnlem1  24045  itg2cnlem2  24046  bddmulibl  24122  ellimc2  24158  cpnord  24215  cpnres  24217  dvmulbr  24219  dvcobr  24226  dvlipcn  24274  dvlip2  24275  dvivthlem1  24288  lhop1lem  24293  lhop1  24294  dvfsumlem2  24307  itgsubstlem  24328  deg1add  24380  deg1sublt  24387  ply1remlem  24439  plyeq0lem  24483  taylthlem2  24645  ulmdvlem3  24673  abelthlem7  24709  pilem2  24723  pilem3  24724  pige3ALT  24788  logccv  24927  cxpaddlelem  25013  cvxcl  25244  fsumharmonic  25271  ftalem5  25336  dvdsmulf1o  25453  bposlem1  25542  lgsqr  25609  lgsquad2lem2  25643  2lgsoddprmlem1  25666  2sqlem8a  25683  2sqlem8  25684  dchrmusum2  25752  dchrvmasumiflem1  25759  dchrisum0flblem1  25766  dchrisum0lem1b  25773  pntlem3  25867  tgdim01  25975  axsegcon  26396  ax5seglem1  26397  ax5seglem2  26398  axlowdimlem6  26416  axeuclidlem  26431  axcontlem7  26439  axcontlem9  26441  axcontlem10  26442  nbupgr  26809  nbumgrvtx  26811  cusgrsize2inds  26918  upgriswlk  27105  2pthnloop  27199  clwwlknonex2lem2  27574  numclwwlk2lem1  27847  frgrreg  27865  nmoub3i  28241  ubthlem3  28340  minvecolem2  28343  minvecolem4  28348  minvecolem5  28349  minvecolem6  28350  htthlem  28385  pjpjpre  28887  chscllem1  29105  chscllem2  29106  chscllem3  29107  cnlnadjlem2  29536  leopnmid  29606  br8d  30051  dvdszzq  30215  ogrpaddlt  30378  symgcom2  30387  cyc3genpmlem  30431  archirngz  30456  ornglmullt  30534  orngrmullt  30535  elrhmunit  30547  lssdimle  30610  dimkerim  30627  fedgmullem2  30630  fedgmul  30631  qqhval2lem  30839  qqhnm  30848  qqhucn  30850  esumcst  30939  esumpcvgval  30954  measunl  31092  dya2iocbrsiga  31150  dya2icobrsiga  31151  omssubadd  31175  inelcarsg  31186  carsgclctunlem2  31194  sibfof  31215  sitgaddlemb  31223  oddpwdc  31229  eulerpartlemgc  31237  bayesth  31314  ftc2re  31486  breprexplemc  31520  tgoldbachgt  31551  erdszelem8  32054  2goelgoanfmla1  32280  br8  32601  noetalem3  32829  noetalem5  32831  matunitlindflem2  34439  totbndbnd  34618  prdsbnd  34622  rrncmslem  34661  rrntotbnd  34665  isdrngo2  34787  lsatcmp  35689  lcvexchlem2  35721  lcvexchlem3  35722  ncvr1  35958  cvrletrN  35959  cvrnbtwn3  35962  cvrnrefN  35968  cvrcmp  35969  0ltat  35977  atnle0  35995  atlen0  35996  cvlcvr1  36025  cvrval3  36099  atle  36122  athgt  36142  1cvratex  36159  ps-2  36164  ps-2b  36168  llnnleat  36199  2atneat  36201  llnle  36204  atcvrlln  36206  llncmp  36208  2llnmat  36210  2at0mat0  36211  2atm  36213  ps-2c  36214  lplnle  36226  lplnnle2at  36227  llncvrlpln2  36243  llncvrlpln  36244  2lplnmN  36245  2llnmj  36246  2atmat  36247  lplncmp  36248  lplnexllnN  36250  2llnm2N  36254  2llnm4  36256  lvolnle3at  36268  4atlem3a  36283  4atlem3b  36284  4atlem10  36292  4atlem11  36295  4atlem12  36298  lplncvrlvol2  36301  lplncvrlvol  36302  lvolcmp  36303  2lplnm2N  36307  2lplnmj  36308  dalempjsen  36339  dalemcea  36346  dalem2  36347  dalemdea  36348  dalem9  36358  dalem16  36365  dalemcjden  36378  dalem21  36380  dalem23  36382  dalem39  36397  dalem54  36412  dalem60  36418  cdlemb  36480  elpadd2at  36492  paddasslem4  36509  paddasslem7  36512  paddasslem15  36520  paddasslem16  36521  pmodlem1  36532  pmodlem2  36533  llnexchb2  36555  pclfinclN  36636  osumcllem9N  36650  pmapojoinN  36654  pexmidN  36655  pl42lem1N  36665  lhp0lt  36689  lhpexle1  36694  lhpexle2lem  36695  lhpexle3lem  36697  lhprelat3N  36726  ltrnid  36821  trlval3  36873  arglem1N  36876  cdlemc5  36881  cdleme3b  36915  cdleme3c  36916  cdleme3h  36921  cdleme7e  36933  cdleme7ga  36934  cdleme20l1  37006  cdleme20l2  37007  cdleme20l  37008  cdleme22b  37027  cdlemefrs29clN  37085  cdlemefrs32fva  37086  cdlemeg46fvcl  37192  cdlemeg46c  37199  cdlemeg46fvaw  37202  cdlemeg46req  37215  cdleme48fgv  37224  cdlemf1  37247  cdlemg1cex  37274  cdlemg2dN  37276  cdlemg2ce  37278  cdlemg12e  37333  cdlemg35  37399  cdlemh  37503  tendocan  37510  cdlemk28-3  37594  tendoex  37661  dih1  37972  dihmeetlem9N  38001  dihlspsnssN  38018  dihlspsnat  38019  lcfrlem23  38251  expgcd  38724  mzpsubst  38849  rencldnfi  38922  irrapx1  38929  pellexlem3  38932  pellexlem5  38934  infmrgelbi  38979  pellqrex  38980  pellfundge  38983  rmspecfund  39010  congtr  39066  acongeq  39084  jm2.20nn  39098  jm2.25lem1  39099  jm2.26  39103  expdiophlem1  39122  hbtlem2  39228  suprleubrd  40021  suprlubrd  40025  suprnmpt  40989  wessf1ornlem  41004  mpct  41023  upbdrech  41132  ssfiunibd  41136  uzfissfz  41154  xleadd2d  41155  suprltrp  41156  xleadd1d  41157  suprleubrnmpt  41257  iccintsng  41360  limcrecl  41471  fnlimfvre  41516  dvmulcncf  41771  dvdivcncf  41773  dvbdfbdioolem1  41774  ioodvbdlimc1lem2  41778  ioodvbdlimc2lem  41780  stoweidlem1  41848  stoweidlem20  41867  stoweidlem24  41871  stoweidlem34  41881  stoweidlem45  41892  stoweidlem60  41907  fourierdlem20  41974  fourierdlem31  41985  fourierdlem38  41992  fourierdlem64  42017  fourierdlem79  42032  fourierdlem94  42047  fourierdlem113  42066  fouriersw  42078  fouriercn  42079  sge0isum  42271  hoicvr  42392  ovnsubaddlem2  42415  hoidmv1lelem1  42435  hoidmv1lelem3  42437  hoidmvlelem1  42439  hoidmvlelem4  42442  smflimlem2  42610  fmtnof1  43199  lighneallem2  43273  upgrwlkupwlk  43517  lincresunit3  44036  elbigolo1  44118  eenglngeehlnm  44227