Theorem syl12anc 850

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl22anc  852  raaan  4474  raaanv  4475  raaan2  4478  copsex2dv  5466  soltmin  6130  xpdifid  6159  xpdifcnvepel  6160  reuop  6295  f1dom3fv3dif  7270  f1prex  7290  cocan1  7297  fliftfun  7318  soisores  7333  soisoi  7334  isopolem  7351  f1oiso2  7358  weniso  7362  caovcld  7612  caovcomd  7615  onminex  7814  poxp2  8153  poxp3  8160  poseq  8168  tfrlem12  8390  omeulem1  8583  nnaordex2  8641  oaabs2  8651  omabs  8653  eldifsucnn  8666  naddcllem  8678  erov  8828  findcard2d  9175  frfi  9269  finsschain  9341  suplub2  9446  supgtoreq  9456  supisolem  9459  ordiso2  9502  ordtypelem7  9511  wemaplem2  9534  wemapsolem  9537  cantnflt  9666  cantnfp1lem3  9674  cantnflem1b  9680  cantnflem1  9683  wemapwe  9691  cnfcomlem  9693  cnfcom  9694  cnfcom3lem  9697  infxpenlem  10085  fseqenlem1  10096  dfac12lem2  10216  infpssrlem4  10377  enfin2i  10392  isf34lem7  10450  isf34lem6  10451  fin1a2lem7  10477  fin1a2lem10  10480  fin1a2lem11  10481  fin1a2lem13  10483  ttukeylem6  10585  ttukeylem7  10586  iundom2g  10617  fpwwe2lem5  10713  fpwwe2lem6  10714  fpwwe2lem8  10716  fpwwe2lem11  10719  fpwwe2  10721  canthnumlem  10726  canthwelem  10728  canthp1lem2  10731  pwfseqlem4  10740  inar1  10853  intgru  10892  distrlem4pr  11104  conjmul  12027  lediv12a  12203  recp1lt1  12208  cju  12309  gtndiv  12769  zsupss  13057  uzsupss  13060  icc0  13517  iccssioo2  13543  fzrev3  13717  ico01fl0  13952  fldiv  13993  modabs  14037  modltm1p1mod  14059  modifeq2int  14069  modsumfzodifsn  14080  seqcaopr  14175  seqf1olem1  14177  seqof2  14196  crreczi  14365  seqcoll  14602  seqcoll2  14603  hashtpg  14623  swrdccat3b  14882  sgnmul  15253  01sqrexlem2  15403  resqrex  15410  abs1m  15496  isercoll  15828  zsum  15877  fsum2dlem  15929  fsumcom2  15933  fprod2dlem  16140  fprodcom2  16144  efsub  16261  bitsinv2  16606  sqgcd  16729  expgcd  16730  qredeu  16826  isprm7  16877  pcpremul  17014  pceulem  17016  pczpre  17018  pcdiv  17023  pcqmul  17024  pcqdiv  17028  pcexp  17030  pcdvdsb  17040  pcneg  17045  pcdvdstr  17047  pcgcd1  17048  pc2dvds  17050  pcz  17052  pcaddlem  17059  pcadd  17060  qexpz  17072  expnprm  17073  infpnlem2  17082  ramub2  17185  ramub1lem1  17197  setsstruct2  17345  f1ocpbllem  17689  f1ovscpbl  17691  mreexexlem3d  17813  mreexexlem4d  17814  fthi  18088  ipodrsima  18708  chnind  18788  mgmpropd  18822  sgrppropd  18913  mndpropd  18944  grpsubpropd2  19249  f1ghm0to0  19452  ghmqusker  19494  symgfvne  19588  f1omvdmvd  19650  f1otrspeq  19654  pmtrdifwrdel  19692  pmtrdifwrdel2  19693  psgnunilem2  19702  psgnunilem3  19703  psgnvalii  19716  odf1  19769  lsmpropd  19884  ablnnncan  20029  gsummptshft  20143  dprdf1o  20241  pgpfac1lem3  20286  pgpfac1lem5  20288  pgpfaclem1  20290  ablfaclem2  20295  rngpropd  20389  srgbinomlem3  20447  ringpropd  20512  orngsqr  21116  ornglmullt  21119  orngrmullt  21120  lmodprop2d  21192  lsspropd  21285  lmhmpropd  21341  lbspropd  21367  lbsextlem3  21431  unichnlidl  21509  ssdifidllem  21633  iporthcom  21934  obslbs  22029  assapropd  22172  psrass1  22264  psrass23l  22267  psrass23  22269  mplsubrg  22305  mplmon  22337  mplmonmul  22338  mplcoe1  22339  mplbas2  22344  mplind  22372  evlslem2  22381  mpfind  22417  gsumply1subr  22544  psrplusgpropd  22546  ply1scln0  22603  evls1addd  22682  evls1muld  22683  evls1vsca  22684  asclply1subcl  22685  scmataddcl  22824  scmatsubcl  22825  scmatmulcl  22826  smatvscl  22832  scmatrhmcl  22836  mat1scmat  22847  smadiadetglem2  22980  cramerimplem2  22995  cramerimplem3  22996  cramerimp  22997  1pmatscmul  23013  mat2pmatf1  23040  pm2mp  23136  chmatcl  23139  chmatval  23140  chmaidscmat  23159  chfacfisf  23165  cayhamlem1  23177  cpmidgsumm2pm  23180  cpmidpmat  23184  cpmadugsumfi  23188  cpmadumatpoly  23194  cayhamlem3  23198  pptbas  23319  elcls  23384  neiint  23415  neiptopnei  23443  restbas  23469  neitr  23491  iscnp4  23574  cnconst2  23594  cnpdis  23604  cnt0  23657  cnhaus  23665  cmpcovf  23702  hauscmplem  23717  conncompid  23742  2ndci  23759  2ndc1stc  23762  1stcrest  23764  2ndcctbss  23767  2ndcomap  23770  2ndcsep  23771  dis2ndc  23772  restlly  23795  islly2  23796  lly1stc  23808  dislly  23809  finlocfin  23832  dissnlocfin  23841  locfindis  23842  llycmpkgen2  23862  ptbasfi  23893  neitx  23919  ptpjopn  23924  ptcnplem  23933  upxp  23935  txlly  23948  txtube  23952  tx1stc  23962  txkgen  23964  xkococnlem  23971  kqreglem1  24053  kqreglem2  24054  kqnrmlem1  24055  kqnrmlem2  24056  hmeoimaf1o  24082  reghmph  24105  nrmhmph  24106  ordthmeolem  24113  trfil2  24199  fmfnfm  24270  hauspwpwf1  24299  fclsfnflim  24339  cnextf  24378  cnextcn  24379  tmdgsum2  24408  symgtgp  24418  subgntr  24419  opnsubg  24420  ghmcnp  24427  qustgpopn  24432  tsmsf1o  24457  tsmsxplem1  24465  tsmsxplem2  24466  tsmsxp  24467  ustexsym  24528  restutop  24549  imasdsf1olem  24685  blssexps  24738  blssex  24739  ssblex  24740  imasf1oxms  24801  blcld  24817  stdbdmopn  24830  met1stc  24833  met2ndci  24834  prdsxmslem2  24841  metcnp3  24852  cfilucfil  24871  ngptgp  24948  tgioo  25108  tgqioo  25112  zdis  25129  iccpnfhmeo  25259  xrhmeo  25260  cnheibor  25269  elpi1i  25360  cmetcusp  25668  bncssbn  25688  pjthlem2  25752  ivthlem2  25766  ovolicc1  25830  ovolicc2lem3  25833  ovolicc2lem4  25834  volsup  25870  volivth  25921  vitalilem3  25924  mbflimsup  25980  mbfi1fseqlem1  26029  mbfi1fseqlem3  26031  mbfi1fseqlem5  26033  limcnlp  26191  limcflf  26194  limciun  26207  dvmptfsum  26288  dvcnvlem  26289  dvcvx  26333  facth1  26478  elply2  26507  plypf1  26524  coeeq  26539  aaliou3lem8  26665  ulm2  26705  mtestbdd  26725  reeff1o  26767  logbgcd1irr  27115  dcubic2  27165  quart  27182  xrlimcnp  27289  amgm  27311  harmonicbnd4  27331  perfect  27551  dchrptlem1  27584  bposlem2  27605  lgsfcl2  27623  lgsdir  27652  lgsdi  27654  lgsne0  27655  2lgslem1a1  27709  2sqmod  27756  dchrvmasumlem2  27818  chpdifbndlem2  27874  pntpbnd1  27906  pntpbnd2  27907  padicabv  27950  ltsres  28012  nolesgn2o  28021  nogesgn1o  28023  nodense  28042  nosupbnd1lem3  28060  nosupbnd1lem5  28062  nosupbnd2lem1  28065  noinfres  28072  noinfbnd1lem3  28075  noinfbnd1lem5  28077  noinfbnd2lem1  28080  noetalem1  28091  nocvxmin  28134  noeta2  28140  oncutlt  28643  eucliddivs  28755  readdscl  28878  tgcgrxfr  28974  idmot  28993  legid  29043  btwnleg  29044  leg0  29048  tghilberti1  29098  mirreu3  29119  colperpex  29202  lnopp2hpgb  29234  dfprlng2  29418  axcgrrflx  29485  axsegconlem1  29488  axcontlem2  29536  axcontlem12  29546  eengtrkg  29557  wwlksnredwwlkn  30477  0wlkon  30704  0trlon  30708  upgr3v3e3cycl  30774  frgrogt3nreg  30991  nvpi  31262  nmlno0lem  31388  fh1  32213  fh2  32214  nmlnop0iALT  32590  nmopun  32609  branmfn  32700  opsqrlem1  32735  opsqrlem6  32740  mdslmd1lem1  32920  csmdsymi  32929  atom1d  32948  chirredlem2  32986  cdj1i  33028  cdj3i  33036  fcnvgreu  33259  suppovss  33267  xrofsup  33352  nn0difffzod  33389  pwrssmgc  33554  gsummpt2d  33603  gsumhashmul  33621  odpmco  33640  cycpmco2lem6  33685  cycpmco2  33687  cyc3evpm  33704  cycpmconjslem2  33709  fxpsubg  33727  fxpsdrg  33729  archirngz  33743  archiabllem2a  33748  elrgspnlem4  33799  rloc0g  33826  rloc1r  33827  domnpropd  33834  sdrgdvcl  33854  sdrginvcl  33855  lindssn  33926  lindfpropd  33930  ssmxidllem  33991  drnglring  34017  dflring2  34018  rsprprmprmidlb  34048  rprmirredb  34057  1arithufd  34073  ply1asclunit  34099  ply1dg1rt  34105  ply1dg3rt0irred  34109  ply1degltel  34119  ply1degleel  34120  ply1degltlss  34121  psrmonmul  34175  esplyind  34200  esplyindfv  34201  lsssra  34213  lindsun  34250  dimkerim  34252  fedgmullem2  34255  fldextrspunlem1  34300  fldextrspunfld  34301  irngss  34312  irngnzply1  34316  algextdeglem2  34343  algextdeglem4  34345  constrext2chnlem  34375  metideq  34518  metider  34519  pstmfval  34521  lmxrge0  34577  qqhval2  34607  qqhf  34611  qqhghm  34613  qqhrhm  34614  esumpcvgval  34703  esum2dlem  34717  esum2d  34718  sigainb  34762  insiga  34763  ddemeas  34862  imambfm  34887  dya2icoseg  34902  dya2iocnrect  34906  eulerpartlemgvv  35001  probun  35044  ballotlemfc0  35118  ballotlemfcc  35119  breprexplemc  35254  erdszelem8  35942  erdszelem9  35943  erdsze2lem2  35948  cnpconn  35974  txpconn  35976  ptpconn  35977  indispconn  35978  connpconn  35979  cvxpconn  35986  cnllysconn  35989  cvmcov2  36019  cvmopnlem  36022  cvmliftmolem1  36025  cvmliftlem14  36041  cvmliftlem15  36042  cvmlift2lem13  36059  cvmlift3lem2  36064  cvmlift3lem9  36071  seglerflx  36857  seglemin  36858  btwnsegle  36862  hilbert1.1  36899  neibastop2lem  37128  weiunfrlem  37232  weiunso  37234  mh-inf3f1  37309  bj-finsumval0  38186  qdiff  38228  relowlssretop  38266  wl-2sb6d  38470  tan2h  38515  poimirlem1  38519  poimirlem3  38521  poimirlem4  38522  poimirlem9  38527  poimirlem22  38540  poimirlem28  38546  heicant  38553  mblfinlem2  38556  itg2addnc  38572  ftc2nc  38600  dvasin  38602  sdclem1  38657  fdc  38659  istotbnd3  38685  sstotbnd  38689  prdstotbnd  38708  prdsbnd2  38709  cntotbnd  38710  rngoisocnv  38895  lsmsat  40045  islfld  40099  ps-2  40515  lplnexllnN  40601  4atlem9  40640  4atlem10a  40641  lnatexN  40816  2lnat  40821  pmapjat1  40890  lhpj1  41059  lhpm0atN  41066  4atexlemex2  41108  4atex  41113  4atex2-0aOLDN  41115  4atex2-0cOLDN  41117  lautcnvle  41126  lautj  41130  lautm  41131  idltrn  41187  cdleme01N  41258  cdleme0ex1N  41260  cdleme5  41277  cdleme9  41290  cdleme11c  41298  cdleme11g  41302  cdlemefrs29bpre0  41433  cdlemefrs29cpre1  41435  cdlemefrs32fva1  41438  cdleme32fva  41474  cdleme32fva1  41475  cdleme32fvaw  41476  cdleme32d  41481  cdleme32f  41483  cdleme35fnpq  41486  cdleme48d  41572  cdleme48gfv  41574  cdleme50ltrn  41594  trlord  41606  cdlemg4b1  41646  cdlemg4b2  41647  cdlemg13a  41688  cdlemg17a  41698  cdlemg17f  41703  erng1lem  42024  erngdvlem3  42027  erngdvlem4  42028  erng1r  42032  erngdvlem3-rN  42035  erngdvlem4-rN  42036  dva0g  42064  dialss  42083  dia0  42089  dia1N  42090  diaglbN  42092  diameetN  42093  diainN  42094  diaintclN  42095  dia1dim  42098  dia2dimlem5  42105  dia2dimlem7  42107  dia2dimlem9  42109  dia2dimlem10  42110  dia2dimlem12  42112  dia2dimlem13  42113  dvhopvadd  42130  dvhvaddass  42134  dvhopvsca  42139  tendolinv  42142  tendorinv  42143  dvhlveclem  42145  dvh0g  42148  dvheveccl  42149  dvhopN  42153  docaclN  42161  diaocN  42162  djajN  42174  dib0  42201  dib1dim  42202  dibglbN  42203  dibintclN  42204  dib1dim2  42205  diblss  42207  diblsmopel  42208  dicvaddcl  42227  dicvscacl  42228  diclspsn  42231  cdlemn4a  42236  cdlemn11c  42246  dihjustlem  42253  dihord1  42255  dihord2a  42256  dihord2b  42257  dihord2cN  42258  dihord11b  42259  dihord11c  42261  dihord2pre  42262  dihlsscpre  42271  dih1dimb  42277  dib2dim  42280  dih2dimb  42281  dih2dimbALTN  42282  dihvalcq2  42284  dihopelvalcpre  42285  dihord6apre  42293  dihord5b  42296  dihord5apre  42299  dih0  42317  dihmeetlem1N  42327  dihglblem5apreN  42328  dihglblem3N  42332  dihmeetlem2N  42336  dihglbcpreN  42337  dihmeetlem4preN  42343  dih1dimatlem0  42365  dih1dimatlem  42366  dihatlat  42371  dihatexv  42375  dihglb2  42379  dihmeet  42380  dihintcl  42381  dihmeet2  42383  doch2val2  42401  dochocss  42403  dihoml4c  42413  dochdmj1  42427  djhlj  42438  djhljjN  42439  djhjlj  42440  dihsumssj  42445  djhexmid  42448  djhlsmcl  42451  djhcvat42  42452  dihjatcclem4  42458  dihjat1lem  42465  dihsmsprn  42467  dihjat3  42469  dvh3dim2  42485  dvh3dim3N  42486  dochkr1OLDN  42516  lclkrlem2c  42546  lclkrlem2d  42547  mapdpglem23  42731  hdmap11lem2  42879  0prjspn  43644  mzpcompact2lem  43741  diophrw  43749  rexrabdioph  43780  eldioph4b  43797  pellexlem5  43819  pellfund14  43884  acongtr  43964  fnwe2lem3  44038  gicabl  44085  hbtlem2  44110  hbtlem4  44112  hbtlem5  44114  dgraalem  44131  aaitgo  44148  onexlimgt  44229  onexoegt  44230  oalim2cl  44275  cantnfresb  44310  onmcl  44317  tfsconcatfv  44327  tfsconcatrn  44328  ofoaid1  44344  ofoaid2  44345  ntrclsk13  45056  gneispb  45116  wessf1ornlem  46169  ltdiv23neg  46374  islptre  46600  limclner  46630  icccncfext  46866  stoweidlem1  46980  stoweidlem14  46993  stoweidlem24  47003  stoweidlem46  47025  stoweidlem57  47036  dirkercncflem2  47083  fourierdlem20  47106  fourierdlem41  47127  fourierdlem46  47131  fourierdlem48  47133  fourierdlem50  47135  fourierdlem62  47147  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem76  47161  fourierdlem79  47164  fourierdlem103  47188  fourierdlem104  47189  etransclem47  47260  m1modmmod  48403  iccpartiun  48485  reupr  48573  sqrtpwpw2p  48592  fmtnoprmfac1lem  48618  fmtnoprmfac2lem1  48620  lighneallem4a  48662  requad2  48690  perfectALTV  48790  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  isuspgrim0lem  48960  isuspgrim0  48961  isuspgrimlem  48962  upgrimwlklem2  48965  upgrimwlklem3  48966  upgrimtrlslem1  48971  uhgrimisgrgriclem  48997  uhgrimisgrgric  48998  clnbgrgrimlem  49000  grimgrtri  49016  gpgedgvtx1  49129  gpgedg2ov  49133  gpgedg2iv  49134  gsumlsscl  49461  lincsumcl  49512  lincscmcl  49513  isldepslvec2  49566  elbigo2  49633  relogbdivb  49643  blennnt2  49670  dignn0ldlem  49683  itsclc0yqsollem2  49844  inlinecirc02p  49868  lubeldm2  50033  glbeldm2  50034  lubsscl  50037  glbsscl  50038  isclatd  50060  sectpropdlem  50113  invpropdlem  50115  isopropdlem  50117  uptrlem1  50287  fucofulem1  50387  fullthinc  50527