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  4458  raaanv  4459  raaan2  4462  copsex2dv  5448  soltmin  6099  xpdifid  6132  reuop  6257  f1dom3fv3dif  7223  f1prex  7239  cocan1  7246  fliftfun  7267  soisores  7282  soisoi  7283  isopolem  7300  f1oiso2  7307  weniso  7309  caovcld  7560  caovcomd  7563  onminex  7756  poxp2  8093  poxp3  8100  poseq  8108  tfrlem12  8328  omeulem1  8517  nnaordex2  8575  oaabs2  8585  omabs  8587  eldifsucnn  8600  naddcllem  8612  erov  8761  findcard2d  9101  frfi  9195  finsschain  9269  suplub2  9374  supgtoreq  9384  supisolem  9387  ordiso2  9430  ordtypelem7  9439  wemaplem2  9462  wemapsolem  9465  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  11872  lediv12a  12049  recp1lt1  12054  cju  12155  gtndiv  12606  zsupss  12887  uzsupss  12890  icc0  13346  iccssioo2  13372  fzrev3  13544  ico01fl0  13778  fldiv  13819  modabs  13863  modltm1p1mod  13885  modifeq2int  13895  modsumfzodifsn  13906  seqcaopr  14001  seqf1olem1  14003  seqof2  14022  crreczi  14190  seqcoll  14426  seqcoll2  14427  hashtpg  14447  swrdccat3b  14702  01sqrexlem2  15205  resqrex  15212  abs1m  15298  isercoll  15630  zsum  15680  fsum2dlem  15732  fsumcom2  15736  fprod2dlem  15945  fprodcom2  15949  efsub  16067  bitsinv2  16412  sqgcd  16531  expgcd  16532  qredeu  16627  isprm7  16678  pcpremul  16814  pceulem  16816  pczpre  16818  pcdiv  16823  pcqmul  16824  pcqdiv  16828  pcexp  16830  pcdvdsb  16840  pcneg  16845  pcdvdstr  16847  pcgcd1  16848  pc2dvds  16850  pcz  16852  pcaddlem  16859  pcadd  16860  qexpz  16872  expnprm  16873  infpnlem2  16882  ramub2  16985  ramub1lem1  16997  setsstruct2  17144  f1ocpbllem  17488  f1ovscpbl  17490  mreexexlem3d  17612  mreexexlem4d  17613  fthi  17887  ipodrsima  18507  chnind  18587  mgmpropd  18619  sgrppropd  18699  mndpropd  18727  grpsubpropd2  19022  f1ghm0to0  19220  ghmqusker  19262  symgfvne  19356  f1omvdmvd  19418  f1otrspeq  19422  pmtrdifwrdel  19460  pmtrdifwrdel2  19461  psgnunilem2  19470  psgnunilem3  19471  psgnvalii  19484  odf1  19537  lsmpropd  19652  ablnnncan  19797  gsummptshft  19911  dprdf1o  20009  pgpfac1lem3  20054  pgpfac1lem5  20056  pgpfaclem1  20058  ablfaclem2  20063  rngpropd  20155  srgbinomlem3  20209  ringpropd  20269  orngsqr  20843  ornglmullt  20846  orngrmullt  20847  lmodprop2d  20919  lsspropd  21012  lmhmpropd  21068  lbspropd  21094  lbsextlem3  21158  iporthcom  21615  obslbs  21710  assapropd  21851  psrass1  21942  psrass23l  21945  psrass23  21947  mplsubrg  21983  mplmon  22013  mplmonmul  22014  mplcoe1  22015  mplbas2  22020  mplind  22048  evlslem2  22057  mpfind  22093  gsumply1subr  22197  psrplusgpropd  22199  ply1scln0  22256  evls1addd  22336  evls1muld  22337  evls1vsca  22338  asclply1subcl  22339  scmataddcl  22481  scmatsubcl  22482  scmatmulcl  22483  smatvscl  22489  scmatrhmcl  22493  mat1scmat  22504  smadiadetglem2  22637  cramerimplem2  22649  cramerimplem3  22650  cramerimp  22651  1pmatscmul  22667  mat2pmatf1  22694  pm2mp  22790  chmatcl  22793  chmatval  22794  chmaidscmat  22813  chfacfisf  22819  cayhamlem1  22831  cpmidgsumm2pm  22834  cpmidpmat  22838  cpmadugsumfi  22842  cpmadumatpoly  22848  cayhamlem3  22852  pptbas  22973  elcls  23038  neiint  23069  neiptopnei  23097  restbas  23123  neitr  23145  iscnp4  23228  cnconst2  23248  cnpdis  23258  cnt0  23311  cnhaus  23319  cmpcovf  23356  hauscmplem  23371  conncompid  23396  2ndci  23413  2ndc1stc  23416  1stcrest  23418  2ndcctbss  23420  2ndcomap  23423  2ndcsep  23424  dis2ndc  23425  restlly  23448  islly2  23449  lly1stc  23461  dislly  23462  finlocfin  23485  dissnlocfin  23494  locfindis  23495  llycmpkgen2  23515  ptbasfi  23546  neitx  23572  ptpjopn  23577  ptcnplem  23586  upxp  23588  txlly  23601  txtube  23605  tx1stc  23615  txkgen  23617  xkococnlem  23624  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  hmeoimaf1o  23735  reghmph  23758  nrmhmph  23759  ordthmeolem  23766  trfil2  23852  fmfnfm  23923  hauspwpwf1  23952  fclsfnflim  23992  cnextf  24031  cnextcn  24032  tmdgsum2  24061  symgtgp  24071  subgntr  24072  opnsubg  24073  ghmcnp  24080  qustgpopn  24085  tsmsf1o  24110  tsmsxplem1  24118  tsmsxplem2  24119  tsmsxp  24120  ustexsym  24181  restutop  24202  imasdsf1olem  24338  blssexps  24391  blssex  24392  ssblex  24393  imasf1oxms  24454  blcld  24470  stdbdmopn  24483  met1stc  24486  met2ndci  24487  prdsxmslem2  24494  metcnp3  24505  cfilucfil  24524  ngptgp  24601  tgioo  24761  tgqioo  24765  zdis  24782  iccpnfhmeo  24912  xrhmeo  24913  cnheibor  24922  elpi1i  25013  cmetcusp  25321  bncssbn  25341  pjthlem2  25405  ivthlem2  25419  ovolicc1  25483  ovolicc2lem3  25486  ovolicc2lem4  25487  volsup  25523  volivth  25574  vitalilem3  25577  mbflimsup  25633  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem5  25686  limcnlp  25845  limcflf  25848  limciun  25861  dvmptfsum  25942  dvcnvlem  25943  dvcvx  25987  facth1  26132  elply2  26161  plypf1  26177  coeeq  26192  aaliou3lem8  26311  ulm2  26350  mtestbdd  26370  reeff1o  26412  logbgcd1irr  26758  dcubic2  26808  quart  26825  xrlimcnp  26932  amgm  26954  harmonicbnd4  26974  perfect  27194  dchrptlem1  27227  bposlem2  27248  lgsfcl2  27266  lgsdir  27295  lgsdi  27297  lgsne0  27298  2lgslem1a1  27352  2sqmod  27399  dchrvmasumlem2  27461  chpdifbndlem2  27517  pntpbnd1  27549  pntpbnd2  27550  padicabv  27593  ltsres  27626  nolesgn2o  27635  nogesgn1o  27637  nodense  27656  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  noetalem1  27705  nocvxmin  27747  noeta2  27753  oncutlt  28256  eucliddivs  28368  readdscl  28491  tgcgrxfr  28586  idmot  28605  legid  28655  btwnleg  28656  leg0  28660  tghilberti1  28705  mirreu3  28722  colperpex  28801  lnopp2hpgb  28831  axcgrrflx  28983  axsegconlem1  28986  axcontlem2  29034  axcontlem12  29044  eengtrkg  29055  wwlksnredwwlkn  29963  0wlkon  30190  0trlon  30194  upgr3v3e3cycl  30250  frgrogt3nreg  30467  nvpi  30738  nmlno0lem  30864  fh1  31689  fh2  31690  nmlnop0iALT  32066  nmopun  32085  branmfn  32176  opsqrlem1  32211  opsqrlem6  32216  mdslmd1lem1  32396  csmdsymi  32405  atom1d  32424  chirredlem2  32462  cdj1i  32504  cdj3i  32512  fcnvgreu  32745  suppovss  32754  xrofsup  32840  nn0difffzod  32877  sgnmul  32908  pwrssmgc  33060  gsummpt2d  33110  gsumhashmul  33128  odpmco  33147  cycpmco2lem6  33192  cycpmco2  33194  cyc3evpm  33211  cycpmconjslem2  33216  fxpsubg  33234  fxpsdrg  33236  archirngz  33250  archiabllem2a  33255  elrgspnlem4  33306  rloc0g  33332  rloc1r  33333  domnpropd  33338  sdrgdvcl  33360  sdrginvcl  33361  lindssn  33438  lindfpropd  33442  ssdifidllem  33516  ssmxidllem  33533  rsprprmprmidlb  33583  rprmirredb  33592  1arithufd  33608  ply1asclunit  33634  ply1dg1rt  33640  ply1dg3rt0irred  33644  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  psrmonmul  33694  esplyind  33719  esplyindfv  33720  lsssra  33732  lindsun  33769  dimkerim  33771  fedgmullem2  33774  fldextrspunlem1  33819  fldextrspunfld  33820  irngss  33831  irngnzply1  33835  algextdeglem2  33862  algextdeglem4  33864  constrext2chnlem  33894  metideq  34037  metider  34038  pstmfval  34040  lmxrge0  34096  qqhval2  34126  qqhf  34130  qqhghm  34132  qqhrhm  34133  esumpcvgval  34222  esum2dlem  34236  esum2d  34237  sigainb  34280  insiga  34281  ddemeas  34380  imambfm  34406  dya2icoseg  34421  dya2iocnrect  34425  eulerpartlemgvv  34520  probun  34563  ballotlemfc0  34637  ballotlemfcc  34638  breprexplemc  34776  erdszelem8  35380  erdszelem9  35381  erdsze2lem2  35386  cnpconn  35412  txpconn  35414  ptpconn  35415  indispconn  35416  connpconn  35417  cvxpconn  35424  cnllysconn  35427  cvmcov2  35457  cvmopnlem  35460  cvmliftmolem1  35463  cvmliftlem14  35479  cvmliftlem15  35480  cvmlift2lem13  35497  cvmlift3lem2  35502  cvmlift3lem9  35509  seglerflx  36294  seglemin  36295  btwnsegle  36299  hilbert1.1  36336  neibastop2lem  36542  weiunfrlem  36646  weiunso  36648  mh-inf3f1  36723  bj-finsumval0  37599  qdiff  37641  relowlssretop  37679  wl-2sb6d  37883  tan2h  37933  poimirlem1  37942  poimirlem3  37944  poimirlem4  37945  poimirlem9  37950  poimirlem22  37963  poimirlem28  37969  heicant  37976  mblfinlem2  37979  itg2addnc  37995  ftc2nc  38023  dvasin  38025  sdclem1  38064  fdc  38066  istotbnd3  38092  sstotbnd  38096  prdstotbnd  38115  prdsbnd2  38116  cntotbnd  38117  rngoisocnv  38302  lsmsat  39454  islfld  39508  ps-2  39924  lplnexllnN  40010  4atlem9  40049  4atlem10a  40050  lnatexN  40225  2lnat  40230  pmapjat1  40299  lhpj1  40468  lhpm0atN  40475  4atexlemex2  40517  4atex  40522  4atex2-0aOLDN  40524  4atex2-0cOLDN  40526  lautcnvle  40535  lautj  40539  lautm  40540  idltrn  40596  cdleme01N  40667  cdleme0ex1N  40669  cdleme5  40686  cdleme9  40699  cdleme11c  40707  cdleme11g  40711  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdlemefrs32fva1  40847  cdleme32fva  40883  cdleme32fva1  40884  cdleme32fvaw  40885  cdleme32d  40890  cdleme32f  40892  cdleme35fnpq  40895  cdleme48d  40981  cdleme48gfv  40983  cdleme50ltrn  41003  trlord  41015  cdlemg4b1  41055  cdlemg4b2  41056  cdlemg13a  41097  cdlemg17a  41107  cdlemg17f  41112  erng1lem  41433  erngdvlem3  41436  erngdvlem4  41437  erng1r  41441  erngdvlem3-rN  41444  erngdvlem4-rN  41445  dva0g  41473  dialss  41492  dia0  41498  dia1N  41499  diaglbN  41501  diameetN  41502  diainN  41503  diaintclN  41504  dia1dim  41507  dia2dimlem5  41514  dia2dimlem7  41516  dia2dimlem9  41518  dia2dimlem10  41519  dia2dimlem12  41521  dia2dimlem13  41522  dvhopvadd  41539  dvhvaddass  41543  dvhopvsca  41548  tendolinv  41551  tendorinv  41552  dvhlveclem  41554  dvh0g  41557  dvheveccl  41558  dvhopN  41562  docaclN  41570  diaocN  41571  djajN  41583  dib0  41610  dib1dim  41611  dibglbN  41612  dibintclN  41613  dib1dim2  41614  diblss  41616  diblsmopel  41617  dicvaddcl  41636  dicvscacl  41637  diclspsn  41640  cdlemn4a  41645  cdlemn11c  41655  dihjustlem  41662  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord2cN  41667  dihord11b  41668  dihord11c  41670  dihord2pre  41671  dihlsscpre  41680  dih1dimb  41686  dib2dim  41689  dih2dimb  41690  dih2dimbALTN  41691  dihvalcq2  41693  dihopelvalcpre  41694  dihord6apre  41702  dihord5b  41705  dihord5apre  41708  dih0  41726  dihmeetlem1N  41736  dihglblem5apreN  41737  dihglblem3N  41741  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetlem4preN  41752  dih1dimatlem0  41774  dih1dimatlem  41775  dihatlat  41780  dihatexv  41784  dihglb2  41788  dihmeet  41789  dihintcl  41790  dihmeet2  41792  doch2val2  41810  dochocss  41812  dihoml4c  41822  dochdmj1  41836  djhlj  41847  djhljjN  41848  djhjlj  41849  dihsumssj  41854  djhexmid  41857  djhlsmcl  41860  djhcvat42  41861  dihjatcclem4  41867  dihjat1lem  41874  dihsmsprn  41876  dihjat3  41878  dvh3dim2  41894  dvh3dim3N  41895  dochkr1OLDN  41925  lclkrlem2c  41955  lclkrlem2d  41956  mapdpglem23  42140  hdmap11lem2  42288  0prjspn  43061  mzpcompact2lem  43183  diophrw  43191  rexrabdioph  43222  eldioph4b  43239  pellexlem5  43261  pellfund14  43326  acongtr  43406  fnwe2lem3  43480  gicabl  43527  hbtlem2  43552  hbtlem4  43554  hbtlem5  43556  dgraalem  43573  aaitgo  43590  onexlimgt  43671  onexoegt  43672  oalim2cl  43717  cantnfresb  43752  onmcl  43759  tfsconcatfv  43769  tfsconcatrn  43770  ofoaid1  43786  ofoaid2  43787  ntrclsk13  44498  gneispb  44558  wessf1ornlem  45615  ltdiv23neg  45823  islptre  46049  limclner  46079  icccncfext  46315  stoweidlem1  46429  stoweidlem14  46442  stoweidlem24  46452  stoweidlem46  46474  stoweidlem57  46485  dirkercncflem2  46532  fourierdlem20  46555  fourierdlem41  46576  fourierdlem46  46580  fourierdlem48  46582  fourierdlem50  46584  fourierdlem62  46596  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem76  46610  fourierdlem79  46613  fourierdlem103  46637  fourierdlem104  46638  etransclem47  46709  m1modmmod  47812  iccpartiun  47894  reupr  47982  sqrtpwpw2p  48001  fmtnoprmfac1lem  48027  fmtnoprmfac2lem1  48029  lighneallem4a  48071  requad2  48099  perfectALTV  48199  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  isuspgrim0lem  48369  isuspgrim0  48370  isuspgrimlem  48371  upgrimwlklem2  48374  upgrimwlklem3  48375  upgrimtrlslem1  48380  uhgrimisgrgriclem  48406  uhgrimisgrgric  48407  clnbgrgrimlem  48409  grimgrtri  48425  gpgedgvtx1  48538  gpgedg2ov  48542  gpgedg2iv  48543  gsumlsscl  48856  lincsumcl  48907  lincscmcl  48908  isldepslvec2  48961  elbigo2  49028  relogbdivb  49038  blennnt2  49065  dignn0ldlem  49078  itsclc0yqsollem2  49239  inlinecirc02p  49263  lubeldm2  49431  glbeldm2  49432  lubsscl  49435  glbsscl  49436  isclatd  49458  sectpropdlem  49511  invpropdlem  49513  isopropdlem  49515  uptrlem1  49685  fucofulem1  49785  fullthinc  49925