Theorem syl12anc 849

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 520	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	1, 4, 5	syl2anc 595	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl22anc  851  raaan  4475  raaanv  4476  raaan2  4479  copsex2dv  5467  soltmin  6126  xpdifid  6156  xpdifcnvepel  6157  reuop  6283  f1dom3fv3dif  7256  f1prex  7272  cocan1  7279  fliftfun  7300  soisores  7315  soisoi  7316  isopolem  7333  f1oiso2  7340  weniso  7342  caovcld  7593  caovcomd  7596  onminex  7789  poxp2  8127  poxp3  8134  poseq  8142  tfrlem12  8364  omeulem1  8555  nnaordex2  8613  oaabs2  8623  omabs  8625  eldifsucnn  8638  naddcllem  8650  erov  8800  findcard2d  9139  frfi  9233  finsschain  9304  suplub2  9409  supgtoreq  9419  supisolem  9422  ordiso2  9465  ordtypelem7  9474  wemaplem2  9497  wemapsolem  9500  cantnflt  9629  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1  9646  wemapwe  9654  cnfcomlem  9656  cnfcom  9657  cnfcom3lem  9660  infxpenlem  9985  fseqenlem1  9996  dfac12lem2  10116  infpssrlem4  10278  enfin2i  10293  isf34lem7  10351  isf34lem6  10352  fin1a2lem7  10378  fin1a2lem10  10381  fin1a2lem11  10382  fin1a2lem13  10384  ttukeylem6  10486  ttukeylem7  10487  iundom2g  10512  fpwwe2lem5  10608  fpwwe2lem6  10609  fpwwe2lem8  10611  fpwwe2lem11  10614  fpwwe2  10616  canthnumlem  10621  canthwelem  10623  canthp1lem2  10626  pwfseqlem4  10635  inar1  10748  intgru  10787  distrlem4pr  10999  conjmul  11920  lediv12a  12096  recp1lt1  12101  cju  12202  gtndiv  12661  zsupss  12949  uzsupss  12952  icc0  13408  iccssioo2  13434  fzrev3  13606  ico01fl0  13840  fldiv  13881  modabs  13925  modltm1p1mod  13947  modifeq2int  13957  modsumfzodifsn  13968  seqcaopr  14063  seqf1olem1  14065  seqof2  14084  crreczi  14252  seqcoll  14489  seqcoll2  14490  hashtpg  14510  swrdccat3b  14765  sgnmul  15132  01sqrexlem2  15282  resqrex  15289  abs1m  15375  isercoll  15707  zsum  15757  fsum2dlem  15809  fsumcom2  15813  fprod2dlem  16022  fprodcom2  16026  efsub  16144  bitsinv2  16489  sqgcd  16608  expgcd  16609  qredeu  16704  isprm7  16755  pcpremul  16891  pceulem  16893  pczpre  16895  pcdiv  16900  pcqmul  16901  pcqdiv  16905  pcexp  16907  pcdvdsb  16917  pcneg  16922  pcdvdstr  16924  pcgcd1  16925  pc2dvds  16927  pcz  16929  pcaddlem  16936  pcadd  16937  qexpz  16949  expnprm  16950  infpnlem2  16959  ramub2  17062  ramub1lem1  17074  setsstruct2  17222  f1ocpbllem  17566  f1ovscpbl  17568  mreexexlem3d  17690  mreexexlem4d  17691  fthi  17965  ipodrsima  18585  chnind  18665  mgmpropd  18697  sgrppropd  18777  mndpropd  18805  grpsubpropd2  19100  f1ghm0to0  19303  ghmqusker  19345  symgfvne  19439  f1omvdmvd  19501  f1otrspeq  19505  pmtrdifwrdel  19543  pmtrdifwrdel2  19544  psgnunilem2  19553  psgnunilem3  19554  psgnvalii  19567  odf1  19620  lsmpropd  19735  ablnnncan  19880  gsummptshft  19994  dprdf1o  20092  pgpfac1lem3  20137  pgpfac1lem5  20139  pgpfaclem1  20141  ablfaclem2  20146  rngpropd  20240  srgbinomlem3  20298  ringpropd  20359  orngsqr  20935  ornglmullt  20938  orngrmullt  20939  lmodprop2d  21011  lsspropd  21104  lmhmpropd  21160  lbspropd  21186  lbsextlem3  21250  unichnlidl  21328  ssdifidllem  21441  iporthcom  21742  obslbs  21837  assapropd  21978  psrass1  22070  psrass23l  22073  psrass23  22075  mplsubrg  22111  mplmon  22143  mplmonmul  22144  mplcoe1  22145  mplbas2  22150  mplind  22178  evlslem2  22187  mpfind  22223  gsumply1subr  22350  psrplusgpropd  22352  ply1scln0  22409  evls1addd  22488  evls1muld  22489  evls1vsca  22490  asclply1subcl  22491  scmataddcl  22630  scmatsubcl  22631  scmatmulcl  22632  smatvscl  22638  scmatrhmcl  22642  mat1scmat  22653  smadiadetglem2  22786  cramerimplem2  22798  cramerimplem3  22799  cramerimp  22800  1pmatscmul  22816  mat2pmatf1  22843  pm2mp  22939  chmatcl  22942  chmatval  22943  chmaidscmat  22962  chfacfisf  22968  cayhamlem1  22980  cpmidgsumm2pm  22983  cpmidpmat  22987  cpmadugsumfi  22991  cpmadumatpoly  22997  cayhamlem3  23001  pptbas  23122  elcls  23187  neiint  23218  neiptopnei  23246  restbas  23272  neitr  23294  iscnp4  23377  cnconst2  23397  cnpdis  23407  cnt0  23460  cnhaus  23468  cmpcovf  23505  hauscmplem  23520  conncompid  23545  2ndci  23562  2ndc1stc  23565  1stcrest  23567  2ndcctbss  23569  2ndcomap  23572  2ndcsep  23573  dis2ndc  23574  restlly  23597  islly2  23598  lly1stc  23610  dislly  23611  finlocfin  23634  dissnlocfin  23643  locfindis  23644  llycmpkgen2  23664  ptbasfi  23695  neitx  23721  ptpjopn  23726  ptcnplem  23735  upxp  23737  txlly  23750  txtube  23754  tx1stc  23764  txkgen  23766  xkococnlem  23773  kqreglem1  23855  kqreglem2  23856  kqnrmlem1  23857  kqnrmlem2  23858  hmeoimaf1o  23884  reghmph  23907  nrmhmph  23908  ordthmeolem  23915  trfil2  24001  fmfnfm  24072  hauspwpwf1  24101  fclsfnflim  24141  cnextf  24180  cnextcn  24181  tmdgsum2  24210  symgtgp  24220  subgntr  24221  opnsubg  24222  ghmcnp  24229  qustgpopn  24234  tsmsf1o  24259  tsmsxplem1  24267  tsmsxplem2  24268  tsmsxp  24269  ustexsym  24330  restutop  24351  imasdsf1olem  24487  blssexps  24540  blssex  24541  ssblex  24542  imasf1oxms  24603  blcld  24619  stdbdmopn  24632  met1stc  24635  met2ndci  24636  prdsxmslem2  24643  metcnp3  24654  cfilucfil  24673  ngptgp  24750  tgioo  24910  tgqioo  24914  zdis  24931  iccpnfhmeo  25061  xrhmeo  25062  cnheibor  25071  elpi1i  25162  cmetcusp  25470  bncssbn  25490  pjthlem2  25554  ivthlem2  25568  ovolicc1  25632  ovolicc2lem3  25635  ovolicc2lem4  25636  volsup  25672  volivth  25723  vitalilem3  25726  mbflimsup  25782  mbfi1fseqlem1  25831  mbfi1fseqlem3  25833  mbfi1fseqlem5  25835  limcnlp  25994  limcflf  25997  limciun  26010  dvmptfsum  26091  dvcnvlem  26092  dvcvx  26136  facth1  26281  elply2  26310  plypf1  26326  coeeq  26341  aaliou3lem8  26463  ulm2  26502  mtestbdd  26522  reeff1o  26564  logbgcd1irr  26913  dcubic2  26963  quart  26980  xrlimcnp  27087  amgm  27109  harmonicbnd4  27129  perfect  27349  dchrptlem1  27382  bposlem2  27403  lgsfcl2  27421  lgsdir  27450  lgsdi  27452  lgsne0  27453  2lgslem1a1  27507  2sqmod  27554  dchrvmasumlem2  27616  chpdifbndlem2  27672  pntpbnd1  27704  pntpbnd2  27705  padicabv  27748  ltsres  27780  nolesgn2o  27789  nogesgn1o  27791  nodense  27810  nosupbnd1lem3  27828  nosupbnd1lem5  27830  nosupbnd2lem1  27833  noinfres  27840  noinfbnd1lem3  27843  noinfbnd1lem5  27845  noinfbnd2lem1  27848  noetalem1  27859  nocvxmin  27902  noeta2  27908  oncutlt  28411  eucliddivs  28523  readdscl  28646  tgcgrxfr  28741  idmot  28760  legid  28810  btwnleg  28811  leg0  28815  tghilberti1  28860  mirreu3  28881  colperpex  28960  lnopp2hpgb  28990  axcgrrflx  29169  axsegconlem1  29172  axcontlem2  29220  axcontlem12  29230  eengtrkg  29241  wwlksnredwwlkn  30149  0wlkon  30376  0trlon  30380  upgr3v3e3cycl  30436  frgrogt3nreg  30653  nvpi  30924  nmlno0lem  31050  fh1  31875  fh2  31876  nmlnop0iALT  32252  nmopun  32271  branmfn  32362  opsqrlem1  32397  opsqrlem6  32402  mdslmd1lem1  32582  csmdsymi  32591  atom1d  32610  chirredlem2  32648  cdj1i  32690  cdj3i  32698  fcnvgreu  32925  suppovss  32934  xrofsup  33020  nn0difffzod  33057  pwrssmgc  33228  gsummpt2d  33277  gsumhashmul  33295  odpmco  33314  cycpmco2lem6  33359  cycpmco2  33361  cyc3evpm  33378  cycpmconjslem2  33383  fxpsubg  33401  fxpsdrg  33403  archirngz  33417  archiabllem2a  33422  elrgspnlem4  33473  rloc0g  33500  rloc1r  33501  domnpropd  33508  sdrgdvcl  33530  sdrginvcl  33531  lindssn  33602  lindfpropd  33606  ssmxidllem  33668  drnglring  33694  dflring2  33695  rsprprmprmidlb  33725  rprmirredb  33734  1arithufd  33750  ply1asclunit  33776  ply1dg1rt  33782  ply1dg3rt0irred  33786  ply1degltel  33796  ply1degleel  33797  ply1degltlss  33798  psrmonmul  33852  esplyind  33877  esplyindfv  33878  lsssra  33890  lindsun  33927  dimkerim  33929  fedgmullem2  33932  fldextrspunlem1  33977  fldextrspunfld  33978  irngss  33989  irngnzply1  33993  algextdeglem2  34020  algextdeglem4  34022  constrext2chnlem  34052  metideq  34195  metider  34196  pstmfval  34198  lmxrge0  34254  qqhval2  34284  qqhf  34288  qqhghm  34290  qqhrhm  34291  esumpcvgval  34380  esum2dlem  34394  esum2d  34395  sigainb  34438  insiga  34439  ddemeas  34538  imambfm  34564  dya2icoseg  34579  dya2iocnrect  34583  eulerpartlemgvv  34678  probun  34721  ballotlemfc0  34795  ballotlemfcc  34796  breprexplemc  34931  erdszelem8  35556  erdszelem9  35557  erdsze2lem2  35562  cnpconn  35588  txpconn  35590  ptpconn  35591  indispconn  35592  connpconn  35593  cvxpconn  35600  cnllysconn  35603  cvmcov2  35633  cvmopnlem  35636  cvmliftmolem1  35639  cvmliftlem14  35655  cvmliftlem15  35656  cvmlift2lem13  35673  cvmlift3lem2  35678  cvmlift3lem9  35685  seglerflx  36470  seglemin  36471  btwnsegle  36475  hilbert1.1  36512  neibastop2lem  36728  weiunfrlem  36832  weiunso  36834  mh-inf3f1  36909  bj-finsumval0  37784  qdiff  37826  relowlssretop  37864  wl-2sb6d  38068  tan2h  38118  poimirlem1  38127  poimirlem3  38129  poimirlem4  38130  poimirlem9  38135  poimirlem22  38148  poimirlem28  38154  heicant  38161  mblfinlem2  38164  itg2addnc  38180  ftc2nc  38208  dvasin  38210  sdclem1  38249  fdc  38251  istotbnd3  38277  sstotbnd  38281  prdstotbnd  38300  prdsbnd2  38301  cntotbnd  38302  rngoisocnv  38487  lsmsat  39639  islfld  39693  ps-2  40109  lplnexllnN  40195  4atlem9  40234  4atlem10a  40235  lnatexN  40410  2lnat  40415  pmapjat1  40484  lhpj1  40653  lhpm0atN  40660  4atexlemex2  40702  4atex  40707  4atex2-0aOLDN  40709  4atex2-0cOLDN  40711  lautcnvle  40720  lautj  40724  lautm  40725  idltrn  40781  cdleme01N  40852  cdleme0ex1N  40854  cdleme5  40871  cdleme9  40884  cdleme11c  40892  cdleme11g  40896  cdlemefrs29bpre0  41027  cdlemefrs29cpre1  41029  cdlemefrs32fva1  41032  cdleme32fva  41068  cdleme32fva1  41069  cdleme32fvaw  41070  cdleme32d  41075  cdleme32f  41077  cdleme35fnpq  41080  cdleme48d  41166  cdleme48gfv  41168  cdleme50ltrn  41188  trlord  41200  cdlemg4b1  41240  cdlemg4b2  41241  cdlemg13a  41282  cdlemg17a  41292  cdlemg17f  41297  erng1lem  41618  erngdvlem3  41621  erngdvlem4  41622  erng1r  41626  erngdvlem3-rN  41629  erngdvlem4-rN  41630  dva0g  41658  dialss  41677  dia0  41683  dia1N  41684  diaglbN  41686  diameetN  41687  diainN  41688  diaintclN  41689  dia1dim  41692  dia2dimlem5  41699  dia2dimlem7  41701  dia2dimlem9  41703  dia2dimlem10  41704  dia2dimlem12  41706  dia2dimlem13  41707  dvhopvadd  41724  dvhvaddass  41728  dvhopvsca  41733  tendolinv  41736  tendorinv  41737  dvhlveclem  41739  dvh0g  41742  dvheveccl  41743  dvhopN  41747  docaclN  41755  diaocN  41756  djajN  41768  dib0  41795  dib1dim  41796  dibglbN  41797  dibintclN  41798  dib1dim2  41799  diblss  41801  diblsmopel  41802  dicvaddcl  41821  dicvscacl  41822  diclspsn  41825  cdlemn4a  41830  cdlemn11c  41840  dihjustlem  41847  dihord1  41849  dihord2a  41850  dihord2b  41851  dihord2cN  41852  dihord11b  41853  dihord11c  41855  dihord2pre  41856  dihlsscpre  41865  dih1dimb  41871  dib2dim  41874  dih2dimb  41875  dih2dimbALTN  41876  dihvalcq2  41878  dihopelvalcpre  41879  dihord6apre  41887  dihord5b  41890  dihord5apre  41893  dih0  41911  dihmeetlem1N  41921  dihglblem5apreN  41922  dihglblem3N  41926  dihmeetlem2N  41930  dihglbcpreN  41931  dihmeetlem4preN  41937  dih1dimatlem0  41959  dih1dimatlem  41960  dihatlat  41965  dihatexv  41969  dihglb2  41973  dihmeet  41974  dihintcl  41975  dihmeet2  41977  doch2val2  41995  dochocss  41997  dihoml4c  42007  dochdmj1  42021  djhlj  42032  djhljjN  42033  djhjlj  42034  dihsumssj  42039  djhexmid  42042  djhlsmcl  42045  djhcvat42  42046  dihjatcclem4  42052  dihjat1lem  42059  dihsmsprn  42061  dihjat3  42063  dvh3dim2  42079  dvh3dim3N  42080  dochkr1OLDN  42110  lclkrlem2c  42140  lclkrlem2d  42141  mapdpglem23  42325  hdmap11lem2  42473  0prjspn  43217  mzpcompact2lem  43339  diophrw  43347  rexrabdioph  43378  eldioph4b  43395  pellexlem5  43417  pellfund14  43482  acongtr  43562  fnwe2lem3  43636  gicabl  43683  hbtlem2  43708  hbtlem4  43710  hbtlem5  43712  dgraalem  43729  aaitgo  43746  onexlimgt  43827  onexoegt  43828  oalim2cl  43873  cantnfresb  43908  onmcl  43915  tfsconcatfv  43925  tfsconcatrn  43926  ofoaid1  43942  ofoaid2  43943  ntrclsk13  44654  gneispb  44714  wessf1ornlem  45762  ltdiv23neg  45968  islptre  46194  limclner  46224  icccncfext  46460  stoweidlem1  46574  stoweidlem14  46587  stoweidlem24  46597  stoweidlem46  46619  stoweidlem57  46630  dirkercncflem2  46677  fourierdlem20  46700  fourierdlem41  46721  fourierdlem46  46725  fourierdlem48  46727  fourierdlem50  46729  fourierdlem62  46741  fourierdlem63  46742  fourierdlem64  46743  fourierdlem65  46744  fourierdlem76  46755  fourierdlem79  46758  fourierdlem103  46782  fourierdlem104  46783  etransclem47  46854  m1modmmod  47957  iccpartiun  48039  reupr  48127  sqrtpwpw2p  48146  fmtnoprmfac1lem  48172  fmtnoprmfac2lem1  48174  lighneallem4a  48216  requad2  48244  perfectALTV  48344  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  isuspgrim0lem  48514  isuspgrim0  48515  isuspgrimlem  48516  upgrimwlklem2  48519  upgrimwlklem3  48520  upgrimtrlslem1  48525  uhgrimisgrgriclem  48551  uhgrimisgrgric  48552  clnbgrgrimlem  48554  grimgrtri  48570  gpgedgvtx1  48683  gpgedg2ov  48687  gpgedg2iv  48688  gsumlsscl  49012  lincsumcl  49063  lincscmcl  49064  isldepslvec2  49117  elbigo2  49184  relogbdivb  49194  blennnt2  49221  dignn0ldlem  49234  itsclc0yqsollem2  49395  inlinecirc02p  49419  lubeldm2  49586  glbeldm2  49587  lubsscl  49590  glbsscl  49591  isclatd  49613  sectpropdlem  49666  invpropdlem  49668  isopropdlem  49670  uptrlem1  49840  fucofulem1  49940  fullthinc  50080