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  4473  raaanv  4474  raaan2  4477  copsex2dv  5450  soltmin  6101  xpdifid  6134  reuop  6259  f1dom3fv3dif  7224  f1prex  7240  cocan1  7247  fliftfun  7268  soisores  7283  soisoi  7284  isopolem  7301  f1oiso2  7308  weniso  7310  caovcld  7561  caovcomd  7564  onminex  7757  poxp2  8095  poxp3  8102  poseq  8110  tfrlem12  8330  omeulem1  8519  nnaordex2  8577  oaabs2  8587  omabs  8589  eldifsucnn  8602  naddcllem  8614  erov  8763  findcard2d  9103  frfi  9197  finsschain  9271  suplub2  9376  supgtoreq  9386  supisolem  9389  ordiso2  9432  ordtypelem7  9441  wemaplem2  9464  wemapsolem  9467  cantnflt  9593  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  wemapwe  9618  cnfcomlem  9620  cnfcom  9621  cnfcom3lem  9624  infxpenlem  9935  fseqenlem1  9946  dfac12lem2  10067  infpssrlem4  10228  enfin2i  10243  isf34lem7  10301  isf34lem6  10302  fin1a2lem7  10328  fin1a2lem10  10331  fin1a2lem11  10332  fin1a2lem13  10334  ttukeylem6  10436  ttukeylem7  10437  iundom2g  10462  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  fpwwe2lem11  10564  fpwwe2  10566  canthnumlem  10571  canthwelem  10573  canthp1lem2  10576  pwfseqlem4  10585  inar1  10698  intgru  10737  distrlem4pr  10949  conjmul  11870  lediv12a  12047  recp1lt1  12052  cju  12153  gtndiv  12581  zsupss  12862  uzsupss  12865  icc0  13321  iccssioo2  13347  fzrev3  13518  ico01fl0  13751  fldiv  13792  modabs  13836  modltm1p1mod  13858  modifeq2int  13868  modsumfzodifsn  13879  seqcaopr  13974  seqf1olem1  13976  seqof2  13995  crreczi  14163  seqcoll  14399  seqcoll2  14400  hashtpg  14420  swrdccat3b  14675  01sqrexlem2  15178  resqrex  15185  abs1m  15271  isercoll  15603  zsum  15653  fsum2dlem  15705  fsumcom2  15709  fprod2dlem  15915  fprodcom2  15919  efsub  16037  bitsinv2  16382  sqgcd  16501  expgcd  16502  qredeu  16597  isprm7  16647  pcpremul  16783  pceulem  16785  pczpre  16787  pcdiv  16792  pcqmul  16793  pcqdiv  16797  pcexp  16799  pcdvdsb  16809  pcneg  16814  pcdvdstr  16816  pcgcd1  16817  pc2dvds  16819  pcz  16821  pcaddlem  16828  pcadd  16829  qexpz  16841  expnprm  16842  infpnlem2  16851  ramub2  16954  ramub1lem1  16966  setsstruct2  17113  f1ocpbllem  17457  f1ovscpbl  17459  mreexexlem3d  17581  mreexexlem4d  17582  fthi  17856  ipodrsima  18476  chnind  18556  mgmpropd  18588  sgrppropd  18668  mndpropd  18696  grpsubpropd2  18988  f1ghm0to0  19186  ghmqusker  19228  symgfvne  19322  f1omvdmvd  19384  f1otrspeq  19388  pmtrdifwrdel  19426  pmtrdifwrdel2  19427  psgnunilem2  19436  psgnunilem3  19437  psgnvalii  19450  odf1  19503  lsmpropd  19618  ablnnncan  19763  gsummptshft  19877  dprdf1o  19975  pgpfac1lem3  20020  pgpfac1lem5  20022  pgpfaclem1  20024  ablfaclem2  20029  rngpropd  20121  srgbinomlem3  20175  ringpropd  20235  orngsqr  20811  ornglmullt  20814  orngrmullt  20815  lmodprop2d  20887  lsspropd  20981  lmhmpropd  21037  lbspropd  21063  lbsextlem3  21127  iporthcom  21602  obslbs  21697  assapropd  21839  psrass1  21931  psrass23l  21934  psrass23  21936  mplsubrg  21972  mplmon  22002  mplmonmul  22003  mplcoe1  22004  mplbas2  22009  mplind  22037  evlslem2  22046  mpfind  22082  gsumply1subr  22186  psrplusgpropd  22188  ply1scln0  22246  evls1addd  22327  evls1muld  22328  evls1vsca  22329  asclply1subcl  22330  scmataddcl  22472  scmatsubcl  22473  scmatmulcl  22474  smatvscl  22480  scmatrhmcl  22484  mat1scmat  22495  smadiadetglem2  22628  cramerimplem2  22640  cramerimplem3  22641  cramerimp  22642  1pmatscmul  22658  mat2pmatf1  22685  pm2mp  22781  chmatcl  22784  chmatval  22785  chmaidscmat  22804  chfacfisf  22810  cayhamlem1  22822  cpmidgsumm2pm  22825  cpmidpmat  22829  cpmadugsumfi  22833  cpmadumatpoly  22839  cayhamlem3  22843  pptbas  22964  elcls  23029  neiint  23060  neiptopnei  23088  restbas  23114  neitr  23136  iscnp4  23219  cnconst2  23239  cnpdis  23249  cnt0  23302  cnhaus  23310  cmpcovf  23347  hauscmplem  23362  conncompid  23387  2ndci  23404  2ndc1stc  23407  1stcrest  23409  2ndcctbss  23411  2ndcomap  23414  2ndcsep  23415  dis2ndc  23416  restlly  23439  islly2  23440  lly1stc  23452  dislly  23453  finlocfin  23476  dissnlocfin  23485  locfindis  23486  llycmpkgen2  23506  ptbasfi  23537  neitx  23563  ptpjopn  23568  ptcnplem  23577  upxp  23579  txlly  23592  txtube  23596  tx1stc  23606  txkgen  23608  xkococnlem  23615  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  hmeoimaf1o  23726  reghmph  23749  nrmhmph  23750  ordthmeolem  23757  trfil2  23843  fmfnfm  23914  hauspwpwf1  23943  fclsfnflim  23983  cnextf  24022  cnextcn  24023  tmdgsum2  24052  symgtgp  24062  subgntr  24063  opnsubg  24064  ghmcnp  24071  qustgpopn  24076  tsmsf1o  24101  tsmsxplem1  24109  tsmsxplem2  24110  tsmsxp  24111  ustexsym  24172  restutop  24193  imasdsf1olem  24329  blssexps  24382  blssex  24383  ssblex  24384  imasf1oxms  24445  blcld  24461  stdbdmopn  24474  met1stc  24477  met2ndci  24478  prdsxmslem2  24485  metcnp3  24496  cfilucfil  24515  ngptgp  24592  tgioo  24752  tgqioo  24756  zdis  24773  iccpnfhmeo  24911  xrhmeo  24912  cnheibor  24922  elpi1i  25014  cmetcusp  25322  bncssbn  25342  pjthlem2  25406  ivthlem2  25421  ovolicc1  25485  ovolicc2lem3  25488  ovolicc2lem4  25489  volsup  25525  volivth  25576  vitalilem3  25579  mbflimsup  25635  mbfi1fseqlem1  25684  mbfi1fseqlem3  25686  mbfi1fseqlem5  25688  limcnlp  25847  limcflf  25850  limciun  25863  dvmptfsum  25947  dvcnvlem  25948  dvcvx  25993  facth1  26140  elply2  26169  plypf1  26185  coeeq  26200  aaliou3lem8  26321  ulm2  26362  mtestbdd  26382  reeff1o  26425  logbgcd1irr  26772  dcubic2  26822  quart  26839  xrlimcnp  26946  amgm  26969  harmonicbnd4  26989  perfect  27210  dchrptlem1  27243  bposlem2  27264  lgsfcl2  27282  lgsdir  27311  lgsdi  27313  lgsne0  27314  2lgslem1a1  27368  2sqmod  27415  dchrvmasumlem2  27477  chpdifbndlem2  27533  pntpbnd1  27565  pntpbnd2  27566  padicabv  27609  ltsres  27642  nolesgn2o  27651  nogesgn1o  27653  nodense  27672  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd2lem1  27695  noinfres  27702  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd2lem1  27710  noetalem1  27721  nocvxmin  27763  noeta2  27769  oncutlt  28272  eucliddivs  28384  readdscl  28507  tgcgrxfr  28602  idmot  28621  legid  28671  btwnleg  28672  leg0  28676  tghilberti1  28721  mirreu3  28738  colperpex  28817  lnopp2hpgb  28847  axcgrrflx  28999  axsegconlem1  29002  axcontlem2  29050  axcontlem12  29060  eengtrkg  29071  wwlksnredwwlkn  29980  0wlkon  30207  0trlon  30211  upgr3v3e3cycl  30267  frgrogt3nreg  30484  nvpi  30754  nmlno0lem  30880  fh1  31705  fh2  31706  nmlnop0iALT  32082  nmopun  32101  branmfn  32192  opsqrlem1  32227  opsqrlem6  32232  mdslmd1lem1  32412  csmdsymi  32421  atom1d  32440  chirredlem2  32478  cdj1i  32520  cdj3i  32528  fcnvgreu  32761  suppovss  32770  xrofsup  32857  nn0difffzod  32894  sgnmul  32926  pwrssmgc  33092  gsummpt2d  33142  gsumhashmul  33160  odpmco  33179  cycpmco2lem6  33224  cycpmco2  33226  cyc3evpm  33243  cycpmconjslem2  33248  fxpsubg  33266  fxpsdrg  33268  archirngz  33282  archiabllem2a  33287  elrgspnlem4  33338  rloc0g  33364  rloc1r  33365  domnpropd  33370  sdrgdvcl  33392  sdrginvcl  33393  lindssn  33470  lindfpropd  33474  ssdifidllem  33548  ssmxidllem  33565  rsprprmprmidlb  33615  rprmirredb  33624  1arithufd  33640  ply1asclunit  33666  ply1dg1rt  33672  ply1dg3rt0irred  33676  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  psrmonmul  33726  esplyind  33751  esplyindfv  33752  lsssra  33764  lindsun  33802  dimkerim  33804  fedgmullem2  33807  fldextrspunlem1  33852  fldextrspunfld  33853  irngss  33864  irngnzply1  33868  algextdeglem2  33895  algextdeglem4  33897  constrext2chnlem  33927  metideq  34070  metider  34071  pstmfval  34073  lmxrge0  34129  qqhval2  34159  qqhf  34163  qqhghm  34165  qqhrhm  34166  esumpcvgval  34255  esum2dlem  34269  esum2d  34270  sigainb  34313  insiga  34314  ddemeas  34413  imambfm  34439  dya2icoseg  34454  dya2iocnrect  34458  eulerpartlemgvv  34553  probun  34596  ballotlemfc0  34670  ballotlemfcc  34671  breprexplemc  34809  erdszelem8  35411  erdszelem9  35412  erdsze2lem2  35417  cnpconn  35443  txpconn  35445  ptpconn  35446  indispconn  35447  connpconn  35448  cvxpconn  35455  cnllysconn  35458  cvmcov2  35488  cvmopnlem  35491  cvmliftmolem1  35494  cvmliftlem14  35510  cvmliftlem15  35511  cvmlift2lem13  35528  cvmlift3lem2  35533  cvmlift3lem9  35540  seglerflx  36325  seglemin  36326  btwnsegle  36330  hilbert1.1  36367  neibastop2lem  36573  weiunfrlem  36677  weiunso  36679  bj-finsumval0  37537  relowlssretop  37615  wl-2sb6d  37810  tan2h  37860  poimirlem1  37869  poimirlem3  37871  poimirlem4  37872  poimirlem9  37877  poimirlem22  37890  poimirlem28  37896  heicant  37903  mblfinlem2  37906  itg2addnc  37922  ftc2nc  37950  dvasin  37952  sdclem1  37991  fdc  37993  istotbnd3  38019  sstotbnd  38023  prdstotbnd  38042  prdsbnd2  38043  cntotbnd  38044  rngoisocnv  38229  lsmsat  39381  islfld  39435  ps-2  39851  lplnexllnN  39937  4atlem9  39976  4atlem10a  39977  lnatexN  40152  2lnat  40157  pmapjat1  40226  lhpj1  40395  lhpm0atN  40402  4atexlemex2  40444  4atex  40449  4atex2-0aOLDN  40451  4atex2-0cOLDN  40453  lautcnvle  40462  lautj  40466  lautm  40467  idltrn  40523  cdleme01N  40594  cdleme0ex1N  40596  cdleme5  40613  cdleme9  40626  cdleme11c  40634  cdleme11g  40638  cdlemefrs29bpre0  40769  cdlemefrs29cpre1  40771  cdlemefrs32fva1  40774  cdleme32fva  40810  cdleme32fva1  40811  cdleme32fvaw  40812  cdleme32d  40817  cdleme32f  40819  cdleme35fnpq  40822  cdleme48d  40908  cdleme48gfv  40910  cdleme50ltrn  40930  trlord  40942  cdlemg4b1  40982  cdlemg4b2  40983  cdlemg13a  41024  cdlemg17a  41034  cdlemg17f  41039  erng1lem  41360  erngdvlem3  41363  erngdvlem4  41364  erng1r  41368  erngdvlem3-rN  41371  erngdvlem4-rN  41372  dva0g  41400  dialss  41419  dia0  41425  dia1N  41426  diaglbN  41428  diameetN  41429  diainN  41430  diaintclN  41431  dia1dim  41434  dia2dimlem5  41441  dia2dimlem7  41443  dia2dimlem9  41445  dia2dimlem10  41446  dia2dimlem12  41448  dia2dimlem13  41449  dvhopvadd  41466  dvhvaddass  41470  dvhopvsca  41475  tendolinv  41478  tendorinv  41479  dvhlveclem  41481  dvh0g  41484  dvheveccl  41485  dvhopN  41489  docaclN  41497  diaocN  41498  djajN  41510  dib0  41537  dib1dim  41538  dibglbN  41539  dibintclN  41540  dib1dim2  41541  diblss  41543  diblsmopel  41544  dicvaddcl  41563  dicvscacl  41564  diclspsn  41567  cdlemn4a  41572  cdlemn11c  41582  dihjustlem  41589  dihord1  41591  dihord2a  41592  dihord2b  41593  dihord2cN  41594  dihord11b  41595  dihord11c  41597  dihord2pre  41598  dihlsscpre  41607  dih1dimb  41613  dib2dim  41616  dih2dimb  41617  dih2dimbALTN  41618  dihvalcq2  41620  dihopelvalcpre  41621  dihord6apre  41629  dihord5b  41632  dihord5apre  41635  dih0  41653  dihmeetlem1N  41663  dihglblem5apreN  41664  dihglblem3N  41668  dihmeetlem2N  41672  dihglbcpreN  41673  dihmeetlem4preN  41679  dih1dimatlem0  41701  dih1dimatlem  41702  dihatlat  41707  dihatexv  41711  dihglb2  41715  dihmeet  41716  dihintcl  41717  dihmeet2  41719  doch2val2  41737  dochocss  41739  dihoml4c  41749  dochdmj1  41763  djhlj  41774  djhljjN  41775  djhjlj  41776  dihsumssj  41781  djhexmid  41784  djhlsmcl  41787  djhcvat42  41788  dihjatcclem4  41794  dihjat1lem  41801  dihsmsprn  41803  dihjat3  41805  dvh3dim2  41821  dvh3dim3N  41822  dochkr1OLDN  41852  lclkrlem2c  41882  lclkrlem2d  41883  mapdpglem23  42067  hdmap11lem2  42215  0prjspn  42983  mzpcompact2lem  43105  diophrw  43113  rexrabdioph  43148  eldioph4b  43165  pellexlem5  43187  pellfund14  43252  acongtr  43332  fnwe2lem3  43406  gicabl  43453  hbtlem2  43478  hbtlem4  43480  hbtlem5  43482  dgraalem  43499  aaitgo  43516  onexlimgt  43597  onexoegt  43598  oalim2cl  43643  cantnfresb  43678  onmcl  43685  tfsconcatfv  43695  tfsconcatrn  43696  ofoaid1  43712  ofoaid2  43713  ntrclsk13  44424  gneispb  44484  wessf1ornlem  45541  ltdiv23neg  45749  islptre  45976  limclner  46006  icccncfext  46242  stoweidlem1  46356  stoweidlem14  46369  stoweidlem24  46379  stoweidlem46  46401  stoweidlem57  46412  dirkercncflem2  46459  fourierdlem20  46482  fourierdlem41  46503  fourierdlem46  46507  fourierdlem48  46509  fourierdlem50  46511  fourierdlem62  46523  fourierdlem63  46524  fourierdlem64  46525  fourierdlem65  46526  fourierdlem76  46537  fourierdlem79  46540  fourierdlem103  46564  fourierdlem104  46565  etransclem47  46636  m1modmmod  47715  iccpartiun  47791  reupr  47879  sqrtpwpw2p  47895  fmtnoprmfac1lem  47921  fmtnoprmfac2lem1  47923  lighneallem4a  47965  requad2  47980  perfectALTV  48080  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  isuspgrim0lem  48250  isuspgrim0  48251  isuspgrimlem  48252  upgrimwlklem2  48255  upgrimwlklem3  48256  upgrimtrlslem1  48261  uhgrimisgrgriclem  48287  uhgrimisgrgric  48288  clnbgrgrimlem  48290  grimgrtri  48306  gpgedgvtx1  48419  gpgedg2ov  48423  gpgedg2iv  48424  gsumlsscl  48737  lincsumcl  48788  lincscmcl  48789  isldepslvec2  48842  elbigo2  48909  relogbdivb  48919  blennnt2  48946  dignn0ldlem  48959  itsclc0yqsollem2  49120  inlinecirc02p  49144  lubeldm2  49312  glbeldm2  49313  lubsscl  49316  glbsscl  49317  isclatd  49339  sectpropdlem  49392  invpropdlem  49394  isopropdlem  49396  uptrlem1  49566  fucofulem1  49666  fullthinc  49806