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  4467  raaanv  4468  raaan2  4471  copsex2dv  5434  soltmin  6083  xpdifid  6115  reuop  6240  f1dom3fv3dif  7202  f1prex  7218  cocan1  7225  fliftfun  7246  soisores  7261  soisoi  7262  isopolem  7279  f1oiso2  7286  weniso  7288  caovcld  7539  caovcomd  7542  onminex  7735  poxp2  8073  poxp3  8080  poseq  8088  tfrlem12  8308  omeulem1  8497  nnaordex2  8554  oaabs2  8564  omabs  8566  eldifsucnn  8579  naddcllem  8591  erov  8738  findcard2d  9076  frfi  9169  finsschain  9243  suplub2  9345  supgtoreq  9355  supisolem  9358  ordiso2  9401  ordtypelem7  9410  wemaplem2  9433  wemapsolem  9436  cantnflt  9562  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1  9579  wemapwe  9587  cnfcomlem  9589  cnfcom  9590  cnfcom3lem  9593  infxpenlem  9901  fseqenlem1  9912  dfac12lem2  10033  infpssrlem4  10194  enfin2i  10209  isf34lem7  10267  isf34lem6  10268  fin1a2lem7  10294  fin1a2lem10  10297  fin1a2lem11  10298  fin1a2lem13  10300  ttukeylem6  10402  ttukeylem7  10403  iundom2g  10428  fpwwe2lem5  10523  fpwwe2lem6  10524  fpwwe2lem8  10526  fpwwe2lem11  10529  fpwwe2  10531  canthnumlem  10536  canthwelem  10538  canthp1lem2  10541  pwfseqlem4  10550  inar1  10663  intgru  10702  distrlem4pr  10914  conjmul  11835  lediv12a  12012  recp1lt1  12017  cju  12118  gtndiv  12547  zsupss  12832  uzsupss  12835  icc0  13290  iccssioo2  13316  fzrev3  13487  ico01fl0  13720  fldiv  13761  modabs  13805  modltm1p1mod  13827  modifeq2int  13837  modsumfzodifsn  13848  seqcaopr  13943  seqf1olem1  13945  seqof2  13964  crreczi  14132  seqcoll  14368  seqcoll2  14369  hashtpg  14389  swrdccat3b  14644  01sqrexlem2  15147  resqrex  15154  abs1m  15240  isercoll  15572  zsum  15622  fsum2dlem  15674  fsumcom2  15678  fprod2dlem  15884  fprodcom2  15888  efsub  16006  bitsinv2  16351  sqgcd  16470  expgcd  16471  qredeu  16566  isprm7  16616  pcpremul  16752  pceulem  16754  pczpre  16756  pcdiv  16761  pcqmul  16762  pcqdiv  16766  pcexp  16768  pcdvdsb  16778  pcneg  16783  pcdvdstr  16785  pcgcd1  16786  pc2dvds  16788  pcz  16790  pcaddlem  16797  pcadd  16798  qexpz  16810  expnprm  16811  infpnlem2  16820  ramub2  16923  ramub1lem1  16935  setsstruct2  17082  f1ocpbllem  17425  f1ovscpbl  17427  mreexexlem3d  17549  mreexexlem4d  17550  fthi  17824  ipodrsima  18444  chnind  18524  mgmpropd  18556  sgrppropd  18636  mndpropd  18664  grpsubpropd2  18956  f1ghm0to0  19155  ghmqusker  19197  symgfvne  19291  f1omvdmvd  19353  f1otrspeq  19357  pmtrdifwrdel  19395  pmtrdifwrdel2  19396  psgnunilem2  19405  psgnunilem3  19406  psgnvalii  19419  odf1  19472  lsmpropd  19587  ablnnncan  19732  gsummptshft  19846  dprdf1o  19944  pgpfac1lem3  19989  pgpfac1lem5  19991  pgpfaclem1  19993  ablfaclem2  19998  rngpropd  20090  srgbinomlem3  20144  ringpropd  20204  orngsqr  20779  ornglmullt  20782  orngrmullt  20783  lmodprop2d  20855  lsspropd  20949  lmhmpropd  21005  lbspropd  21031  lbsextlem3  21095  iporthcom  21570  obslbs  21665  assapropd  21807  psrass1  21899  psrass23l  21902  psrass23  21904  mplsubrg  21940  mplmon  21968  mplmonmul  21969  mplcoe1  21970  mplbas2  21975  mplind  22003  evlslem2  22012  mpfind  22040  gsumply1subr  22144  psrplusgpropd  22146  ply1scln0  22204  evls1addd  22284  evls1muld  22285  evls1vsca  22286  asclply1subcl  22287  scmataddcl  22429  scmatsubcl  22430  scmatmulcl  22431  smatvscl  22437  scmatrhmcl  22441  mat1scmat  22452  smadiadetglem2  22585  cramerimplem2  22597  cramerimplem3  22598  cramerimp  22599  1pmatscmul  22615  mat2pmatf1  22642  pm2mp  22738  chmatcl  22741  chmatval  22742  chmaidscmat  22761  chfacfisf  22767  cayhamlem1  22779  cpmidgsumm2pm  22782  cpmidpmat  22786  cpmadugsumfi  22790  cpmadumatpoly  22796  cayhamlem3  22800  pptbas  22921  elcls  22986  neiint  23017  neiptopnei  23045  restbas  23071  neitr  23093  iscnp4  23176  cnconst2  23196  cnpdis  23206  cnt0  23259  cnhaus  23267  cmpcovf  23304  hauscmplem  23319  conncompid  23344  2ndci  23361  2ndc1stc  23364  1stcrest  23366  2ndcctbss  23368  2ndcomap  23371  2ndcsep  23372  dis2ndc  23373  restlly  23396  islly2  23397  lly1stc  23409  dislly  23410  finlocfin  23433  dissnlocfin  23442  locfindis  23443  llycmpkgen2  23463  ptbasfi  23494  neitx  23520  ptpjopn  23525  ptcnplem  23534  upxp  23536  txlly  23549  txtube  23553  tx1stc  23563  txkgen  23565  xkococnlem  23572  kqreglem1  23654  kqreglem2  23655  kqnrmlem1  23656  kqnrmlem2  23657  hmeoimaf1o  23683  reghmph  23706  nrmhmph  23707  ordthmeolem  23714  trfil2  23800  fmfnfm  23871  hauspwpwf1  23900  fclsfnflim  23940  cnextf  23979  cnextcn  23980  tmdgsum2  24009  symgtgp  24019  subgntr  24020  opnsubg  24021  ghmcnp  24028  qustgpopn  24033  tsmsf1o  24058  tsmsxplem1  24066  tsmsxplem2  24067  tsmsxp  24068  ustexsym  24129  restutop  24150  imasdsf1olem  24286  blssexps  24339  blssex  24340  ssblex  24341  imasf1oxms  24402  blcld  24418  stdbdmopn  24431  met1stc  24434  met2ndci  24435  prdsxmslem2  24442  metcnp3  24453  cfilucfil  24472  ngptgp  24549  tgioo  24709  tgqioo  24713  zdis  24730  iccpnfhmeo  24868  xrhmeo  24869  cnheibor  24879  elpi1i  24971  cmetcusp  25279  bncssbn  25299  pjthlem2  25363  ivthlem2  25378  ovolicc1  25442  ovolicc2lem3  25445  ovolicc2lem4  25446  volsup  25482  volivth  25533  vitalilem3  25536  mbflimsup  25592  mbfi1fseqlem1  25641  mbfi1fseqlem3  25643  mbfi1fseqlem5  25645  limcnlp  25804  limcflf  25807  limciun  25820  dvmptfsum  25904  dvcnvlem  25905  dvcvx  25950  facth1  26097  elply2  26126  plypf1  26142  coeeq  26157  aaliou3lem8  26278  ulm2  26319  mtestbdd  26339  reeff1o  26382  logbgcd1irr  26729  dcubic2  26779  quart  26796  xrlimcnp  26903  amgm  26926  harmonicbnd4  26946  perfect  27167  dchrptlem1  27200  bposlem2  27221  lgsfcl2  27239  lgsdir  27268  lgsdi  27270  lgsne0  27271  2lgslem1a1  27325  2sqmod  27372  dchrvmasumlem2  27434  chpdifbndlem2  27490  pntpbnd1  27522  pntpbnd2  27523  padicabv  27566  sltres  27599  nolesgn2o  27608  nogesgn1o  27610  nodense  27629  nosupbnd1lem3  27647  nosupbnd1lem5  27649  nosupbnd2lem1  27652  noinfres  27659  noinfbnd1lem3  27662  noinfbnd1lem5  27664  noinfbnd2lem1  27667  noetalem1  27678  nocvxmin  27716  noeta2  27722  onscutlt  28199  eucliddivs  28299  readdscl  28399  tgcgrxfr  28494  idmot  28513  legid  28563  btwnleg  28564  leg0  28568  tghilberti1  28613  mirreu3  28630  colperpex  28709  lnopp2hpgb  28739  axcgrrflx  28890  axsegconlem1  28893  axcontlem2  28941  axcontlem12  28951  eengtrkg  28962  wwlksnredwwlkn  29871  0wlkon  30095  0trlon  30099  upgr3v3e3cycl  30155  frgrogt3nreg  30372  nvpi  30642  nmlno0lem  30768  fh1  31593  fh2  31594  nmlnop0iALT  31970  nmopun  31989  branmfn  32080  opsqrlem1  32115  opsqrlem6  32120  mdslmd1lem1  32300  csmdsymi  32309  atom1d  32328  chirredlem2  32366  cdj1i  32408  cdj3i  32416  fcnvgreu  32650  suppovss  32657  xrofsup  32745  nn0difffzod  32781  sgnmul  32813  pwrssmgc  32976  gsummpt2d  33024  gsumhashmul  33036  odpmco  33050  cycpmco2lem6  33095  cycpmco2  33097  cyc3evpm  33114  cycpmconjslem2  33119  fxpsubg  33137  fxpsdrg  33139  archirngz  33153  archiabllem2a  33158  elrgspnlem4  33207  rloc0g  33233  rloc1r  33234  domnpropd  33238  sdrgdvcl  33260  sdrginvcl  33261  lindssn  33338  lindfpropd  33342  ssdifidllem  33416  ssmxidllem  33433  rsprprmprmidlb  33483  rprmirredb  33492  1arithufd  33508  ply1asclunit  33532  ply1dg1rt  33538  ply1dg3rt0irred  33541  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  lsssra  33595  lindsun  33633  dimkerim  33635  fedgmullem2  33638  fldextrspunlem1  33683  fldextrspunfld  33684  irngss  33695  irngnzply1  33699  algextdeglem2  33726  algextdeglem4  33728  constrext2chnlem  33758  metideq  33901  metider  33902  pstmfval  33904  lmxrge0  33960  qqhval2  33990  qqhf  33994  qqhghm  33996  qqhrhm  33997  esumpcvgval  34086  esum2dlem  34100  esum2d  34101  sigainb  34144  insiga  34145  ddemeas  34244  imambfm  34270  dya2icoseg  34285  dya2iocnrect  34289  eulerpartlemgvv  34384  probun  34427  ballotlemfc0  34501  ballotlemfcc  34502  breprexplemc  34640  erdszelem8  35230  erdszelem9  35231  erdsze2lem2  35236  cnpconn  35262  txpconn  35264  ptpconn  35265  indispconn  35266  connpconn  35267  cvxpconn  35274  cnllysconn  35277  cvmcov2  35307  cvmopnlem  35310  cvmliftmolem1  35313  cvmliftlem14  35329  cvmliftlem15  35330  cvmlift2lem13  35347  cvmlift3lem2  35352  cvmlift3lem9  35359  seglerflx  36145  seglemin  36146  btwnsegle  36150  hilbert1.1  36187  neibastop2lem  36393  weiunfrlem  36497  weiunso  36499  bj-finsumval0  37318  relowlssretop  37396  wl-2sb6d  37591  tan2h  37651  poimirlem1  37660  poimirlem3  37662  poimirlem4  37663  poimirlem9  37668  poimirlem22  37681  poimirlem28  37687  heicant  37694  mblfinlem2  37697  itg2addnc  37713  ftc2nc  37741  dvasin  37743  sdclem1  37782  fdc  37784  istotbnd3  37810  sstotbnd  37814  prdstotbnd  37833  prdsbnd2  37834  cntotbnd  37835  rngoisocnv  38020  lsmsat  39046  islfld  39100  ps-2  39516  lplnexllnN  39602  4atlem9  39641  4atlem10a  39642  lnatexN  39817  2lnat  39822  pmapjat1  39891  lhpj1  40060  lhpm0atN  40067  4atexlemex2  40109  4atex  40114  4atex2-0aOLDN  40116  4atex2-0cOLDN  40118  lautcnvle  40127  lautj  40131  lautm  40132  idltrn  40188  cdleme01N  40259  cdleme0ex1N  40261  cdleme5  40278  cdleme9  40291  cdleme11c  40299  cdleme11g  40303  cdlemefrs29bpre0  40434  cdlemefrs29cpre1  40436  cdlemefrs32fva1  40439  cdleme32fva  40475  cdleme32fva1  40476  cdleme32fvaw  40477  cdleme32d  40482  cdleme32f  40484  cdleme35fnpq  40487  cdleme48d  40573  cdleme48gfv  40575  cdleme50ltrn  40595  trlord  40607  cdlemg4b1  40647  cdlemg4b2  40648  cdlemg13a  40689  cdlemg17a  40699  cdlemg17f  40704  erng1lem  41025  erngdvlem3  41028  erngdvlem4  41029  erng1r  41033  erngdvlem3-rN  41036  erngdvlem4-rN  41037  dva0g  41065  dialss  41084  dia0  41090  dia1N  41091  diaglbN  41093  diameetN  41094  diainN  41095  diaintclN  41096  dia1dim  41099  dia2dimlem5  41106  dia2dimlem7  41108  dia2dimlem9  41110  dia2dimlem10  41111  dia2dimlem12  41113  dia2dimlem13  41114  dvhopvadd  41131  dvhvaddass  41135  dvhopvsca  41140  tendolinv  41143  tendorinv  41144  dvhlveclem  41146  dvh0g  41149  dvheveccl  41150  dvhopN  41154  docaclN  41162  diaocN  41163  djajN  41175  dib0  41202  dib1dim  41203  dibglbN  41204  dibintclN  41205  dib1dim2  41206  diblss  41208  diblsmopel  41209  dicvaddcl  41228  dicvscacl  41229  diclspsn  41232  cdlemn4a  41237  cdlemn11c  41247  dihjustlem  41254  dihord1  41256  dihord2a  41257  dihord2b  41258  dihord2cN  41259  dihord11b  41260  dihord11c  41262  dihord2pre  41263  dihlsscpre  41272  dih1dimb  41278  dib2dim  41281  dih2dimb  41282  dih2dimbALTN  41283  dihvalcq2  41285  dihopelvalcpre  41286  dihord6apre  41294  dihord5b  41297  dihord5apre  41300  dih0  41318  dihmeetlem1N  41328  dihglblem5apreN  41329  dihglblem3N  41333  dihmeetlem2N  41337  dihglbcpreN  41338  dihmeetlem4preN  41344  dih1dimatlem0  41366  dih1dimatlem  41367  dihatlat  41372  dihatexv  41376  dihglb2  41380  dihmeet  41381  dihintcl  41382  dihmeet2  41384  doch2val2  41402  dochocss  41404  dihoml4c  41414  dochdmj1  41428  djhlj  41439  djhljjN  41440  djhjlj  41441  dihsumssj  41446  djhexmid  41449  djhlsmcl  41452  djhcvat42  41453  dihjatcclem4  41459  dihjat1lem  41466  dihsmsprn  41468  dihjat3  41470  dvh3dim2  41486  dvh3dim3N  41487  dochkr1OLDN  41517  lclkrlem2c  41547  lclkrlem2d  41548  mapdpglem23  41732  hdmap11lem2  41880  0prjspn  42660  mzpcompact2lem  42783  diophrw  42791  rexrabdioph  42826  eldioph4b  42843  pellexlem5  42865  pellfund14  42930  acongtr  43010  fnwe2lem3  43084  gicabl  43131  hbtlem2  43156  hbtlem4  43158  hbtlem5  43160  dgraalem  43177  aaitgo  43194  onexlimgt  43275  onexoegt  43276  oalim2cl  43321  cantnfresb  43356  onmcl  43363  tfsconcatfv  43373  tfsconcatrn  43374  ofoaid1  43390  ofoaid2  43391  ntrclsk13  44103  gneispb  44163  wessf1ornlem  45221  ltdiv23neg  45431  islptre  45658  limclner  45688  icccncfext  45924  stoweidlem1  46038  stoweidlem14  46051  stoweidlem24  46061  stoweidlem46  46083  stoweidlem57  46094  dirkercncflem2  46141  fourierdlem20  46164  fourierdlem41  46185  fourierdlem46  46189  fourierdlem48  46191  fourierdlem50  46193  fourierdlem62  46205  fourierdlem63  46206  fourierdlem64  46207  fourierdlem65  46208  fourierdlem76  46219  fourierdlem79  46222  fourierdlem103  46246  fourierdlem104  46247  etransclem47  46318  m1modmmod  47388  iccpartiun  47464  reupr  47552  sqrtpwpw2p  47568  fmtnoprmfac1lem  47594  fmtnoprmfac2lem1  47596  lighneallem4a  47638  requad2  47653  perfectALTV  47753  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  isuspgrim0lem  47923  isuspgrim0  47924  isuspgrimlem  47925  upgrimwlklem2  47928  upgrimwlklem3  47929  upgrimtrlslem1  47934  uhgrimisgrgriclem  47960  uhgrimisgrgric  47961  clnbgrgrimlem  47963  grimgrtri  47979  gpgedgvtx1  48092  gpgedg2ov  48096  gpgedg2iv  48097  gsumlsscl  48410  lincsumcl  48462  lincscmcl  48463  isldepslvec2  48516  elbigo2  48583  relogbdivb  48593  blennnt2  48620  dignn0ldlem  48633  itsclc0yqsollem2  48794  inlinecirc02p  48818  lubeldm2  48986  glbeldm2  48987  lubsscl  48990  glbsscl  48991  isclatd  49013  sectpropdlem  49067  invpropdlem  49069  isopropdlem  49071  uptrlem1  49241  fucofulem1  49341  fullthinc  49481