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  4483  raaanv  4484  raaan2  4487  copsex2dv  5457  soltmin  6112  xpdifid  6144  reuop  6269  f1dom3fv3dif  7246  f1prex  7262  cocan1  7269  fliftfun  7290  soisores  7305  soisoi  7306  isopolem  7323  f1oiso2  7330  weniso  7332  caovcld  7585  caovcomd  7588  onminex  7781  poxp2  8125  poxp3  8132  poseq  8140  tfrlem12  8360  omeulem1  8549  nnaordex2  8606  oaabs2  8616  omabs  8618  eldifsucnn  8631  naddcllem  8643  erov  8790  findcard2d  9136  frfi  9239  finsschain  9317  suplub2  9419  supgtoreq  9429  supisolem  9432  ordiso2  9475  ordtypelem7  9484  wemaplem2  9507  wemapsolem  9510  cantnflt  9632  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  wemapwe  9657  cnfcomlem  9659  cnfcom  9660  cnfcom3lem  9663  infxpenlem  9973  fseqenlem1  9984  dfac12lem2  10105  infpssrlem4  10266  enfin2i  10281  isf34lem7  10339  isf34lem6  10340  fin1a2lem7  10366  fin1a2lem10  10369  fin1a2lem11  10370  fin1a2lem13  10372  ttukeylem6  10474  ttukeylem7  10475  iundom2g  10500  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  fpwwe2lem11  10601  fpwwe2  10603  canthnumlem  10608  canthwelem  10610  canthp1lem2  10613  pwfseqlem4  10622  inar1  10735  intgru  10774  distrlem4pr  10986  conjmul  11906  lediv12a  12083  recp1lt1  12088  cju  12189  gtndiv  12618  zsupss  12903  uzsupss  12906  icc0  13361  iccssioo2  13387  fzrev3  13558  ico01fl0  13788  fldiv  13829  modabs  13873  modltm1p1mod  13895  modifeq2int  13905  modsumfzodifsn  13916  seqcaopr  14011  seqf1olem1  14013  seqof2  14032  crreczi  14200  seqcoll  14436  seqcoll2  14437  hashtpg  14457  swrdccat3b  14712  01sqrexlem2  15216  resqrex  15223  abs1m  15309  isercoll  15641  zsum  15691  fsum2dlem  15743  fsumcom2  15747  fprod2dlem  15953  fprodcom2  15957  efsub  16075  bitsinv2  16420  sqgcd  16539  expgcd  16540  qredeu  16635  isprm7  16685  pcpremul  16821  pceulem  16823  pczpre  16825  pcdiv  16830  pcqmul  16831  pcqdiv  16835  pcexp  16837  pcdvdsb  16847  pcneg  16852  pcdvdstr  16854  pcgcd1  16855  pc2dvds  16857  pcz  16859  pcaddlem  16866  pcadd  16867  qexpz  16879  expnprm  16880  infpnlem2  16889  ramub2  16992  ramub1lem1  17004  setsstruct2  17151  f1ocpbllem  17494  f1ovscpbl  17496  mreexexlem3d  17614  mreexexlem4d  17615  fthi  17889  ipodrsima  18507  mgmpropd  18585  sgrppropd  18665  mndpropd  18693  grpsubpropd2  18985  f1ghm0to0  19184  ghmqusker  19226  symgfvne  19318  f1omvdmvd  19380  f1otrspeq  19384  pmtrdifwrdel  19422  pmtrdifwrdel2  19423  psgnunilem2  19432  psgnunilem3  19433  psgnvalii  19446  odf1  19499  lsmpropd  19614  ablnnncan  19759  gsummptshft  19873  dprdf1o  19971  pgpfac1lem3  20016  pgpfac1lem5  20018  pgpfaclem1  20020  ablfaclem2  20025  rngpropd  20090  srgbinomlem3  20144  ringpropd  20204  lmodprop2d  20837  lsspropd  20931  lmhmpropd  20987  lbspropd  21013  lbsextlem3  21077  iporthcom  21551  obslbs  21646  assapropd  21788  psrass1  21880  psrass23l  21883  psrass23  21885  mplsubrg  21921  mplmon  21949  mplmonmul  21950  mplcoe1  21951  mplbas2  21956  mplind  21984  evlslem2  21993  mpfind  22021  gsumply1subr  22125  psrplusgpropd  22127  ply1scln0  22185  evls1addd  22265  evls1muld  22266  evls1vsca  22267  asclply1subcl  22268  scmataddcl  22410  scmatsubcl  22411  scmatmulcl  22412  smatvscl  22418  scmatrhmcl  22422  mat1scmat  22433  smadiadetglem2  22566  cramerimplem2  22578  cramerimplem3  22579  cramerimp  22580  1pmatscmul  22596  mat2pmatf1  22623  pm2mp  22719  chmatcl  22722  chmatval  22723  chmaidscmat  22742  chfacfisf  22748  cayhamlem1  22760  cpmidgsumm2pm  22763  cpmidpmat  22767  cpmadugsumfi  22771  cpmadumatpoly  22777  cayhamlem3  22781  pptbas  22902  elcls  22967  neiint  22998  neiptopnei  23026  restbas  23052  neitr  23074  iscnp4  23157  cnconst2  23177  cnpdis  23187  cnt0  23240  cnhaus  23248  cmpcovf  23285  hauscmplem  23300  conncompid  23325  2ndci  23342  2ndc1stc  23345  1stcrest  23347  2ndcctbss  23349  2ndcomap  23352  2ndcsep  23353  dis2ndc  23354  restlly  23377  islly2  23378  lly1stc  23390  dislly  23391  finlocfin  23414  dissnlocfin  23423  locfindis  23424  llycmpkgen2  23444  ptbasfi  23475  neitx  23501  ptpjopn  23506  ptcnplem  23515  upxp  23517  txlly  23530  txtube  23534  tx1stc  23544  txkgen  23546  xkococnlem  23553  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  hmeoimaf1o  23664  reghmph  23687  nrmhmph  23688  ordthmeolem  23695  trfil2  23781  fmfnfm  23852  hauspwpwf1  23881  fclsfnflim  23921  cnextf  23960  cnextcn  23961  tmdgsum2  23990  symgtgp  24000  subgntr  24001  opnsubg  24002  ghmcnp  24009  qustgpopn  24014  tsmsf1o  24039  tsmsxplem1  24047  tsmsxplem2  24048  tsmsxp  24049  ustexsym  24110  restutop  24132  imasdsf1olem  24268  blssexps  24321  blssex  24322  ssblex  24323  imasf1oxms  24384  blcld  24400  stdbdmopn  24413  met1stc  24416  met2ndci  24417  prdsxmslem2  24424  metcnp3  24435  cfilucfil  24454  ngptgp  24531  tgioo  24691  tgqioo  24695  zdis  24712  iccpnfhmeo  24850  xrhmeo  24851  cnheibor  24861  elpi1i  24953  cmetcusp  25261  bncssbn  25281  pjthlem2  25345  ivthlem2  25360  ovolicc1  25424  ovolicc2lem3  25427  ovolicc2lem4  25428  volsup  25464  volivth  25515  vitalilem3  25518  mbflimsup  25574  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem5  25627  limcnlp  25786  limcflf  25789  limciun  25802  dvmptfsum  25886  dvcnvlem  25887  dvcvx  25932  facth1  26079  elply2  26108  plypf1  26124  coeeq  26139  aaliou3lem8  26260  ulm2  26301  mtestbdd  26321  reeff1o  26364  logbgcd1irr  26711  dcubic2  26761  quart  26778  xrlimcnp  26885  amgm  26908  harmonicbnd4  26928  perfect  27149  dchrptlem1  27182  bposlem2  27203  lgsfcl2  27221  lgsdir  27250  lgsdi  27252  lgsne0  27253  2lgslem1a1  27307  2sqmod  27354  dchrvmasumlem2  27416  chpdifbndlem2  27472  pntpbnd1  27504  pntpbnd2  27505  padicabv  27548  sltres  27581  nolesgn2o  27590  nogesgn1o  27592  nodense  27611  nosupbnd1lem3  27629  nosupbnd1lem5  27631  nosupbnd2lem1  27634  noinfres  27641  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd2lem1  27649  noetalem1  27660  nocvxmin  27697  noeta2  27703  onscutlt  28172  eucliddivs  28272  readdscl  28357  tgcgrxfr  28452  idmot  28471  legid  28521  btwnleg  28522  leg0  28526  tghilberti1  28571  mirreu3  28588  colperpex  28667  lnopp2hpgb  28697  axcgrrflx  28848  axsegconlem1  28851  axcontlem2  28899  axcontlem12  28909  eengtrkg  28920  wwlksnredwwlkn  29832  0wlkon  30056  0trlon  30060  upgr3v3e3cycl  30116  frgrogt3nreg  30333  nvpi  30603  nmlno0lem  30729  fh1  31554  fh2  31555  nmlnop0iALT  31931  nmopun  31950  branmfn  32041  opsqrlem1  32076  opsqrlem6  32081  mdslmd1lem1  32261  csmdsymi  32270  atom1d  32289  chirredlem2  32327  cdj1i  32369  cdj3i  32377  fcnvgreu  32604  suppovss  32611  xrofsup  32697  nn0difffzod  32736  sgnmul  32767  pwrssmgc  32933  chnind  32944  gsummpt2d  32996  gsumhashmul  33008  odpmco  33050  cycpmco2lem6  33095  cycpmco2  33097  cyc3evpm  33114  cycpmconjslem2  33119  archirngz  33150  archiabllem2a  33155  elrgspnlem4  33203  rloc0g  33229  rloc1r  33230  domnpropd  33234  sdrgdvcl  33256  sdrginvcl  33257  orngsqr  33289  ornglmullt  33292  orngrmullt  33293  lindssn  33356  lindfpropd  33360  ssdifidllem  33434  ssmxidllem  33451  rsprprmprmidlb  33501  rprmirredb  33510  1arithufd  33526  ply1asclunit  33550  ply1dg1rt  33555  ply1dg3rt0irred  33558  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  lsssra  33591  lindsun  33628  dimkerim  33630  fedgmullem2  33633  fldextrspunlem1  33677  fldextrspunfld  33678  irngss  33689  irngnzply1  33693  algextdeglem2  33715  algextdeglem4  33717  constrext2chnlem  33747  metideq  33890  metider  33891  pstmfval  33893  lmxrge0  33949  qqhval2  33979  qqhf  33983  qqhghm  33985  qqhrhm  33986  esumpcvgval  34075  esum2dlem  34089  esum2d  34090  sigainb  34133  insiga  34134  ddemeas  34233  imambfm  34260  dya2icoseg  34275  dya2iocnrect  34279  eulerpartlemgvv  34374  probun  34417  ballotlemfc0  34491  ballotlemfcc  34492  breprexplemc  34630  erdszelem8  35192  erdszelem9  35193  erdsze2lem2  35198  cnpconn  35224  txpconn  35226  ptpconn  35227  indispconn  35228  connpconn  35229  cvxpconn  35236  cnllysconn  35239  cvmcov2  35269  cvmopnlem  35272  cvmliftmolem1  35275  cvmliftlem14  35291  cvmliftlem15  35292  cvmlift2lem13  35309  cvmlift3lem2  35314  cvmlift3lem9  35321  seglerflx  36107  seglemin  36108  btwnsegle  36112  hilbert1.1  36149  neibastop2lem  36355  weiunfrlem  36459  weiunso  36461  bj-finsumval0  37280  relowlssretop  37358  wl-2sb6d  37553  tan2h  37613  poimirlem1  37622  poimirlem3  37624  poimirlem4  37625  poimirlem9  37630  poimirlem22  37643  poimirlem28  37649  heicant  37656  mblfinlem2  37659  itg2addnc  37675  ftc2nc  37703  dvasin  37705  sdclem1  37744  fdc  37746  istotbnd3  37772  sstotbnd  37776  prdstotbnd  37795  prdsbnd2  37796  cntotbnd  37797  rngoisocnv  37982  lsmsat  39008  islfld  39062  ps-2  39479  lplnexllnN  39565  4atlem9  39604  4atlem10a  39605  lnatexN  39780  2lnat  39785  pmapjat1  39854  lhpj1  40023  lhpm0atN  40030  4atexlemex2  40072  4atex  40077  4atex2-0aOLDN  40079  4atex2-0cOLDN  40081  lautcnvle  40090  lautj  40094  lautm  40095  idltrn  40151  cdleme01N  40222  cdleme0ex1N  40224  cdleme5  40241  cdleme9  40254  cdleme11c  40262  cdleme11g  40266  cdlemefrs29bpre0  40397  cdlemefrs29cpre1  40399  cdlemefrs32fva1  40402  cdleme32fva  40438  cdleme32fva1  40439  cdleme32fvaw  40440  cdleme32d  40445  cdleme32f  40447  cdleme35fnpq  40450  cdleme48d  40536  cdleme48gfv  40538  cdleme50ltrn  40558  trlord  40570  cdlemg4b1  40610  cdlemg4b2  40611  cdlemg13a  40652  cdlemg17a  40662  cdlemg17f  40667  erng1lem  40988  erngdvlem3  40991  erngdvlem4  40992  erng1r  40996  erngdvlem3-rN  40999  erngdvlem4-rN  41000  dva0g  41028  dialss  41047  dia0  41053  dia1N  41054  diaglbN  41056  diameetN  41057  diainN  41058  diaintclN  41059  dia1dim  41062  dia2dimlem5  41069  dia2dimlem7  41071  dia2dimlem9  41073  dia2dimlem10  41074  dia2dimlem12  41076  dia2dimlem13  41077  dvhopvadd  41094  dvhvaddass  41098  dvhopvsca  41103  tendolinv  41106  tendorinv  41107  dvhlveclem  41109  dvh0g  41112  dvheveccl  41113  dvhopN  41117  docaclN  41125  diaocN  41126  djajN  41138  dib0  41165  dib1dim  41166  dibglbN  41167  dibintclN  41168  dib1dim2  41169  diblss  41171  diblsmopel  41172  dicvaddcl  41191  dicvscacl  41192  diclspsn  41195  cdlemn4a  41200  cdlemn11c  41210  dihjustlem  41217  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord2cN  41222  dihord11b  41223  dihord11c  41225  dihord2pre  41226  dihlsscpre  41235  dih1dimb  41241  dib2dim  41244  dih2dimb  41245  dih2dimbALTN  41246  dihvalcq2  41248  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihord5apre  41263  dih0  41281  dihmeetlem1N  41291  dihglblem5apreN  41292  dihglblem3N  41296  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetlem4preN  41307  dih1dimatlem0  41329  dih1dimatlem  41330  dihatlat  41335  dihatexv  41339  dihglb2  41343  dihmeet  41344  dihintcl  41345  dihmeet2  41347  doch2val2  41365  dochocss  41367  dihoml4c  41377  dochdmj1  41391  djhlj  41402  djhljjN  41403  djhjlj  41404  dihsumssj  41409  djhexmid  41412  djhlsmcl  41415  djhcvat42  41416  dihjatcclem4  41422  dihjat1lem  41429  dihsmsprn  41431  dihjat3  41433  dvh3dim2  41449  dvh3dim3N  41450  dochkr1OLDN  41480  lclkrlem2c  41510  lclkrlem2d  41511  mapdpglem23  41695  hdmap11lem2  41843  0prjspn  42623  mzpcompact2lem  42746  diophrw  42754  rexrabdioph  42789  eldioph4b  42806  pellexlem5  42828  pellfund14  42893  acongtr  42974  fnwe2lem3  43048  gicabl  43095  hbtlem2  43120  hbtlem4  43122  hbtlem5  43124  dgraalem  43141  aaitgo  43158  onexlimgt  43239  onexoegt  43240  oalim2cl  43285  cantnfresb  43320  onmcl  43327  tfsconcatfv  43337  tfsconcatrn  43338  ofoaid1  43354  ofoaid2  43355  ntrclsk13  44067  gneispb  44127  wessf1ornlem  45186  ltdiv23neg  45397  islptre  45624  limclner  45656  icccncfext  45892  stoweidlem1  46006  stoweidlem14  46019  stoweidlem24  46029  stoweidlem46  46051  stoweidlem57  46062  dirkercncflem2  46109  fourierdlem20  46132  fourierdlem41  46153  fourierdlem46  46157  fourierdlem48  46159  fourierdlem50  46161  fourierdlem62  46173  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem76  46187  fourierdlem79  46190  fourierdlem103  46214  fourierdlem104  46215  etransclem47  46286  m1modmmod  47363  iccpartiun  47439  reupr  47527  sqrtpwpw2p  47543  fmtnoprmfac1lem  47569  fmtnoprmfac2lem1  47571  lighneallem4a  47613  requad2  47628  perfectALTV  47728  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  isuspgrim0lem  47897  isuspgrim0  47898  isuspgrimlem  47899  upgrimwlklem2  47902  upgrimwlklem3  47903  upgrimtrlslem1  47908  uhgrimisgrgriclem  47934  uhgrimisgrgric  47935  clnbgrgrimlem  47937  grimgrtri  47952  gpgedgvtx1  48057  gpgedg2ov  48061  gpgedg2iv  48062  gsumlsscl  48372  lincsumcl  48424  lincscmcl  48425  isldepslvec2  48478  elbigo2  48545  relogbdivb  48555  blennnt2  48582  dignn0ldlem  48595  itsclc0yqsollem2  48756  inlinecirc02p  48780  lubeldm2  48948  glbeldm2  48949  lubsscl  48952  glbsscl  48953  isclatd  48975  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  uptrlem1  49203  fucofulem1  49303  fullthinc  49443