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 585	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  4473  raaanv  4474  raaan2  4477  copsex2dv  5452  soltmin  6103  xpdifid  6136  reuop  6261  f1dom3fv3dif  7226  f1prex  7242  cocan1  7249  fliftfun  7270  soisores  7285  soisoi  7286  isopolem  7303  f1oiso2  7310  weniso  7312  caovcld  7563  caovcomd  7566  onminex  7759  poxp2  8097  poxp3  8104  poseq  8112  tfrlem12  8332  omeulem1  8521  nnaordex2  8579  oaabs2  8589  omabs  8591  eldifsucnn  8604  naddcllem  8616  erov  8765  findcard2d  9105  frfi  9199  finsschain  9273  suplub2  9378  supgtoreq  9388  supisolem  9391  ordiso2  9434  ordtypelem7  9443  wemaplem2  9466  wemapsolem  9469  cantnflt  9595  cantnfp1lem3  9603  cantnflem1b  9609  cantnflem1  9612  wemapwe  9620  cnfcomlem  9622  cnfcom  9623  cnfcom3lem  9626  infxpenlem  9937  fseqenlem1  9948  dfac12lem2  10069  infpssrlem4  10230  enfin2i  10245  isf34lem7  10303  isf34lem6  10304  fin1a2lem7  10330  fin1a2lem10  10333  fin1a2lem11  10334  fin1a2lem13  10336  ttukeylem6  10438  ttukeylem7  10439  iundom2g  10464  fpwwe2lem5  10560  fpwwe2lem6  10561  fpwwe2lem8  10563  fpwwe2lem11  10566  fpwwe2  10568  canthnumlem  10573  canthwelem  10575  canthp1lem2  10578  pwfseqlem4  10587  inar1  10700  intgru  10739  distrlem4pr  10951  conjmul  11872  lediv12a  12049  recp1lt1  12054  cju  12155  gtndiv  12583  zsupss  12864  uzsupss  12867  icc0  13323  iccssioo2  13349  fzrev3  13520  ico01fl0  13753  fldiv  13794  modabs  13838  modltm1p1mod  13860  modifeq2int  13870  modsumfzodifsn  13881  seqcaopr  13976  seqf1olem1  13978  seqof2  13997  crreczi  14165  seqcoll  14401  seqcoll2  14402  hashtpg  14422  swrdccat3b  14677  01sqrexlem2  15180  resqrex  15187  abs1m  15273  isercoll  15605  zsum  15655  fsum2dlem  15707  fsumcom2  15711  fprod2dlem  15917  fprodcom2  15921  efsub  16039  bitsinv2  16384  sqgcd  16503  expgcd  16504  qredeu  16599  isprm7  16649  pcpremul  16785  pceulem  16787  pczpre  16789  pcdiv  16794  pcqmul  16795  pcqdiv  16799  pcexp  16801  pcdvdsb  16811  pcneg  16816  pcdvdstr  16818  pcgcd1  16819  pc2dvds  16821  pcz  16823  pcaddlem  16830  pcadd  16831  qexpz  16843  expnprm  16844  infpnlem2  16853  ramub2  16956  ramub1lem1  16968  setsstruct2  17115  f1ocpbllem  17459  f1ovscpbl  17461  mreexexlem3d  17583  mreexexlem4d  17584  fthi  17858  ipodrsima  18478  chnind  18558  mgmpropd  18590  sgrppropd  18670  mndpropd  18698  grpsubpropd2  18993  f1ghm0to0  19191  ghmqusker  19233  symgfvne  19327  f1omvdmvd  19389  f1otrspeq  19393  pmtrdifwrdel  19431  pmtrdifwrdel2  19432  psgnunilem2  19441  psgnunilem3  19442  psgnvalii  19455  odf1  19508  lsmpropd  19623  ablnnncan  19768  gsummptshft  19882  dprdf1o  19980  pgpfac1lem3  20025  pgpfac1lem5  20027  pgpfaclem1  20029  ablfaclem2  20034  rngpropd  20126  srgbinomlem3  20180  ringpropd  20240  orngsqr  20816  ornglmullt  20819  orngrmullt  20820  lmodprop2d  20892  lsspropd  20986  lmhmpropd  21042  lbspropd  21068  lbsextlem3  21132  iporthcom  21607  obslbs  21702  assapropd  21844  psrass1  21936  psrass23l  21939  psrass23  21941  mplsubrg  21977  mplmon  22007  mplmonmul  22008  mplcoe1  22009  mplbas2  22014  mplind  22042  evlslem2  22051  mpfind  22087  gsumply1subr  22191  psrplusgpropd  22193  ply1scln0  22251  evls1addd  22332  evls1muld  22333  evls1vsca  22334  asclply1subcl  22335  scmataddcl  22477  scmatsubcl  22478  scmatmulcl  22479  smatvscl  22485  scmatrhmcl  22489  mat1scmat  22500  smadiadetglem2  22633  cramerimplem2  22645  cramerimplem3  22646  cramerimp  22647  1pmatscmul  22663  mat2pmatf1  22690  pm2mp  22786  chmatcl  22789  chmatval  22790  chmaidscmat  22809  chfacfisf  22815  cayhamlem1  22827  cpmidgsumm2pm  22830  cpmidpmat  22834  cpmadugsumfi  22838  cpmadumatpoly  22844  cayhamlem3  22848  pptbas  22969  elcls  23034  neiint  23065  neiptopnei  23093  restbas  23119  neitr  23141  iscnp4  23224  cnconst2  23244  cnpdis  23254  cnt0  23307  cnhaus  23315  cmpcovf  23352  hauscmplem  23367  conncompid  23392  2ndci  23409  2ndc1stc  23412  1stcrest  23414  2ndcctbss  23416  2ndcomap  23419  2ndcsep  23420  dis2ndc  23421  restlly  23444  islly2  23445  lly1stc  23457  dislly  23458  finlocfin  23481  dissnlocfin  23490  locfindis  23491  llycmpkgen2  23511  ptbasfi  23542  neitx  23568  ptpjopn  23573  ptcnplem  23582  upxp  23584  txlly  23597  txtube  23601  tx1stc  23611  txkgen  23613  xkococnlem  23620  kqreglem1  23702  kqreglem2  23703  kqnrmlem1  23704  kqnrmlem2  23705  hmeoimaf1o  23731  reghmph  23754  nrmhmph  23755  ordthmeolem  23762  trfil2  23848  fmfnfm  23919  hauspwpwf1  23948  fclsfnflim  23988  cnextf  24027  cnextcn  24028  tmdgsum2  24057  symgtgp  24067  subgntr  24068  opnsubg  24069  ghmcnp  24076  qustgpopn  24081  tsmsf1o  24106  tsmsxplem1  24114  tsmsxplem2  24115  tsmsxp  24116  ustexsym  24177  restutop  24198  imasdsf1olem  24334  blssexps  24387  blssex  24388  ssblex  24389  imasf1oxms  24450  blcld  24466  stdbdmopn  24479  met1stc  24482  met2ndci  24483  prdsxmslem2  24490  metcnp3  24501  cfilucfil  24520  ngptgp  24597  tgioo  24757  tgqioo  24761  zdis  24778  iccpnfhmeo  24916  xrhmeo  24917  cnheibor  24927  elpi1i  25019  cmetcusp  25327  bncssbn  25347  pjthlem2  25411  ivthlem2  25426  ovolicc1  25490  ovolicc2lem3  25493  ovolicc2lem4  25494  volsup  25530  volivth  25581  vitalilem3  25584  mbflimsup  25640  mbfi1fseqlem1  25689  mbfi1fseqlem3  25691  mbfi1fseqlem5  25693  limcnlp  25852  limcflf  25855  limciun  25868  dvmptfsum  25952  dvcnvlem  25953  dvcvx  25998  facth1  26145  elply2  26174  plypf1  26190  coeeq  26205  aaliou3lem8  26326  ulm2  26367  mtestbdd  26387  reeff1o  26430  logbgcd1irr  26777  dcubic2  26827  quart  26844  xrlimcnp  26951  amgm  26974  harmonicbnd4  26994  perfect  27215  dchrptlem1  27248  bposlem2  27269  lgsfcl2  27287  lgsdir  27316  lgsdi  27318  lgsne0  27319  2lgslem1a1  27373  2sqmod  27420  dchrvmasumlem2  27482  chpdifbndlem2  27538  pntpbnd1  27570  pntpbnd2  27571  padicabv  27614  ltsres  27647  nolesgn2o  27656  nogesgn1o  27658  nodense  27677  nosupbnd1lem3  27695  nosupbnd1lem5  27697  nosupbnd2lem1  27700  noinfres  27707  noinfbnd1lem3  27710  noinfbnd1lem5  27712  noinfbnd2lem1  27715  noetalem1  27726  nocvxmin  27768  noeta2  27774  oncutlt  28277  eucliddivs  28389  readdscl  28512  tgcgrxfr  28608  idmot  28627  legid  28677  btwnleg  28678  leg0  28682  tghilberti1  28727  mirreu3  28744  colperpex  28823  lnopp2hpgb  28853  axcgrrflx  29005  axsegconlem1  29008  axcontlem2  29056  axcontlem12  29066  eengtrkg  29077  wwlksnredwwlkn  29986  0wlkon  30213  0trlon  30217  upgr3v3e3cycl  30273  frgrogt3nreg  30490  nvpi  30761  nmlno0lem  30887  fh1  31712  fh2  31713  nmlnop0iALT  32089  nmopun  32108  branmfn  32199  opsqrlem1  32234  opsqrlem6  32239  mdslmd1lem1  32419  csmdsymi  32428  atom1d  32447  chirredlem2  32485  cdj1i  32527  cdj3i  32535  fcnvgreu  32768  suppovss  32777  xrofsup  32864  nn0difffzod  32901  sgnmul  32933  pwrssmgc  33099  gsummpt2d  33149  gsumhashmul  33167  odpmco  33186  cycpmco2lem6  33231  cycpmco2  33233  cyc3evpm  33250  cycpmconjslem2  33255  fxpsubg  33273  fxpsdrg  33275  archirngz  33289  archiabllem2a  33294  elrgspnlem4  33345  rloc0g  33371  rloc1r  33372  domnpropd  33377  sdrgdvcl  33399  sdrginvcl  33400  lindssn  33477  lindfpropd  33481  ssdifidllem  33555  ssmxidllem  33572  rsprprmprmidlb  33622  rprmirredb  33631  1arithufd  33647  ply1asclunit  33673  ply1dg1rt  33679  ply1dg3rt0irred  33683  ply1degltel  33693  ply1degleel  33694  ply1degltlss  33695  psrmonmul  33733  esplyind  33758  esplyindfv  33759  lsssra  33771  lindsun  33809  dimkerim  33811  fedgmullem2  33814  fldextrspunlem1  33859  fldextrspunfld  33860  irngss  33871  irngnzply1  33875  algextdeglem2  33902  algextdeglem4  33904  constrext2chnlem  33934  metideq  34077  metider  34078  pstmfval  34080  lmxrge0  34136  qqhval2  34166  qqhf  34170  qqhghm  34172  qqhrhm  34173  esumpcvgval  34262  esum2dlem  34276  esum2d  34277  sigainb  34320  insiga  34321  ddemeas  34420  imambfm  34446  dya2icoseg  34461  dya2iocnrect  34465  eulerpartlemgvv  34560  probun  34603  ballotlemfc0  34677  ballotlemfcc  34678  breprexplemc  34816  erdszelem8  35420  erdszelem9  35421  erdsze2lem2  35426  cnpconn  35452  txpconn  35454  ptpconn  35455  indispconn  35456  connpconn  35457  cvxpconn  35464  cnllysconn  35467  cvmcov2  35497  cvmopnlem  35500  cvmliftmolem1  35503  cvmliftlem14  35519  cvmliftlem15  35520  cvmlift2lem13  35537  cvmlift3lem2  35542  cvmlift3lem9  35549  seglerflx  36334  seglemin  36335  btwnsegle  36339  hilbert1.1  36376  neibastop2lem  36582  weiunfrlem  36686  weiunso  36688  bj-finsumval0  37567  relowlssretop  37645  wl-2sb6d  37842  tan2h  37892  poimirlem1  37901  poimirlem3  37903  poimirlem4  37904  poimirlem9  37909  poimirlem22  37922  poimirlem28  37928  heicant  37935  mblfinlem2  37938  itg2addnc  37954  ftc2nc  37982  dvasin  37984  sdclem1  38023  fdc  38025  istotbnd3  38051  sstotbnd  38055  prdstotbnd  38074  prdsbnd2  38075  cntotbnd  38076  rngoisocnv  38261  lsmsat  39413  islfld  39467  ps-2  39883  lplnexllnN  39969  4atlem9  40008  4atlem10a  40009  lnatexN  40184  2lnat  40189  pmapjat1  40258  lhpj1  40427  lhpm0atN  40434  4atexlemex2  40476  4atex  40481  4atex2-0aOLDN  40483  4atex2-0cOLDN  40485  lautcnvle  40494  lautj  40498  lautm  40499  idltrn  40555  cdleme01N  40626  cdleme0ex1N  40628  cdleme5  40645  cdleme9  40658  cdleme11c  40666  cdleme11g  40670  cdlemefrs29bpre0  40801  cdlemefrs29cpre1  40803  cdlemefrs32fva1  40806  cdleme32fva  40842  cdleme32fva1  40843  cdleme32fvaw  40844  cdleme32d  40849  cdleme32f  40851  cdleme35fnpq  40854  cdleme48d  40940  cdleme48gfv  40942  cdleme50ltrn  40962  trlord  40974  cdlemg4b1  41014  cdlemg4b2  41015  cdlemg13a  41056  cdlemg17a  41066  cdlemg17f  41071  erng1lem  41392  erngdvlem3  41395  erngdvlem4  41396  erng1r  41400  erngdvlem3-rN  41403  erngdvlem4-rN  41404  dva0g  41432  dialss  41451  dia0  41457  dia1N  41458  diaglbN  41460  diameetN  41461  diainN  41462  diaintclN  41463  dia1dim  41466  dia2dimlem5  41473  dia2dimlem7  41475  dia2dimlem9  41477  dia2dimlem10  41478  dia2dimlem12  41480  dia2dimlem13  41481  dvhopvadd  41498  dvhvaddass  41502  dvhopvsca  41507  tendolinv  41510  tendorinv  41511  dvhlveclem  41513  dvh0g  41516  dvheveccl  41517  dvhopN  41521  docaclN  41529  diaocN  41530  djajN  41542  dib0  41569  dib1dim  41570  dibglbN  41571  dibintclN  41572  dib1dim2  41573  diblss  41575  diblsmopel  41576  dicvaddcl  41595  dicvscacl  41596  diclspsn  41599  cdlemn4a  41604  cdlemn11c  41614  dihjustlem  41621  dihord1  41623  dihord2a  41624  dihord2b  41625  dihord2cN  41626  dihord11b  41627  dihord11c  41629  dihord2pre  41630  dihlsscpre  41639  dih1dimb  41645  dib2dim  41648  dih2dimb  41649  dih2dimbALTN  41650  dihvalcq2  41652  dihopelvalcpre  41653  dihord6apre  41661  dihord5b  41664  dihord5apre  41667  dih0  41685  dihmeetlem1N  41695  dihglblem5apreN  41696  dihglblem3N  41700  dihmeetlem2N  41704  dihglbcpreN  41705  dihmeetlem4preN  41711  dih1dimatlem0  41733  dih1dimatlem  41734  dihatlat  41739  dihatexv  41743  dihglb2  41747  dihmeet  41748  dihintcl  41749  dihmeet2  41751  doch2val2  41769  dochocss  41771  dihoml4c  41781  dochdmj1  41795  djhlj  41806  djhljjN  41807  djhjlj  41808  dihsumssj  41813  djhexmid  41816  djhlsmcl  41819  djhcvat42  41820  dihjatcclem4  41826  dihjat1lem  41833  dihsmsprn  41835  dihjat3  41837  dvh3dim2  41853  dvh3dim3N  41854  dochkr1OLDN  41884  lclkrlem2c  41914  lclkrlem2d  41915  mapdpglem23  42099  hdmap11lem2  42247  0prjspn  43015  mzpcompact2lem  43137  diophrw  43145  rexrabdioph  43180  eldioph4b  43197  pellexlem5  43219  pellfund14  43284  acongtr  43364  fnwe2lem3  43438  gicabl  43485  hbtlem2  43510  hbtlem4  43512  hbtlem5  43514  dgraalem  43531  aaitgo  43548  onexlimgt  43629  onexoegt  43630  oalim2cl  43675  cantnfresb  43710  onmcl  43717  tfsconcatfv  43727  tfsconcatrn  43728  ofoaid1  43744  ofoaid2  43745  ntrclsk13  44456  gneispb  44516  wessf1ornlem  45573  ltdiv23neg  45781  islptre  46008  limclner  46038  icccncfext  46274  stoweidlem1  46388  stoweidlem14  46401  stoweidlem24  46411  stoweidlem46  46433  stoweidlem57  46444  dirkercncflem2  46491  fourierdlem20  46514  fourierdlem41  46535  fourierdlem46  46539  fourierdlem48  46541  fourierdlem50  46543  fourierdlem62  46555  fourierdlem63  46556  fourierdlem64  46557  fourierdlem65  46558  fourierdlem76  46569  fourierdlem79  46572  fourierdlem103  46596  fourierdlem104  46597  etransclem47  46668  m1modmmod  47747  iccpartiun  47823  reupr  47911  sqrtpwpw2p  47927  fmtnoprmfac1lem  47953  fmtnoprmfac2lem1  47955  lighneallem4a  47997  requad2  48012  perfectALTV  48112  nnsum4primeseven  48189  nnsum4primesevenALTV  48190  isuspgrim0lem  48282  isuspgrim0  48283  isuspgrimlem  48284  upgrimwlklem2  48287  upgrimwlklem3  48288  upgrimtrlslem1  48293  uhgrimisgrgriclem  48319  uhgrimisgrgric  48320  clnbgrgrimlem  48322  grimgrtri  48338  gpgedgvtx1  48451  gpgedg2ov  48455  gpgedg2iv  48456  gsumlsscl  48769  lincsumcl  48820  lincscmcl  48821  isldepslvec2  48874  elbigo2  48941  relogbdivb  48951  blennnt2  48978  dignn0ldlem  48991  itsclc0yqsollem2  49152  inlinecirc02p  49176  lubeldm2  49344  glbeldm2  49345  lubsscl  49348  glbsscl  49349  isclatd  49371  sectpropdlem  49424  invpropdlem  49426  isopropdlem  49428  uptrlem1  49598  fucofulem1  49698  fullthinc  49838