Theorem syl12anc 847

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  syl22anc  849  raaan  4469  raaanv  4470  raaan2  4473  copsex2dv  5460  soltmin  6118  xpdifid  6148  reuop  6274  f1dom3fv3dif  7246  f1prex  7262  cocan1  7269  fliftfun  7290  soisores  7305  soisoi  7306  isopolem  7323  f1oiso2  7330  weniso  7332  caovcld  7583  caovcomd  7586  onminex  7779  poxp2  8116  poxp3  8123  poseq  8131  tfrlem12  8353  omeulem1  8544  nnaordex2  8602  oaabs2  8612  omabs  8614  eldifsucnn  8627  naddcllem  8639  erov  8789  findcard2d  9128  frfi  9222  finsschain  9295  suplub2  9400  supgtoreq  9410  supisolem  9413  ordiso2  9456  ordtypelem7  9465  wemaplem2  9488  wemapsolem  9491  cantnflt  9620  cantnfp1lem3  9628  cantnflem1b  9634  cantnflem1  9637  wemapwe  9645  cnfcomlem  9647  cnfcom  9648  cnfcom3lem  9651  infxpenlem  9962  fseqenlem1  9973  dfac12lem2  10094  infpssrlem4  10256  enfin2i  10271  isf34lem7  10329  isf34lem6  10330  fin1a2lem7  10356  fin1a2lem10  10359  fin1a2lem11  10360  fin1a2lem13  10362  ttukeylem6  10464  ttukeylem7  10465  iundom2g  10490  fpwwe2lem5  10586  fpwwe2lem6  10587  fpwwe2lem8  10589  fpwwe2lem11  10592  fpwwe2  10594  canthnumlem  10599  canthwelem  10601  canthp1lem2  10604  pwfseqlem4  10613  inar1  10726  intgru  10765  distrlem4pr  10977  conjmul  11901  lediv12a  12078  recp1lt1  12083  cju  12184  gtndiv  12643  zsupss  12931  uzsupss  12934  icc0  13390  iccssioo2  13416  fzrev3  13588  ico01fl0  13822  fldiv  13863  modabs  13907  modltm1p1mod  13929  modifeq2int  13939  modsumfzodifsn  13950  seqcaopr  14045  seqf1olem1  14047  seqof2  14066  crreczi  14234  seqcoll  14470  seqcoll2  14471  hashtpg  14491  swrdccat3b  14746  sgnmul  15110  01sqrexlem2  15260  resqrex  15267  abs1m  15353  isercoll  15685  zsum  15735  fsum2dlem  15787  fsumcom2  15791  fprod2dlem  16000  fprodcom2  16004  efsub  16122  bitsinv2  16467  sqgcd  16586  expgcd  16587  qredeu  16682  isprm7  16733  pcpremul  16869  pceulem  16871  pczpre  16873  pcdiv  16878  pcqmul  16879  pcqdiv  16883  pcexp  16885  pcdvdsb  16895  pcneg  16900  pcdvdstr  16902  pcgcd1  16903  pc2dvds  16905  pcz  16907  pcaddlem  16914  pcadd  16915  qexpz  16927  expnprm  16928  infpnlem2  16937  ramub2  17040  ramub1lem1  17052  setsstruct2  17200  f1ocpbllem  17544  f1ovscpbl  17546  mreexexlem3d  17668  mreexexlem4d  17669  fthi  17943  ipodrsima  18563  chnind  18643  mgmpropd  18675  sgrppropd  18755  mndpropd  18783  grpsubpropd2  19078  f1ghm0to0  19275  ghmqusker  19317  symgfvne  19411  f1omvdmvd  19473  f1otrspeq  19477  pmtrdifwrdel  19515  pmtrdifwrdel2  19516  psgnunilem2  19525  psgnunilem3  19526  psgnvalii  19539  odf1  19592  lsmpropd  19707  ablnnncan  19852  gsummptshft  19966  dprdf1o  20064  pgpfac1lem3  20109  pgpfac1lem5  20111  pgpfaclem1  20113  ablfaclem2  20118  rngpropd  20210  srgbinomlem3  20264  ringpropd  20324  orngsqr  20902  ornglmullt  20905  orngrmullt  20906  lmodprop2d  20978  lsspropd  21071  lmhmpropd  21127  lbspropd  21153  lbsextlem3  21217  iporthcom  21674  obslbs  21769  assapropd  21910  psrass1  22002  psrass23l  22005  psrass23  22007  mplsubrg  22043  mplmon  22075  mplmonmul  22076  mplcoe1  22077  mplbas2  22082  mplind  22110  evlslem2  22119  mpfind  22155  gsumply1subr  22282  psrplusgpropd  22284  ply1scln0  22341  evls1addd  22421  evls1muld  22422  evls1vsca  22423  asclply1subcl  22424  scmataddcl  22563  scmatsubcl  22564  scmatmulcl  22565  smatvscl  22571  scmatrhmcl  22575  mat1scmat  22586  smadiadetglem2  22719  cramerimplem2  22731  cramerimplem3  22732  cramerimp  22733  1pmatscmul  22749  mat2pmatf1  22776  pm2mp  22872  chmatcl  22875  chmatval  22876  chmaidscmat  22895  chfacfisf  22901  cayhamlem1  22913  cpmidgsumm2pm  22916  cpmidpmat  22920  cpmadugsumfi  22924  cpmadumatpoly  22930  cayhamlem3  22934  pptbas  23055  elcls  23120  neiint  23151  neiptopnei  23179  restbas  23205  neitr  23227  iscnp4  23310  cnconst2  23330  cnpdis  23340  cnt0  23393  cnhaus  23401  cmpcovf  23438  hauscmplem  23453  conncompid  23478  2ndci  23495  2ndc1stc  23498  1stcrest  23500  2ndcctbss  23502  2ndcomap  23505  2ndcsep  23506  dis2ndc  23507  restlly  23530  islly2  23531  lly1stc  23543  dislly  23544  finlocfin  23567  dissnlocfin  23576  locfindis  23577  llycmpkgen2  23597  ptbasfi  23628  neitx  23654  ptpjopn  23659  ptcnplem  23668  upxp  23670  txlly  23683  txtube  23687  tx1stc  23697  txkgen  23699  xkococnlem  23706  kqreglem1  23788  kqreglem2  23789  kqnrmlem1  23790  kqnrmlem2  23791  hmeoimaf1o  23817  reghmph  23840  nrmhmph  23841  ordthmeolem  23848  trfil2  23934  fmfnfm  24005  hauspwpwf1  24034  fclsfnflim  24074  cnextf  24113  cnextcn  24114  tmdgsum2  24143  symgtgp  24153  subgntr  24154  opnsubg  24155  ghmcnp  24162  qustgpopn  24167  tsmsf1o  24192  tsmsxplem1  24200  tsmsxplem2  24201  tsmsxp  24202  ustexsym  24263  restutop  24284  imasdsf1olem  24420  blssexps  24473  blssex  24474  ssblex  24475  imasf1oxms  24536  blcld  24552  stdbdmopn  24565  met1stc  24568  met2ndci  24569  prdsxmslem2  24576  metcnp3  24587  cfilucfil  24606  ngptgp  24683  tgioo  24843  tgqioo  24847  zdis  24864  iccpnfhmeo  24994  xrhmeo  24995  cnheibor  25004  elpi1i  25095  cmetcusp  25403  bncssbn  25423  pjthlem2  25487  ivthlem2  25501  ovolicc1  25565  ovolicc2lem3  25568  ovolicc2lem4  25569  volsup  25605  volivth  25656  vitalilem3  25659  mbflimsup  25715  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem5  25768  limcnlp  25927  limcflf  25930  limciun  25943  dvmptfsum  26024  dvcnvlem  26025  dvcvx  26069  facth1  26214  elply2  26243  plypf1  26259  coeeq  26274  aaliou3lem8  26396  ulm2  26435  mtestbdd  26455  reeff1o  26497  logbgcd1irr  26846  dcubic2  26896  quart  26913  xrlimcnp  27020  amgm  27042  harmonicbnd4  27062  perfect  27282  dchrptlem1  27315  bposlem2  27336  lgsfcl2  27354  lgsdir  27383  lgsdi  27385  lgsne0  27386  2lgslem1a1  27440  2sqmod  27487  dchrvmasumlem2  27549  chpdifbndlem2  27605  pntpbnd1  27637  pntpbnd2  27638  padicabv  27681  ltsres  27713  nolesgn2o  27722  nogesgn1o  27724  nodense  27743  nosupbnd1lem3  27761  nosupbnd1lem5  27763  nosupbnd2lem1  27766  noinfres  27773  noinfbnd1lem3  27776  noinfbnd1lem5  27778  noinfbnd2lem1  27781  noetalem1  27792  nocvxmin  27835  noeta2  27841  oncutlt  28344  eucliddivs  28456  readdscl  28579  tgcgrxfr  28674  idmot  28693  legid  28743  btwnleg  28744  leg0  28748  tghilberti1  28793  mirreu3  28810  colperpex  28889  lnopp2hpgb  28919  axcgrrflx  29071  axsegconlem1  29074  axcontlem2  29122  axcontlem12  29132  eengtrkg  29143  wwlksnredwwlkn  30051  0wlkon  30278  0trlon  30282  upgr3v3e3cycl  30338  frgrogt3nreg  30555  nvpi  30826  nmlno0lem  30952  fh1  31777  fh2  31778  nmlnop0iALT  32154  nmopun  32173  branmfn  32264  opsqrlem1  32299  opsqrlem6  32304  mdslmd1lem1  32484  csmdsymi  32493  atom1d  32512  chirredlem2  32550  cdj1i  32592  cdj3i  32600  fcnvgreu  32834  suppovss  32843  xrofsup  32929  nn0difffzod  32966  pwrssmgc  33138  gsummpt2d  33189  gsumhashmul  33207  odpmco  33226  cycpmco2lem6  33271  cycpmco2  33273  cyc3evpm  33290  cycpmconjslem2  33295  fxpsubg  33313  fxpsdrg  33315  archirngz  33329  archiabllem2a  33334  elrgspnlem4  33386  rloc0g  33413  rloc1r  33414  domnpropd  33421  sdrgdvcl  33446  sdrginvcl  33447  lindssn  33524  lindfpropd  33528  ssdifidllem  33603  ssmxidllem  33621  drnglring  33648  dflring2  33649  rsprprmprmidlb  33679  rprmirredb  33688  1arithufd  33704  ply1asclunit  33730  ply1dg1rt  33736  ply1dg3rt0irred  33740  ply1degltel  33750  ply1degleel  33751  ply1degltlss  33752  psrmonmul  33807  esplyind  33832  esplyindfv  33833  lsssra  33845  lindsun  33882  dimkerim  33884  fedgmullem2  33887  fldextrspunlem1  33932  fldextrspunfld  33933  irngss  33944  irngnzply1  33948  algextdeglem2  33975  algextdeglem4  33977  constrext2chnlem  34007  metideq  34150  metider  34151  pstmfval  34153  lmxrge0  34209  qqhval2  34239  qqhf  34243  qqhghm  34245  qqhrhm  34246  esumpcvgval  34335  esum2dlem  34349  esum2d  34350  sigainb  34393  insiga  34394  ddemeas  34493  imambfm  34519  dya2icoseg  34534  dya2iocnrect  34538  eulerpartlemgvv  34633  probun  34676  ballotlemfc0  34750  ballotlemfcc  34751  breprexplemc  34886  erdszelem8  35508  erdszelem9  35509  erdsze2lem2  35514  cnpconn  35540  txpconn  35542  ptpconn  35543  indispconn  35544  connpconn  35545  cvxpconn  35552  cnllysconn  35555  cvmcov2  35585  cvmopnlem  35588  cvmliftmolem1  35591  cvmliftlem14  35607  cvmliftlem15  35608  cvmlift2lem13  35625  cvmlift3lem2  35630  cvmlift3lem9  35637  seglerflx  36422  seglemin  36423  btwnsegle  36427  hilbert1.1  36464  neibastop2lem  36680  weiunfrlem  36784  weiunso  36786  mh-inf3f1  36861  bj-finsumval0  37737  qdiff  37779  relowlssretop  37817  wl-2sb6d  38021  tan2h  38071  poimirlem1  38080  poimirlem3  38082  poimirlem4  38083  poimirlem9  38088  poimirlem22  38101  poimirlem28  38107  heicant  38114  mblfinlem2  38117  itg2addnc  38133  ftc2nc  38161  dvasin  38163  sdclem1  38202  fdc  38204  istotbnd3  38230  sstotbnd  38234  prdstotbnd  38253  prdsbnd2  38254  cntotbnd  38255  rngoisocnv  38440  lsmsat  39592  islfld  39646  ps-2  40062  lplnexllnN  40148  4atlem9  40187  4atlem10a  40188  lnatexN  40363  2lnat  40368  pmapjat1  40437  lhpj1  40606  lhpm0atN  40613  4atexlemex2  40655  4atex  40660  4atex2-0aOLDN  40662  4atex2-0cOLDN  40664  lautcnvle  40673  lautj  40677  lautm  40678  idltrn  40734  cdleme01N  40805  cdleme0ex1N  40807  cdleme5  40824  cdleme9  40837  cdleme11c  40845  cdleme11g  40849  cdlemefrs29bpre0  40980  cdlemefrs29cpre1  40982  cdlemefrs32fva1  40985  cdleme32fva  41021  cdleme32fva1  41022  cdleme32fvaw  41023  cdleme32d  41028  cdleme32f  41030  cdleme35fnpq  41033  cdleme48d  41119  cdleme48gfv  41121  cdleme50ltrn  41141  trlord  41153  cdlemg4b1  41193  cdlemg4b2  41194  cdlemg13a  41235  cdlemg17a  41245  cdlemg17f  41250  erng1lem  41571  erngdvlem3  41574  erngdvlem4  41575  erng1r  41579  erngdvlem3-rN  41582  erngdvlem4-rN  41583  dva0g  41611  dialss  41630  dia0  41636  dia1N  41637  diaglbN  41639  diameetN  41640  diainN  41641  diaintclN  41642  dia1dim  41645  dia2dimlem5  41652  dia2dimlem7  41654  dia2dimlem9  41656  dia2dimlem10  41657  dia2dimlem12  41659  dia2dimlem13  41660  dvhopvadd  41677  dvhvaddass  41681  dvhopvsca  41686  tendolinv  41689  tendorinv  41690  dvhlveclem  41692  dvh0g  41695  dvheveccl  41696  dvhopN  41700  docaclN  41708  diaocN  41709  djajN  41721  dib0  41748  dib1dim  41749  dibglbN  41750  dibintclN  41751  dib1dim2  41752  diblss  41754  diblsmopel  41755  dicvaddcl  41774  dicvscacl  41775  diclspsn  41778  cdlemn4a  41783  cdlemn11c  41793  dihjustlem  41800  dihord1  41802  dihord2a  41803  dihord2b  41804  dihord2cN  41805  dihord11b  41806  dihord11c  41808  dihord2pre  41809  dihlsscpre  41818  dih1dimb  41824  dib2dim  41827  dih2dimb  41828  dih2dimbALTN  41829  dihvalcq2  41831  dihopelvalcpre  41832  dihord6apre  41840  dihord5b  41843  dihord5apre  41846  dih0  41864  dihmeetlem1N  41874  dihglblem5apreN  41875  dihglblem3N  41879  dihmeetlem2N  41883  dihglbcpreN  41884  dihmeetlem4preN  41890  dih1dimatlem0  41912  dih1dimatlem  41913  dihatlat  41918  dihatexv  41922  dihglb2  41926  dihmeet  41927  dihintcl  41928  dihmeet2  41930  doch2val2  41948  dochocss  41950  dihoml4c  41960  dochdmj1  41974  djhlj  41985  djhljjN  41986  djhjlj  41987  dihsumssj  41992  djhexmid  41995  djhlsmcl  41998  djhcvat42  41999  dihjatcclem4  42005  dihjat1lem  42012  dihsmsprn  42014  dihjat3  42016  dvh3dim2  42032  dvh3dim3N  42033  dochkr1OLDN  42063  lclkrlem2c  42093  lclkrlem2d  42094  mapdpglem23  42278  hdmap11lem2  42426  0prjspn  43170  mzpcompact2lem  43292  diophrw  43300  rexrabdioph  43331  eldioph4b  43348  pellexlem5  43370  pellfund14  43435  acongtr  43515  fnwe2lem3  43589  gicabl  43636  hbtlem2  43661  hbtlem4  43663  hbtlem5  43665  dgraalem  43682  aaitgo  43699  onexlimgt  43780  onexoegt  43781  oalim2cl  43826  cantnfresb  43861  onmcl  43868  tfsconcatfv  43878  tfsconcatrn  43879  ofoaid1  43895  ofoaid2  43896  ntrclsk13  44607  gneispb  44667  wessf1ornlem  45723  ltdiv23neg  45929  islptre  46155  limclner  46185  icccncfext  46421  stoweidlem1  46535  stoweidlem14  46548  stoweidlem24  46558  stoweidlem46  46580  stoweidlem57  46591  dirkercncflem2  46638  fourierdlem20  46661  fourierdlem41  46682  fourierdlem46  46686  fourierdlem48  46688  fourierdlem50  46690  fourierdlem62  46702  fourierdlem63  46703  fourierdlem64  46704  fourierdlem65  46705  fourierdlem76  46716  fourierdlem79  46719  fourierdlem103  46743  fourierdlem104  46744  etransclem47  46815  m1modmmod  47918  iccpartiun  48000  reupr  48088  sqrtpwpw2p  48107  fmtnoprmfac1lem  48133  fmtnoprmfac2lem1  48135  lighneallem4a  48177  requad2  48205  perfectALTV  48305  nnsum4primeseven  48382  nnsum4primesevenALTV  48383  isuspgrim0lem  48475  isuspgrim0  48476  isuspgrimlem  48477  upgrimwlklem2  48480  upgrimwlklem3  48481  upgrimtrlslem1  48486  uhgrimisgrgriclem  48512  uhgrimisgrgric  48513  clnbgrgrimlem  48515  grimgrtri  48531  gpgedgvtx1  48644  gpgedg2ov  48648  gpgedg2iv  48649  gsumlsscl  48962  lincsumcl  49013  lincscmcl  49014  isldepslvec2  49067  elbigo2  49134  relogbdivb  49144  blennnt2  49171  dignn0ldlem  49184  itsclc0yqsollem2  49345  inlinecirc02p  49369  lubeldm2  49537  glbeldm2  49538  lubsscl  49541  glbsscl  49542  isclatd  49564  sectpropdlem  49617  invpropdlem  49619  isopropdlem  49621  uptrlem1  49791  fucofulem1  49891  fullthinc  50031