Theorem syl12anc 837

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 585	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  839  raaan  4459  raaanv  4460  raaan2  4463  copsex2dv  5442  soltmin  6093  xpdifid  6126  reuop  6251  f1dom3fv3dif  7216  f1prex  7232  cocan1  7239  fliftfun  7260  soisores  7275  soisoi  7276  isopolem  7293  f1oiso2  7300  weniso  7302  caovcld  7553  caovcomd  7556  onminex  7749  poxp2  8086  poxp3  8093  poseq  8101  tfrlem12  8321  omeulem1  8510  nnaordex2  8568  oaabs2  8578  omabs  8580  eldifsucnn  8593  naddcllem  8605  erov  8754  findcard2d  9094  frfi  9188  finsschain  9262  suplub2  9367  supgtoreq  9377  supisolem  9380  ordiso2  9423  ordtypelem7  9432  wemaplem2  9455  wemapsolem  9458  cantnflt  9584  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1  9601  wemapwe  9609  cnfcomlem  9611  cnfcom  9612  cnfcom3lem  9615  infxpenlem  9926  fseqenlem1  9937  dfac12lem2  10058  infpssrlem4  10219  enfin2i  10234  isf34lem7  10292  isf34lem6  10293  fin1a2lem7  10319  fin1a2lem10  10322  fin1a2lem11  10323  fin1a2lem13  10325  ttukeylem6  10427  ttukeylem7  10428  iundom2g  10453  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  fpwwe2lem11  10555  fpwwe2  10557  canthnumlem  10562  canthwelem  10564  canthp1lem2  10567  pwfseqlem4  10576  inar1  10689  intgru  10728  distrlem4pr  10940  conjmul  11863  lediv12a  12040  recp1lt1  12045  cju  12146  gtndiv  12597  zsupss  12878  uzsupss  12881  icc0  13337  iccssioo2  13363  fzrev3  13535  ico01fl0  13769  fldiv  13810  modabs  13854  modltm1p1mod  13876  modifeq2int  13886  modsumfzodifsn  13897  seqcaopr  13992  seqf1olem1  13994  seqof2  14013  crreczi  14181  seqcoll  14417  seqcoll2  14418  hashtpg  14438  swrdccat3b  14693  01sqrexlem2  15196  resqrex  15203  abs1m  15289  isercoll  15621  zsum  15671  fsum2dlem  15723  fsumcom2  15727  fprod2dlem  15936  fprodcom2  15940  efsub  16058  bitsinv2  16403  sqgcd  16522  expgcd  16523  qredeu  16618  isprm7  16669  pcpremul  16805  pceulem  16807  pczpre  16809  pcdiv  16814  pcqmul  16815  pcqdiv  16819  pcexp  16821  pcdvdsb  16831  pcneg  16836  pcdvdstr  16838  pcgcd1  16839  pc2dvds  16841  pcz  16843  pcaddlem  16850  pcadd  16851  qexpz  16863  expnprm  16864  infpnlem2  16873  ramub2  16976  ramub1lem1  16988  setsstruct2  17135  f1ocpbllem  17479  f1ovscpbl  17481  mreexexlem3d  17603  mreexexlem4d  17604  fthi  17878  ipodrsima  18498  chnind  18578  mgmpropd  18610  sgrppropd  18690  mndpropd  18718  grpsubpropd2  19013  f1ghm0to0  19211  ghmqusker  19253  symgfvne  19347  f1omvdmvd  19409  f1otrspeq  19413  pmtrdifwrdel  19451  pmtrdifwrdel2  19452  psgnunilem2  19461  psgnunilem3  19462  psgnvalii  19475  odf1  19528  lsmpropd  19643  ablnnncan  19788  gsummptshft  19902  dprdf1o  20000  pgpfac1lem3  20045  pgpfac1lem5  20047  pgpfaclem1  20049  ablfaclem2  20054  rngpropd  20146  srgbinomlem3  20200  ringpropd  20260  orngsqr  20834  ornglmullt  20837  orngrmullt  20838  lmodprop2d  20910  lsspropd  21004  lmhmpropd  21060  lbspropd  21086  lbsextlem3  21150  iporthcom  21625  obslbs  21720  assapropd  21861  psrass1  21952  psrass23l  21955  psrass23  21957  mplsubrg  21993  mplmon  22023  mplmonmul  22024  mplcoe1  22025  mplbas2  22030  mplind  22058  evlslem2  22067  mpfind  22103  gsumply1subr  22207  psrplusgpropd  22209  ply1scln0  22266  evls1addd  22346  evls1muld  22347  evls1vsca  22348  asclply1subcl  22349  scmataddcl  22491  scmatsubcl  22492  scmatmulcl  22493  smatvscl  22499  scmatrhmcl  22503  mat1scmat  22514  smadiadetglem2  22647  cramerimplem2  22659  cramerimplem3  22660  cramerimp  22661  1pmatscmul  22677  mat2pmatf1  22704  pm2mp  22800  chmatcl  22803  chmatval  22804  chmaidscmat  22823  chfacfisf  22829  cayhamlem1  22841  cpmidgsumm2pm  22844  cpmidpmat  22848  cpmadugsumfi  22852  cpmadumatpoly  22858  cayhamlem3  22862  pptbas  22983  elcls  23048  neiint  23079  neiptopnei  23107  restbas  23133  neitr  23155  iscnp4  23238  cnconst2  23258  cnpdis  23268  cnt0  23321  cnhaus  23329  cmpcovf  23366  hauscmplem  23381  conncompid  23406  2ndci  23423  2ndc1stc  23426  1stcrest  23428  2ndcctbss  23430  2ndcomap  23433  2ndcsep  23434  dis2ndc  23435  restlly  23458  islly2  23459  lly1stc  23471  dislly  23472  finlocfin  23495  dissnlocfin  23504  locfindis  23505  llycmpkgen2  23525  ptbasfi  23556  neitx  23582  ptpjopn  23587  ptcnplem  23596  upxp  23598  txlly  23611  txtube  23615  tx1stc  23625  txkgen  23627  xkococnlem  23634  kqreglem1  23716  kqreglem2  23717  kqnrmlem1  23718  kqnrmlem2  23719  hmeoimaf1o  23745  reghmph  23768  nrmhmph  23769  ordthmeolem  23776  trfil2  23862  fmfnfm  23933  hauspwpwf1  23962  fclsfnflim  24002  cnextf  24041  cnextcn  24042  tmdgsum2  24071  symgtgp  24081  subgntr  24082  opnsubg  24083  ghmcnp  24090  qustgpopn  24095  tsmsf1o  24120  tsmsxplem1  24128  tsmsxplem2  24129  tsmsxp  24130  ustexsym  24191  restutop  24212  imasdsf1olem  24348  blssexps  24401  blssex  24402  ssblex  24403  imasf1oxms  24464  blcld  24480  stdbdmopn  24493  met1stc  24496  met2ndci  24497  prdsxmslem2  24504  metcnp3  24515  cfilucfil  24534  ngptgp  24611  tgioo  24771  tgqioo  24775  zdis  24792  iccpnfhmeo  24922  xrhmeo  24923  cnheibor  24932  elpi1i  25023  cmetcusp  25331  bncssbn  25351  pjthlem2  25415  ivthlem2  25429  ovolicc1  25493  ovolicc2lem3  25496  ovolicc2lem4  25497  volsup  25533  volivth  25584  vitalilem3  25587  mbflimsup  25643  mbfi1fseqlem1  25692  mbfi1fseqlem3  25694  mbfi1fseqlem5  25696  limcnlp  25855  limcflf  25858  limciun  25871  dvmptfsum  25952  dvcnvlem  25953  dvcvx  25997  facth1  26142  elply2  26171  plypf1  26187  coeeq  26202  aaliou3lem8  26322  ulm2  26363  mtestbdd  26383  reeff1o  26425  logbgcd1irr  26771  dcubic2  26821  quart  26838  xrlimcnp  26945  amgm  26968  harmonicbnd4  26988  perfect  27208  dchrptlem1  27241  bposlem2  27262  lgsfcl2  27280  lgsdir  27309  lgsdi  27311  lgsne0  27312  2lgslem1a1  27366  2sqmod  27413  dchrvmasumlem2  27475  chpdifbndlem2  27531  pntpbnd1  27563  pntpbnd2  27564  padicabv  27607  ltsres  27640  nolesgn2o  27649  nogesgn1o  27651  nodense  27670  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd2lem1  27693  noinfres  27700  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd2lem1  27708  noetalem1  27719  nocvxmin  27761  noeta2  27767  oncutlt  28270  eucliddivs  28382  readdscl  28505  tgcgrxfr  28600  idmot  28619  legid  28669  btwnleg  28670  leg0  28674  tghilberti1  28719  mirreu3  28736  colperpex  28815  lnopp2hpgb  28845  axcgrrflx  28997  axsegconlem1  29000  axcontlem2  29048  axcontlem12  29058  eengtrkg  29069  wwlksnredwwlkn  29978  0wlkon  30205  0trlon  30209  upgr3v3e3cycl  30265  frgrogt3nreg  30482  nvpi  30753  nmlno0lem  30879  fh1  31704  fh2  31705  nmlnop0iALT  32081  nmopun  32100  branmfn  32191  opsqrlem1  32226  opsqrlem6  32231  mdslmd1lem1  32411  csmdsymi  32420  atom1d  32439  chirredlem2  32477  cdj1i  32519  cdj3i  32527  fcnvgreu  32760  suppovss  32769  xrofsup  32855  nn0difffzod  32892  sgnmul  32923  pwrssmgc  33075  gsummpt2d  33125  gsumhashmul  33143  odpmco  33162  cycpmco2lem6  33207  cycpmco2  33209  cyc3evpm  33226  cycpmconjslem2  33231  fxpsubg  33249  fxpsdrg  33251  archirngz  33265  archiabllem2a  33270  elrgspnlem4  33321  rloc0g  33347  rloc1r  33348  domnpropd  33353  sdrgdvcl  33375  sdrginvcl  33376  lindssn  33453  lindfpropd  33457  ssdifidllem  33531  ssmxidllem  33548  rsprprmprmidlb  33598  rprmirredb  33607  1arithufd  33623  ply1asclunit  33649  ply1dg1rt  33655  ply1dg3rt0irred  33659  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  psrmonmul  33709  esplyind  33734  esplyindfv  33735  lsssra  33747  lindsun  33785  dimkerim  33787  fedgmullem2  33790  fldextrspunlem1  33835  fldextrspunfld  33836  irngss  33847  irngnzply1  33851  algextdeglem2  33878  algextdeglem4  33880  constrext2chnlem  33910  metideq  34053  metider  34054  pstmfval  34056  lmxrge0  34112  qqhval2  34142  qqhf  34146  qqhghm  34148  qqhrhm  34149  esumpcvgval  34238  esum2dlem  34252  esum2d  34253  sigainb  34296  insiga  34297  ddemeas  34396  imambfm  34422  dya2icoseg  34437  dya2iocnrect  34441  eulerpartlemgvv  34536  probun  34579  ballotlemfc0  34653  ballotlemfcc  34654  breprexplemc  34792  erdszelem8  35396  erdszelem9  35397  erdsze2lem2  35402  cnpconn  35428  txpconn  35430  ptpconn  35431  indispconn  35432  connpconn  35433  cvxpconn  35440  cnllysconn  35443  cvmcov2  35473  cvmopnlem  35476  cvmliftmolem1  35479  cvmliftlem14  35495  cvmliftlem15  35496  cvmlift2lem13  35513  cvmlift3lem2  35518  cvmlift3lem9  35525  seglerflx  36310  seglemin  36311  btwnsegle  36315  hilbert1.1  36352  neibastop2lem  36558  weiunfrlem  36662  weiunso  36664  mh-inf3f1  36739  bj-finsumval0  37615  relowlssretop  37693  wl-2sb6d  37897  tan2h  37947  poimirlem1  37956  poimirlem3  37958  poimirlem4  37959  poimirlem9  37964  poimirlem22  37977  poimirlem28  37983  heicant  37990  mblfinlem2  37993  itg2addnc  38009  ftc2nc  38037  dvasin  38039  sdclem1  38078  fdc  38080  istotbnd3  38106  sstotbnd  38110  prdstotbnd  38129  prdsbnd2  38130  cntotbnd  38131  rngoisocnv  38316  lsmsat  39468  islfld  39522  ps-2  39938  lplnexllnN  40024  4atlem9  40063  4atlem10a  40064  lnatexN  40239  2lnat  40244  pmapjat1  40313  lhpj1  40482  lhpm0atN  40489  4atexlemex2  40531  4atex  40536  4atex2-0aOLDN  40538  4atex2-0cOLDN  40540  lautcnvle  40549  lautj  40553  lautm  40554  idltrn  40610  cdleme01N  40681  cdleme0ex1N  40683  cdleme5  40700  cdleme9  40713  cdleme11c  40721  cdleme11g  40725  cdlemefrs29bpre0  40856  cdlemefrs29cpre1  40858  cdlemefrs32fva1  40861  cdleme32fva  40897  cdleme32fva1  40898  cdleme32fvaw  40899  cdleme32d  40904  cdleme32f  40906  cdleme35fnpq  40909  cdleme48d  40995  cdleme48gfv  40997  cdleme50ltrn  41017  trlord  41029  cdlemg4b1  41069  cdlemg4b2  41070  cdlemg13a  41111  cdlemg17a  41121  cdlemg17f  41126  erng1lem  41447  erngdvlem3  41450  erngdvlem4  41451  erng1r  41455  erngdvlem3-rN  41458  erngdvlem4-rN  41459  dva0g  41487  dialss  41506  dia0  41512  dia1N  41513  diaglbN  41515  diameetN  41516  diainN  41517  diaintclN  41518  dia1dim  41521  dia2dimlem5  41528  dia2dimlem7  41530  dia2dimlem9  41532  dia2dimlem10  41533  dia2dimlem12  41535  dia2dimlem13  41536  dvhopvadd  41553  dvhvaddass  41557  dvhopvsca  41562  tendolinv  41565  tendorinv  41566  dvhlveclem  41568  dvh0g  41571  dvheveccl  41572  dvhopN  41576  docaclN  41584  diaocN  41585  djajN  41597  dib0  41624  dib1dim  41625  dibglbN  41626  dibintclN  41627  dib1dim2  41628  diblss  41630  diblsmopel  41631  dicvaddcl  41650  dicvscacl  41651  diclspsn  41654  cdlemn4a  41659  cdlemn11c  41669  dihjustlem  41676  dihord1  41678  dihord2a  41679  dihord2b  41680  dihord2cN  41681  dihord11b  41682  dihord11c  41684  dihord2pre  41685  dihlsscpre  41694  dih1dimb  41700  dib2dim  41703  dih2dimb  41704  dih2dimbALTN  41705  dihvalcq2  41707  dihopelvalcpre  41708  dihord6apre  41716  dihord5b  41719  dihord5apre  41722  dih0  41740  dihmeetlem1N  41750  dihglblem5apreN  41751  dihglblem3N  41755  dihmeetlem2N  41759  dihglbcpreN  41760  dihmeetlem4preN  41766  dih1dimatlem0  41788  dih1dimatlem  41789  dihatlat  41794  dihatexv  41798  dihglb2  41802  dihmeet  41803  dihintcl  41804  dihmeet2  41806  doch2val2  41824  dochocss  41826  dihoml4c  41836  dochdmj1  41850  djhlj  41861  djhljjN  41862  djhjlj  41863  dihsumssj  41868  djhexmid  41871  djhlsmcl  41874  djhcvat42  41875  dihjatcclem4  41881  dihjat1lem  41888  dihsmsprn  41890  dihjat3  41892  dvh3dim2  41908  dvh3dim3N  41909  dochkr1OLDN  41939  lclkrlem2c  41969  lclkrlem2d  41970  mapdpglem23  42154  hdmap11lem2  42302  0prjspn  43075  mzpcompact2lem  43197  diophrw  43205  rexrabdioph  43240  eldioph4b  43257  pellexlem5  43279  pellfund14  43344  acongtr  43424  fnwe2lem3  43498  gicabl  43545  hbtlem2  43570  hbtlem4  43572  hbtlem5  43574  dgraalem  43591  aaitgo  43608  onexlimgt  43689  onexoegt  43690  oalim2cl  43735  cantnfresb  43770  onmcl  43777  tfsconcatfv  43787  tfsconcatrn  43788  ofoaid1  43804  ofoaid2  43805  ntrclsk13  44516  gneispb  44576  wessf1ornlem  45633  ltdiv23neg  45841  islptre  46067  limclner  46097  icccncfext  46333  stoweidlem1  46447  stoweidlem14  46460  stoweidlem24  46470  stoweidlem46  46492  stoweidlem57  46503  dirkercncflem2  46550  fourierdlem20  46573  fourierdlem41  46594  fourierdlem46  46598  fourierdlem48  46600  fourierdlem50  46602  fourierdlem62  46614  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem76  46628  fourierdlem79  46631  fourierdlem103  46655  fourierdlem104  46656  etransclem47  46727  m1modmmod  47824  iccpartiun  47906  reupr  47994  sqrtpwpw2p  48013  fmtnoprmfac1lem  48039  fmtnoprmfac2lem1  48041  lighneallem4a  48083  requad2  48111  perfectALTV  48211  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  isuspgrim0lem  48381  isuspgrim0  48382  isuspgrimlem  48383  upgrimwlklem2  48386  upgrimwlklem3  48387  upgrimtrlslem1  48392  uhgrimisgrgriclem  48418  uhgrimisgrgric  48419  clnbgrgrimlem  48421  grimgrtri  48437  gpgedgvtx1  48550  gpgedg2ov  48554  gpgedg2iv  48555  gsumlsscl  48868  lincsumcl  48919  lincscmcl  48920  isldepslvec2  48973  elbigo2  49040  relogbdivb  49050  blennnt2  49077  dignn0ldlem  49090  itsclc0yqsollem2  49251  inlinecirc02p  49275  lubeldm2  49443  glbeldm2  49444  lubsscl  49447  glbsscl  49448  isclatd  49470  sectpropdlem  49523  invpropdlem  49525  isopropdlem  49527  uptrlem1  49697  fucofulem1  49797  fullthinc  49937