Theorem syl12anc 836

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  838  raaan  4471  raaanv  4472  raaan2  4475  copsex2dv  5442  soltmin  6093  xpdifid  6126  reuop  6251  f1dom3fv3dif  7214  f1prex  7230  cocan1  7237  fliftfun  7258  soisores  7273  soisoi  7274  isopolem  7291  f1oiso2  7298  weniso  7300  caovcld  7551  caovcomd  7554  onminex  7747  poxp2  8085  poxp3  8092  poseq  8100  tfrlem12  8320  omeulem1  8509  nnaordex2  8567  oaabs2  8577  omabs  8579  eldifsucnn  8592  naddcllem  8604  erov  8751  findcard2d  9091  frfi  9185  finsschain  9259  suplub2  9364  supgtoreq  9374  supisolem  9377  ordiso2  9420  ordtypelem7  9429  wemaplem2  9452  wemapsolem  9455  cantnflt  9581  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1  9598  wemapwe  9606  cnfcomlem  9608  cnfcom  9609  cnfcom3lem  9612  infxpenlem  9923  fseqenlem1  9934  dfac12lem2  10055  infpssrlem4  10216  enfin2i  10231  isf34lem7  10289  isf34lem6  10290  fin1a2lem7  10316  fin1a2lem10  10319  fin1a2lem11  10320  fin1a2lem13  10322  ttukeylem6  10424  ttukeylem7  10425  iundom2g  10450  fpwwe2lem5  10546  fpwwe2lem6  10547  fpwwe2lem8  10549  fpwwe2lem11  10552  fpwwe2  10554  canthnumlem  10559  canthwelem  10561  canthp1lem2  10564  pwfseqlem4  10573  inar1  10686  intgru  10725  distrlem4pr  10937  conjmul  11858  lediv12a  12035  recp1lt1  12040  cju  12141  gtndiv  12569  zsupss  12850  uzsupss  12853  icc0  13309  iccssioo2  13335  fzrev3  13506  ico01fl0  13739  fldiv  13780  modabs  13824  modltm1p1mod  13846  modifeq2int  13856  modsumfzodifsn  13867  seqcaopr  13962  seqf1olem1  13964  seqof2  13983  crreczi  14151  seqcoll  14387  seqcoll2  14388  hashtpg  14408  swrdccat3b  14663  01sqrexlem2  15166  resqrex  15173  abs1m  15259  isercoll  15591  zsum  15641  fsum2dlem  15693  fsumcom2  15697  fprod2dlem  15903  fprodcom2  15907  efsub  16025  bitsinv2  16370  sqgcd  16489  expgcd  16490  qredeu  16585  isprm7  16635  pcpremul  16771  pceulem  16773  pczpre  16775  pcdiv  16780  pcqmul  16781  pcqdiv  16785  pcexp  16787  pcdvdsb  16797  pcneg  16802  pcdvdstr  16804  pcgcd1  16805  pc2dvds  16807  pcz  16809  pcaddlem  16816  pcadd  16817  qexpz  16829  expnprm  16830  infpnlem2  16839  ramub2  16942  ramub1lem1  16954  setsstruct2  17101  f1ocpbllem  17445  f1ovscpbl  17447  mreexexlem3d  17569  mreexexlem4d  17570  fthi  17844  ipodrsima  18464  chnind  18544  mgmpropd  18576  sgrppropd  18656  mndpropd  18684  grpsubpropd2  18976  f1ghm0to0  19174  ghmqusker  19216  symgfvne  19310  f1omvdmvd  19372  f1otrspeq  19376  pmtrdifwrdel  19414  pmtrdifwrdel2  19415  psgnunilem2  19424  psgnunilem3  19425  psgnvalii  19438  odf1  19491  lsmpropd  19606  ablnnncan  19751  gsummptshft  19865  dprdf1o  19963  pgpfac1lem3  20008  pgpfac1lem5  20010  pgpfaclem1  20012  ablfaclem2  20017  rngpropd  20109  srgbinomlem3  20163  ringpropd  20223  orngsqr  20799  ornglmullt  20802  orngrmullt  20803  lmodprop2d  20875  lsspropd  20969  lmhmpropd  21025  lbspropd  21051  lbsextlem3  21115  iporthcom  21590  obslbs  21685  assapropd  21827  psrass1  21919  psrass23l  21922  psrass23  21924  mplsubrg  21960  mplmon  21990  mplmonmul  21991  mplcoe1  21992  mplbas2  21997  mplind  22025  evlslem2  22034  mpfind  22070  gsumply1subr  22174  psrplusgpropd  22176  ply1scln0  22234  evls1addd  22315  evls1muld  22316  evls1vsca  22317  asclply1subcl  22318  scmataddcl  22460  scmatsubcl  22461  scmatmulcl  22462  smatvscl  22468  scmatrhmcl  22472  mat1scmat  22483  smadiadetglem2  22616  cramerimplem2  22628  cramerimplem3  22629  cramerimp  22630  1pmatscmul  22646  mat2pmatf1  22673  pm2mp  22769  chmatcl  22772  chmatval  22773  chmaidscmat  22792  chfacfisf  22798  cayhamlem1  22810  cpmidgsumm2pm  22813  cpmidpmat  22817  cpmadugsumfi  22821  cpmadumatpoly  22827  cayhamlem3  22831  pptbas  22952  elcls  23017  neiint  23048  neiptopnei  23076  restbas  23102  neitr  23124  iscnp4  23207  cnconst2  23227  cnpdis  23237  cnt0  23290  cnhaus  23298  cmpcovf  23335  hauscmplem  23350  conncompid  23375  2ndci  23392  2ndc1stc  23395  1stcrest  23397  2ndcctbss  23399  2ndcomap  23402  2ndcsep  23403  dis2ndc  23404  restlly  23427  islly2  23428  lly1stc  23440  dislly  23441  finlocfin  23464  dissnlocfin  23473  locfindis  23474  llycmpkgen2  23494  ptbasfi  23525  neitx  23551  ptpjopn  23556  ptcnplem  23565  upxp  23567  txlly  23580  txtube  23584  tx1stc  23594  txkgen  23596  xkococnlem  23603  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  hmeoimaf1o  23714  reghmph  23737  nrmhmph  23738  ordthmeolem  23745  trfil2  23831  fmfnfm  23902  hauspwpwf1  23931  fclsfnflim  23971  cnextf  24010  cnextcn  24011  tmdgsum2  24040  symgtgp  24050  subgntr  24051  opnsubg  24052  ghmcnp  24059  qustgpopn  24064  tsmsf1o  24089  tsmsxplem1  24097  tsmsxplem2  24098  tsmsxp  24099  ustexsym  24160  restutop  24181  imasdsf1olem  24317  blssexps  24370  blssex  24371  ssblex  24372  imasf1oxms  24433  blcld  24449  stdbdmopn  24462  met1stc  24465  met2ndci  24466  prdsxmslem2  24473  metcnp3  24484  cfilucfil  24503  ngptgp  24580  tgioo  24740  tgqioo  24744  zdis  24761  iccpnfhmeo  24899  xrhmeo  24900  cnheibor  24910  elpi1i  25002  cmetcusp  25310  bncssbn  25330  pjthlem2  25394  ivthlem2  25409  ovolicc1  25473  ovolicc2lem3  25476  ovolicc2lem4  25477  volsup  25513  volivth  25564  vitalilem3  25567  mbflimsup  25623  mbfi1fseqlem1  25672  mbfi1fseqlem3  25674  mbfi1fseqlem5  25676  limcnlp  25835  limcflf  25838  limciun  25851  dvmptfsum  25935  dvcnvlem  25936  dvcvx  25981  facth1  26128  elply2  26157  plypf1  26173  coeeq  26188  aaliou3lem8  26309  ulm2  26350  mtestbdd  26370  reeff1o  26413  logbgcd1irr  26760  dcubic2  26810  quart  26827  xrlimcnp  26934  amgm  26957  harmonicbnd4  26977  perfect  27198  dchrptlem1  27231  bposlem2  27252  lgsfcl2  27270  lgsdir  27299  lgsdi  27301  lgsne0  27302  2lgslem1a1  27356  2sqmod  27403  dchrvmasumlem2  27465  chpdifbndlem2  27521  pntpbnd1  27553  pntpbnd2  27554  padicabv  27597  ltsres  27630  nolesgn2o  27639  nogesgn1o  27641  nodense  27660  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfres  27690  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2lem1  27698  noetalem1  27709  nocvxmin  27751  noeta2  27757  oncutlt  28260  eucliddivs  28372  readdscl  28495  tgcgrxfr  28590  idmot  28609  legid  28659  btwnleg  28660  leg0  28664  tghilberti1  28709  mirreu3  28726  colperpex  28805  lnopp2hpgb  28835  axcgrrflx  28987  axsegconlem1  28990  axcontlem2  29038  axcontlem12  29048  eengtrkg  29059  wwlksnredwwlkn  29968  0wlkon  30195  0trlon  30199  upgr3v3e3cycl  30255  frgrogt3nreg  30472  nvpi  30742  nmlno0lem  30868  fh1  31693  fh2  31694  nmlnop0iALT  32070  nmopun  32089  branmfn  32180  opsqrlem1  32215  opsqrlem6  32220  mdslmd1lem1  32400  csmdsymi  32409  atom1d  32428  chirredlem2  32466  cdj1i  32508  cdj3i  32516  fcnvgreu  32751  suppovss  32760  xrofsup  32847  nn0difffzod  32884  sgnmul  32916  pwrssmgc  33082  gsummpt2d  33132  gsumhashmul  33150  odpmco  33168  cycpmco2lem6  33213  cycpmco2  33215  cyc3evpm  33232  cycpmconjslem2  33237  fxpsubg  33255  fxpsdrg  33257  archirngz  33271  archiabllem2a  33276  elrgspnlem4  33327  rloc0g  33353  rloc1r  33354  domnpropd  33359  sdrgdvcl  33381  sdrginvcl  33382  lindssn  33459  lindfpropd  33463  ssdifidllem  33537  ssmxidllem  33554  rsprprmprmidlb  33604  rprmirredb  33613  1arithufd  33629  ply1asclunit  33655  ply1dg1rt  33661  ply1dg3rt0irred  33665  ply1degltel  33675  ply1degleel  33676  ply1degltlss  33677  esplyind  33731  esplyindfv  33732  lsssra  33744  lindsun  33782  dimkerim  33784  fedgmullem2  33787  fldextrspunlem1  33832  fldextrspunfld  33833  irngss  33844  irngnzply1  33848  algextdeglem2  33875  algextdeglem4  33877  constrext2chnlem  33907  metideq  34050  metider  34051  pstmfval  34053  lmxrge0  34109  qqhval2  34139  qqhf  34143  qqhghm  34145  qqhrhm  34146  esumpcvgval  34235  esum2dlem  34249  esum2d  34250  sigainb  34293  insiga  34294  ddemeas  34393  imambfm  34419  dya2icoseg  34434  dya2iocnrect  34438  eulerpartlemgvv  34533  probun  34576  ballotlemfc0  34650  ballotlemfcc  34651  breprexplemc  34789  erdszelem8  35392  erdszelem9  35393  erdsze2lem2  35398  cnpconn  35424  txpconn  35426  ptpconn  35427  indispconn  35428  connpconn  35429  cvxpconn  35436  cnllysconn  35439  cvmcov2  35469  cvmopnlem  35472  cvmliftmolem1  35475  cvmliftlem14  35491  cvmliftlem15  35492  cvmlift2lem13  35509  cvmlift3lem2  35514  cvmlift3lem9  35521  seglerflx  36306  seglemin  36307  btwnsegle  36311  hilbert1.1  36348  neibastop2lem  36554  weiunfrlem  36658  weiunso  36660  bj-finsumval0  37486  relowlssretop  37564  wl-2sb6d  37759  tan2h  37809  poimirlem1  37818  poimirlem3  37820  poimirlem4  37821  poimirlem9  37826  poimirlem22  37839  poimirlem28  37845  heicant  37852  mblfinlem2  37855  itg2addnc  37871  ftc2nc  37899  dvasin  37901  sdclem1  37940  fdc  37942  istotbnd3  37968  sstotbnd  37972  prdstotbnd  37991  prdsbnd2  37992  cntotbnd  37993  rngoisocnv  38178  lsmsat  39264  islfld  39318  ps-2  39734  lplnexllnN  39820  4atlem9  39859  4atlem10a  39860  lnatexN  40035  2lnat  40040  pmapjat1  40109  lhpj1  40278  lhpm0atN  40285  4atexlemex2  40327  4atex  40332  4atex2-0aOLDN  40334  4atex2-0cOLDN  40336  lautcnvle  40345  lautj  40349  lautm  40350  idltrn  40406  cdleme01N  40477  cdleme0ex1N  40479  cdleme5  40496  cdleme9  40509  cdleme11c  40517  cdleme11g  40521  cdlemefrs29bpre0  40652  cdlemefrs29cpre1  40654  cdlemefrs32fva1  40657  cdleme32fva  40693  cdleme32fva1  40694  cdleme32fvaw  40695  cdleme32d  40700  cdleme32f  40702  cdleme35fnpq  40705  cdleme48d  40791  cdleme48gfv  40793  cdleme50ltrn  40813  trlord  40825  cdlemg4b1  40865  cdlemg4b2  40866  cdlemg13a  40907  cdlemg17a  40917  cdlemg17f  40922  erng1lem  41243  erngdvlem3  41246  erngdvlem4  41247  erng1r  41251  erngdvlem3-rN  41254  erngdvlem4-rN  41255  dva0g  41283  dialss  41302  dia0  41308  dia1N  41309  diaglbN  41311  diameetN  41312  diainN  41313  diaintclN  41314  dia1dim  41317  dia2dimlem5  41324  dia2dimlem7  41326  dia2dimlem9  41328  dia2dimlem10  41329  dia2dimlem12  41331  dia2dimlem13  41332  dvhopvadd  41349  dvhvaddass  41353  dvhopvsca  41358  tendolinv  41361  tendorinv  41362  dvhlveclem  41364  dvh0g  41367  dvheveccl  41368  dvhopN  41372  docaclN  41380  diaocN  41381  djajN  41393  dib0  41420  dib1dim  41421  dibglbN  41422  dibintclN  41423  dib1dim2  41424  diblss  41426  diblsmopel  41427  dicvaddcl  41446  dicvscacl  41447  diclspsn  41450  cdlemn4a  41455  cdlemn11c  41465  dihjustlem  41472  dihord1  41474  dihord2a  41475  dihord2b  41476  dihord2cN  41477  dihord11b  41478  dihord11c  41480  dihord2pre  41481  dihlsscpre  41490  dih1dimb  41496  dib2dim  41499  dih2dimb  41500  dih2dimbALTN  41501  dihvalcq2  41503  dihopelvalcpre  41504  dihord6apre  41512  dihord5b  41515  dihord5apre  41518  dih0  41536  dihmeetlem1N  41546  dihglblem5apreN  41547  dihglblem3N  41551  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetlem4preN  41562  dih1dimatlem0  41584  dih1dimatlem  41585  dihatlat  41590  dihatexv  41594  dihglb2  41598  dihmeet  41599  dihintcl  41600  dihmeet2  41602  doch2val2  41620  dochocss  41622  dihoml4c  41632  dochdmj1  41646  djhlj  41657  djhljjN  41658  djhjlj  41659  dihsumssj  41664  djhexmid  41667  djhlsmcl  41670  djhcvat42  41671  dihjatcclem4  41677  dihjat1lem  41684  dihsmsprn  41686  dihjat3  41688  dvh3dim2  41704  dvh3dim3N  41705  dochkr1OLDN  41735  lclkrlem2c  41765  lclkrlem2d  41766  mapdpglem23  41950  hdmap11lem2  42098  0prjspn  42867  mzpcompact2lem  42989  diophrw  42997  rexrabdioph  43032  eldioph4b  43049  pellexlem5  43071  pellfund14  43136  acongtr  43216  fnwe2lem3  43290  gicabl  43337  hbtlem2  43362  hbtlem4  43364  hbtlem5  43366  dgraalem  43383  aaitgo  43400  onexlimgt  43481  onexoegt  43482  oalim2cl  43527  cantnfresb  43562  onmcl  43569  tfsconcatfv  43579  tfsconcatrn  43580  ofoaid1  43596  ofoaid2  43597  ntrclsk13  44308  gneispb  44368  wessf1ornlem  45425  ltdiv23neg  45634  islptre  45861  limclner  45891  icccncfext  46127  stoweidlem1  46241  stoweidlem14  46254  stoweidlem24  46264  stoweidlem46  46286  stoweidlem57  46297  dirkercncflem2  46344  fourierdlem20  46367  fourierdlem41  46388  fourierdlem46  46392  fourierdlem48  46394  fourierdlem50  46396  fourierdlem62  46408  fourierdlem63  46409  fourierdlem64  46410  fourierdlem65  46411  fourierdlem76  46422  fourierdlem79  46425  fourierdlem103  46449  fourierdlem104  46450  etransclem47  46521  m1modmmod  47600  iccpartiun  47676  reupr  47764  sqrtpwpw2p  47780  fmtnoprmfac1lem  47806  fmtnoprmfac2lem1  47808  lighneallem4a  47850  requad2  47865  perfectALTV  47965  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  isuspgrim0lem  48135  isuspgrim0  48136  isuspgrimlem  48137  upgrimwlklem2  48140  upgrimwlklem3  48141  upgrimtrlslem1  48146  uhgrimisgrgriclem  48172  uhgrimisgrgric  48173  clnbgrgrimlem  48175  grimgrtri  48191  gpgedgvtx1  48304  gpgedg2ov  48308  gpgedg2iv  48309  gsumlsscl  48622  lincsumcl  48673  lincscmcl  48674  isldepslvec2  48727  elbigo2  48794  relogbdivb  48804  blennnt2  48831  dignn0ldlem  48844  itsclc0yqsollem2  49005  inlinecirc02p  49029  lubeldm2  49197  glbeldm2  49198  lubsscl  49201  glbsscl  49202  isclatd  49224  sectpropdlem  49277  invpropdlem  49279  isopropdlem  49281  uptrlem1  49451  fucofulem1  49551  fullthinc  49691