Theorem syl12anc 837

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

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

Assertion

Ref	Expression
syl12anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl12anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	1, 4, 5	syl2anc 584	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  syl22anc  839  raaan  4517  raaanv  4518  raaan2  4521  copsex2dv  5499  soltmin  6156  xpdifid  6188  reuop  6313  f1dom3fv3dif  7288  f1prex  7304  cocan1  7311  fliftfun  7332  soisores  7347  soisoi  7348  isopolem  7365  f1oiso2  7372  weniso  7374  caovcld  7626  caovcomd  7629  onminex  7822  poxp2  8168  poxp3  8175  poseq  8183  tfrlem12  8429  omeulem1  8620  nnaordex2  8677  oaabs2  8687  omabs  8689  eldifsucnn  8702  naddcllem  8714  erov  8854  findcard2d  9206  frfi  9321  finsschain  9399  suplub2  9501  supgtoreq  9510  supisolem  9513  ordiso2  9555  ordtypelem7  9564  wemaplem2  9587  wemapsolem  9590  cantnflt  9712  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  wemapwe  9737  cnfcomlem  9739  cnfcom  9740  cnfcom3lem  9743  infxpenlem  10053  fseqenlem1  10064  dfac12lem2  10185  infpssrlem4  10346  enfin2i  10361  isf34lem7  10419  isf34lem6  10420  fin1a2lem7  10446  fin1a2lem10  10449  fin1a2lem11  10450  fin1a2lem13  10452  ttukeylem6  10554  ttukeylem7  10555  iundom2g  10580  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  fpwwe2lem11  10681  fpwwe2  10683  canthnumlem  10688  canthwelem  10690  canthp1lem2  10693  pwfseqlem4  10702  inar1  10815  intgru  10854  distrlem4pr  11066  conjmul  11984  lediv12a  12161  recp1lt1  12166  cju  12262  gtndiv  12695  zsupss  12979  uzsupss  12982  icc0  13435  iccssioo2  13460  fzrev3  13630  ico01fl0  13859  fldiv  13900  modabs  13944  modltm1p1mod  13964  modifeq2int  13974  modsumfzodifsn  13985  seqcaopr  14080  seqf1olem1  14082  seqof2  14101  crreczi  14267  seqcoll  14503  seqcoll2  14504  hashtpg  14524  swrdccat3b  14778  01sqrexlem2  15282  resqrex  15289  abs1m  15374  isercoll  15704  zsum  15754  fsum2dlem  15806  fsumcom2  15810  fprod2dlem  16016  fprodcom2  16020  efsub  16136  bitsinv2  16480  sqgcd  16599  expgcd  16600  qredeu  16695  isprm7  16745  pcpremul  16881  pceulem  16883  pczpre  16885  pcdiv  16890  pcqmul  16891  pcqdiv  16895  pcexp  16897  pcdvdsb  16907  pcneg  16912  pcdvdstr  16914  pcgcd1  16915  pc2dvds  16917  pcz  16919  pcaddlem  16926  pcadd  16927  qexpz  16939  expnprm  16940  infpnlem2  16949  ramub2  17052  ramub1lem1  17064  setsstruct2  17211  f1ocpbllem  17569  f1ovscpbl  17571  mreexexlem3d  17689  mreexexlem4d  17690  fthi  17965  ipodrsima  18586  mgmpropd  18664  sgrppropd  18744  mndpropd  18772  grpsubpropd2  19064  f1ghm0to0  19263  ghmqusker  19305  symgfvne  19398  f1omvdmvd  19461  f1otrspeq  19465  pmtrdifwrdel  19503  pmtrdifwrdel2  19504  psgnunilem2  19513  psgnunilem3  19514  psgnvalii  19527  odf1  19580  lsmpropd  19695  ablnnncan  19840  gsummptshft  19954  dprdf1o  20052  pgpfac1lem3  20097  pgpfac1lem5  20099  pgpfaclem1  20101  ablfaclem2  20106  rngpropd  20171  srgbinomlem3  20225  ringpropd  20285  lmodprop2d  20922  lsspropd  21016  lmhmpropd  21072  lbspropd  21098  lbsextlem3  21162  iporthcom  21653  obslbs  21750  assapropd  21892  psrass1  21984  psrass23l  21987  psrass23  21989  mplsubrg  22025  mplmon  22053  mplmonmul  22054  mplcoe1  22055  mplbas2  22060  mplind  22094  evlslem2  22103  mpfind  22131  gsumply1subr  22235  psrplusgpropd  22237  ply1scln0  22295  evls1addd  22375  evls1muld  22376  evls1vsca  22377  asclply1subcl  22378  scmataddcl  22522  scmatsubcl  22523  scmatmulcl  22524  smatvscl  22530  scmatrhmcl  22534  mat1scmat  22545  smadiadetglem2  22678  cramerimplem2  22690  cramerimplem3  22691  cramerimp  22692  1pmatscmul  22708  mat2pmatf1  22735  pm2mp  22831  chmatcl  22834  chmatval  22835  chmaidscmat  22854  chfacfisf  22860  cayhamlem1  22872  cpmidgsumm2pm  22875  cpmidpmat  22879  cpmadugsumfi  22883  cpmadumatpoly  22889  cayhamlem3  22893  pptbas  23015  elcls  23081  neiint  23112  neiptopnei  23140  restbas  23166  neitr  23188  iscnp4  23271  cnconst2  23291  cnpdis  23301  cnt0  23354  cnhaus  23362  cmpcovf  23399  hauscmplem  23414  conncompid  23439  2ndci  23456  2ndc1stc  23459  1stcrest  23461  2ndcctbss  23463  2ndcomap  23466  2ndcsep  23467  dis2ndc  23468  restlly  23491  islly2  23492  lly1stc  23504  dislly  23505  finlocfin  23528  dissnlocfin  23537  locfindis  23538  llycmpkgen2  23558  ptbasfi  23589  neitx  23615  ptpjopn  23620  ptcnplem  23629  upxp  23631  txlly  23644  txtube  23648  tx1stc  23658  txkgen  23660  xkococnlem  23667  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  hmeoimaf1o  23778  reghmph  23801  nrmhmph  23802  ordthmeolem  23809  trfil2  23895  fmfnfm  23966  hauspwpwf1  23995  fclsfnflim  24035  cnextf  24074  cnextcn  24075  tmdgsum2  24104  symgtgp  24114  subgntr  24115  opnsubg  24116  ghmcnp  24123  qustgpopn  24128  tsmsf1o  24153  tsmsxplem1  24161  tsmsxplem2  24162  tsmsxp  24163  ustexsym  24224  restutop  24246  imasdsf1olem  24383  blssexps  24436  blssex  24437  ssblex  24438  imasf1oxms  24502  blcld  24518  stdbdmopn  24531  met1stc  24534  met2ndci  24535  prdsxmslem2  24542  metcnp3  24553  cfilucfil  24572  ngptgp  24649  tgioo  24817  tgqioo  24821  zdis  24838  iccpnfhmeo  24976  xrhmeo  24977  cnheibor  24987  elpi1i  25079  cmetcusp  25388  bncssbn  25408  pjthlem2  25472  ivthlem2  25487  ovolicc1  25551  ovolicc2lem3  25554  ovolicc2lem4  25555  volsup  25591  volivth  25642  vitalilem3  25645  mbflimsup  25701  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem5  25754  limcnlp  25913  limcflf  25916  limciun  25929  dvmptfsum  26013  dvcnvlem  26014  dvcvx  26059  facth1  26206  elply2  26235  plypf1  26251  coeeq  26266  aaliou3lem8  26387  ulm2  26428  mtestbdd  26448  reeff1o  26491  logbgcd1irr  26837  dcubic2  26887  quart  26904  xrlimcnp  27011  amgm  27034  harmonicbnd4  27054  perfect  27275  dchrptlem1  27308  bposlem2  27329  lgsfcl2  27347  lgsdir  27376  lgsdi  27378  lgsne0  27379  2lgslem1a1  27433  2sqmod  27480  dchrvmasumlem2  27542  chpdifbndlem2  27598  pntpbnd1  27630  pntpbnd2  27631  padicabv  27674  sltres  27707  nolesgn2o  27716  nogesgn1o  27718  nodense  27737  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfres  27767  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  noetalem1  27786  nocvxmin  27823  noeta2  27829  readdscl  28431  tgcgrxfr  28526  idmot  28545  legid  28595  btwnleg  28596  leg0  28600  tghilberti1  28645  mirreu3  28662  colperpex  28741  lnopp2hpgb  28771  axcgrrflx  28929  axsegconlem1  28932  axcontlem2  28980  axcontlem12  28990  eengtrkg  29001  wwlksnredwwlkn  29915  0wlkon  30139  0trlon  30143  upgr3v3e3cycl  30199  frgrogt3nreg  30416  nvpi  30686  nmlno0lem  30812  fh1  31637  fh2  31638  nmlnop0iALT  32014  nmopun  32033  branmfn  32124  opsqrlem1  32159  opsqrlem6  32164  mdslmd1lem1  32344  csmdsymi  32353  atom1d  32372  chirredlem2  32410  cdj1i  32452  cdj3i  32460  fcnvgreu  32683  suppovss  32690  xrofsup  32771  nn0difffzod  32808  pwrssmgc  32990  chnind  33001  gsummpt2d  33052  gsumhashmul  33064  odpmco  33106  cycpmco2lem6  33151  cycpmco2  33153  cyc3evpm  33170  cycpmconjslem2  33175  archirngz  33196  archiabllem2a  33201  elrgspnlem4  33249  rloc0g  33275  rloc1r  33276  domnpropd  33280  sdrgdvcl  33301  sdrginvcl  33302  orngsqr  33334  ornglmullt  33337  orngrmullt  33338  lindssn  33406  lindfpropd  33410  ssdifidllem  33484  ssmxidllem  33501  rsprprmprmidlb  33551  rprmirredb  33560  1arithufd  33576  ply1asclunit  33599  ply1dg1rt  33604  ply1dg3rt0irred  33607  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  lsssra  33639  lindsun  33676  dimkerim  33678  fedgmullem2  33681  fldextrspunlem1  33725  fldextrspunfld  33726  irngss  33737  irngnzply1  33741  algextdeglem2  33759  algextdeglem4  33761  metideq  33892  metider  33893  pstmfval  33895  lmxrge0  33951  qqhval2  33983  qqhf  33987  qqhghm  33989  qqhrhm  33990  esumpcvgval  34079  esum2dlem  34093  esum2d  34094  sigainb  34137  insiga  34138  ddemeas  34237  imambfm  34264  dya2icoseg  34279  dya2iocnrect  34283  eulerpartlemgvv  34378  probun  34421  ballotlemfc0  34495  ballotlemfcc  34496  sgnmul  34545  breprexplemc  34647  erdszelem8  35203  erdszelem9  35204  erdsze2lem2  35209  cnpconn  35235  txpconn  35237  ptpconn  35238  indispconn  35239  connpconn  35240  cvxpconn  35247  cnllysconn  35250  cvmcov2  35280  cvmopnlem  35283  cvmliftmolem1  35286  cvmliftlem14  35302  cvmliftlem15  35303  cvmlift2lem13  35320  cvmlift3lem2  35325  cvmlift3lem9  35332  seglerflx  36113  seglemin  36114  btwnsegle  36118  hilbert1.1  36155  neibastop2lem  36361  weiunfrlem  36465  weiunso  36467  bj-finsumval0  37286  relowlssretop  37364  wl-2sb6d  37559  tan2h  37619  poimirlem1  37628  poimirlem3  37630  poimirlem4  37631  poimirlem9  37636  poimirlem22  37649  poimirlem28  37655  heicant  37662  mblfinlem2  37665  itg2addnc  37681  ftc2nc  37709  dvasin  37711  sdclem1  37750  fdc  37752  istotbnd3  37778  sstotbnd  37782  prdstotbnd  37801  prdsbnd2  37802  cntotbnd  37803  rngoisocnv  37988  lsmsat  39009  islfld  39063  ps-2  39480  lplnexllnN  39566  4atlem9  39605  4atlem10a  39606  lnatexN  39781  2lnat  39786  pmapjat1  39855  lhpj1  40024  lhpm0atN  40031  4atexlemex2  40073  4atex  40078  4atex2-0aOLDN  40080  4atex2-0cOLDN  40082  lautcnvle  40091  lautj  40095  lautm  40096  idltrn  40152  cdleme01N  40223  cdleme0ex1N  40225  cdleme5  40242  cdleme9  40255  cdleme11c  40263  cdleme11g  40267  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdlemefrs32fva1  40403  cdleme32fva  40439  cdleme32fva1  40440  cdleme32fvaw  40441  cdleme32d  40446  cdleme32f  40448  cdleme35fnpq  40451  cdleme48d  40537  cdleme48gfv  40539  cdleme50ltrn  40559  trlord  40571  cdlemg4b1  40611  cdlemg4b2  40612  cdlemg13a  40653  cdlemg17a  40663  cdlemg17f  40668  erng1lem  40989  erngdvlem3  40992  erngdvlem4  40993  erng1r  40997  erngdvlem3-rN  41000  erngdvlem4-rN  41001  dva0g  41029  dialss  41048  dia0  41054  dia1N  41055  diaglbN  41057  diameetN  41058  diainN  41059  diaintclN  41060  dia1dim  41063  dia2dimlem5  41070  dia2dimlem7  41072  dia2dimlem9  41074  dia2dimlem10  41075  dia2dimlem12  41077  dia2dimlem13  41078  dvhopvadd  41095  dvhvaddass  41099  dvhopvsca  41104  tendolinv  41107  tendorinv  41108  dvhlveclem  41110  dvh0g  41113  dvheveccl  41114  dvhopN  41118  docaclN  41126  diaocN  41127  djajN  41139  dib0  41166  dib1dim  41167  dibglbN  41168  dibintclN  41169  dib1dim2  41170  diblss  41172  diblsmopel  41173  dicvaddcl  41192  dicvscacl  41193  diclspsn  41196  cdlemn4a  41201  cdlemn11c  41211  dihjustlem  41218  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord2cN  41223  dihord11b  41224  dihord11c  41226  dihord2pre  41227  dihlsscpre  41236  dih1dimb  41242  dib2dim  41245  dih2dimb  41246  dih2dimbALTN  41247  dihvalcq2  41249  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dih0  41282  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem3N  41297  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetlem4preN  41308  dih1dimatlem0  41330  dih1dimatlem  41331  dihatlat  41336  dihatexv  41340  dihglb2  41344  dihmeet  41345  dihintcl  41346  dihmeet2  41348  doch2val2  41366  dochocss  41368  dihoml4c  41378  dochdmj1  41392  djhlj  41403  djhljjN  41404  djhjlj  41405  dihsumssj  41410  djhexmid  41413  djhlsmcl  41416  djhcvat42  41417  dihjatcclem4  41423  dihjat1lem  41430  dihsmsprn  41432  dihjat3  41434  dvh3dim2  41450  dvh3dim3N  41451  dochkr1OLDN  41481  lclkrlem2c  41511  lclkrlem2d  41512  mapdpglem23  41696  hdmap11lem2  41844  0prjspn  42638  mzpcompact2lem  42762  diophrw  42770  rexrabdioph  42805  eldioph4b  42822  pellexlem5  42844  pellfund14  42909  acongtr  42990  fnwe2lem3  43064  gicabl  43111  hbtlem2  43136  hbtlem4  43138  hbtlem5  43140  dgraalem  43157  aaitgo  43174  onexlimgt  43255  onexoegt  43256  oalim2cl  43302  cantnfresb  43337  onmcl  43344  tfsconcatfv  43354  tfsconcatrn  43355  ofoaid1  43371  ofoaid2  43372  ntrclsk13  44084  gneispb  44144  wessf1ornlem  45190  ltdiv23neg  45405  islptre  45634  limclner  45666  icccncfext  45902  stoweidlem1  46016  stoweidlem14  46029  stoweidlem24  46039  stoweidlem46  46061  stoweidlem57  46072  dirkercncflem2  46119  fourierdlem20  46142  fourierdlem41  46163  fourierdlem46  46167  fourierdlem48  46169  fourierdlem50  46171  fourierdlem62  46183  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem76  46197  fourierdlem79  46200  fourierdlem103  46224  fourierdlem104  46225  etransclem47  46296  iccpartiun  47421  reupr  47509  sqrtpwpw2p  47525  fmtnoprmfac1lem  47551  fmtnoprmfac2lem1  47553  lighneallem4a  47595  requad2  47610  perfectALTV  47710  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  isuspgrim0lem  47871  isuspgrim0  47872  isuspgrimlem  47874  uhgrimisgrgriclem  47898  uhgrimisgrgric  47899  clnbgrgrimlem  47901  grimgrtri  47916  gpgedgvtx1  48020  gsumlsscl  48296  lincsumcl  48348  lincscmcl  48349  isldepslvec2  48402  m1modmmod  48442  elbigo2  48473  relogbdivb  48483  blennnt2  48510  dignn0ldlem  48523  itsclc0yqsollem2  48684  inlinecirc02p  48708  lubeldm2  48853  glbeldm2  48854  lubsscl  48857  glbsscl  48858  isclatd  48872  fucofulem1  49005  fullthinc  49099