Theorem syl12anc 836

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 584	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  838  raaan  4466  raaanv  4467  raaan2  4470  copsex2dv  5437  soltmin  6087  xpdifid  6120  reuop  6245  f1dom3fv3dif  7208  f1prex  7224  cocan1  7231  fliftfun  7252  soisores  7267  soisoi  7268  isopolem  7285  f1oiso2  7292  weniso  7294  caovcld  7545  caovcomd  7548  onminex  7741  poxp2  8079  poxp3  8086  poseq  8094  tfrlem12  8314  omeulem1  8503  nnaordex2  8560  oaabs2  8570  omabs  8572  eldifsucnn  8585  naddcllem  8597  erov  8744  findcard2d  9083  frfi  9176  finsschain  9250  suplub2  9352  supgtoreq  9362  supisolem  9365  ordiso2  9408  ordtypelem7  9417  wemaplem2  9440  wemapsolem  9443  cantnflt  9569  cantnfp1lem3  9577  cantnflem1b  9583  cantnflem1  9586  wemapwe  9594  cnfcomlem  9596  cnfcom  9597  cnfcom3lem  9600  infxpenlem  9911  fseqenlem1  9922  dfac12lem2  10043  infpssrlem4  10204  enfin2i  10219  isf34lem7  10277  isf34lem6  10278  fin1a2lem7  10304  fin1a2lem10  10307  fin1a2lem11  10308  fin1a2lem13  10310  ttukeylem6  10412  ttukeylem7  10413  iundom2g  10438  fpwwe2lem5  10533  fpwwe2lem6  10534  fpwwe2lem8  10536  fpwwe2lem11  10539  fpwwe2  10541  canthnumlem  10546  canthwelem  10548  canthp1lem2  10551  pwfseqlem4  10560  inar1  10673  intgru  10712  distrlem4pr  10924  conjmul  11845  lediv12a  12022  recp1lt1  12027  cju  12128  gtndiv  12556  zsupss  12837  uzsupss  12840  icc0  13295  iccssioo2  13321  fzrev3  13492  ico01fl0  13725  fldiv  13766  modabs  13810  modltm1p1mod  13832  modifeq2int  13842  modsumfzodifsn  13853  seqcaopr  13948  seqf1olem1  13950  seqof2  13969  crreczi  14137  seqcoll  14373  seqcoll2  14374  hashtpg  14394  swrdccat3b  14649  01sqrexlem2  15152  resqrex  15159  abs1m  15245  isercoll  15577  zsum  15627  fsum2dlem  15679  fsumcom2  15683  fprod2dlem  15889  fprodcom2  15893  efsub  16011  bitsinv2  16356  sqgcd  16475  expgcd  16476  qredeu  16571  isprm7  16621  pcpremul  16757  pceulem  16759  pczpre  16761  pcdiv  16766  pcqmul  16767  pcqdiv  16771  pcexp  16773  pcdvdsb  16783  pcneg  16788  pcdvdstr  16790  pcgcd1  16791  pc2dvds  16793  pcz  16795  pcaddlem  16802  pcadd  16803  qexpz  16815  expnprm  16816  infpnlem2  16825  ramub2  16928  ramub1lem1  16940  setsstruct2  17087  f1ocpbllem  17430  f1ovscpbl  17432  mreexexlem3d  17554  mreexexlem4d  17555  fthi  17829  ipodrsima  18449  chnind  18529  mgmpropd  18561  sgrppropd  18641  mndpropd  18669  grpsubpropd2  18961  f1ghm0to0  19159  ghmqusker  19201  symgfvne  19295  f1omvdmvd  19357  f1otrspeq  19361  pmtrdifwrdel  19399  pmtrdifwrdel2  19400  psgnunilem2  19409  psgnunilem3  19410  psgnvalii  19423  odf1  19476  lsmpropd  19591  ablnnncan  19736  gsummptshft  19850  dprdf1o  19948  pgpfac1lem3  19993  pgpfac1lem5  19995  pgpfaclem1  19997  ablfaclem2  20002  rngpropd  20094  srgbinomlem3  20148  ringpropd  20208  orngsqr  20783  ornglmullt  20786  orngrmullt  20787  lmodprop2d  20859  lsspropd  20953  lmhmpropd  21009  lbspropd  21035  lbsextlem3  21099  iporthcom  21574  obslbs  21669  assapropd  21811  psrass1  21902  psrass23l  21905  psrass23  21907  mplsubrg  21943  mplmon  21971  mplmonmul  21972  mplcoe1  21973  mplbas2  21978  mplind  22006  evlslem2  22015  mpfind  22043  gsumply1subr  22147  psrplusgpropd  22149  ply1scln0  22207  evls1addd  22287  evls1muld  22288  evls1vsca  22289  asclply1subcl  22290  scmataddcl  22432  scmatsubcl  22433  scmatmulcl  22434  smatvscl  22440  scmatrhmcl  22444  mat1scmat  22455  smadiadetglem2  22588  cramerimplem2  22600  cramerimplem3  22601  cramerimp  22602  1pmatscmul  22618  mat2pmatf1  22645  pm2mp  22741  chmatcl  22744  chmatval  22745  chmaidscmat  22764  chfacfisf  22770  cayhamlem1  22782  cpmidgsumm2pm  22785  cpmidpmat  22789  cpmadugsumfi  22793  cpmadumatpoly  22799  cayhamlem3  22803  pptbas  22924  elcls  22989  neiint  23020  neiptopnei  23048  restbas  23074  neitr  23096  iscnp4  23179  cnconst2  23199  cnpdis  23209  cnt0  23262  cnhaus  23270  cmpcovf  23307  hauscmplem  23322  conncompid  23347  2ndci  23364  2ndc1stc  23367  1stcrest  23369  2ndcctbss  23371  2ndcomap  23374  2ndcsep  23375  dis2ndc  23376  restlly  23399  islly2  23400  lly1stc  23412  dislly  23413  finlocfin  23436  dissnlocfin  23445  locfindis  23446  llycmpkgen2  23466  ptbasfi  23497  neitx  23523  ptpjopn  23528  ptcnplem  23537  upxp  23539  txlly  23552  txtube  23556  tx1stc  23566  txkgen  23568  xkococnlem  23575  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  hmeoimaf1o  23686  reghmph  23709  nrmhmph  23710  ordthmeolem  23717  trfil2  23803  fmfnfm  23874  hauspwpwf1  23903  fclsfnflim  23943  cnextf  23982  cnextcn  23983  tmdgsum2  24012  symgtgp  24022  subgntr  24023  opnsubg  24024  ghmcnp  24031  qustgpopn  24036  tsmsf1o  24061  tsmsxplem1  24069  tsmsxplem2  24070  tsmsxp  24071  ustexsym  24132  restutop  24153  imasdsf1olem  24289  blssexps  24342  blssex  24343  ssblex  24344  imasf1oxms  24405  blcld  24421  stdbdmopn  24434  met1stc  24437  met2ndci  24438  prdsxmslem2  24445  metcnp3  24456  cfilucfil  24475  ngptgp  24552  tgioo  24712  tgqioo  24716  zdis  24733  iccpnfhmeo  24871  xrhmeo  24872  cnheibor  24882  elpi1i  24974  cmetcusp  25282  bncssbn  25302  pjthlem2  25366  ivthlem2  25381  ovolicc1  25445  ovolicc2lem3  25448  ovolicc2lem4  25449  volsup  25485  volivth  25536  vitalilem3  25539  mbflimsup  25595  mbfi1fseqlem1  25644  mbfi1fseqlem3  25646  mbfi1fseqlem5  25648  limcnlp  25807  limcflf  25810  limciun  25823  dvmptfsum  25907  dvcnvlem  25908  dvcvx  25953  facth1  26100  elply2  26129  plypf1  26145  coeeq  26160  aaliou3lem8  26281  ulm2  26322  mtestbdd  26342  reeff1o  26385  logbgcd1irr  26732  dcubic2  26782  quart  26799  xrlimcnp  26906  amgm  26929  harmonicbnd4  26949  perfect  27170  dchrptlem1  27203  bposlem2  27224  lgsfcl2  27242  lgsdir  27271  lgsdi  27273  lgsne0  27274  2lgslem1a1  27328  2sqmod  27375  dchrvmasumlem2  27437  chpdifbndlem2  27493  pntpbnd1  27525  pntpbnd2  27526  padicabv  27569  sltres  27602  nolesgn2o  27611  nogesgn1o  27613  nodense  27632  nosupbnd1lem3  27650  nosupbnd1lem5  27652  nosupbnd2lem1  27655  noinfres  27662  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noinfbnd2lem1  27670  noetalem1  27681  nocvxmin  27719  noeta2  27725  onscutlt  28202  eucliddivs  28302  readdscl  28402  tgcgrxfr  28497  idmot  28516  legid  28566  btwnleg  28567  leg0  28571  tghilberti1  28616  mirreu3  28633  colperpex  28712  lnopp2hpgb  28742  axcgrrflx  28894  axsegconlem1  28897  axcontlem2  28945  axcontlem12  28955  eengtrkg  28966  wwlksnredwwlkn  29875  0wlkon  30102  0trlon  30106  upgr3v3e3cycl  30162  frgrogt3nreg  30379  nvpi  30649  nmlno0lem  30775  fh1  31600  fh2  31601  nmlnop0iALT  31977  nmopun  31996  branmfn  32087  opsqrlem1  32122  opsqrlem6  32127  mdslmd1lem1  32307  csmdsymi  32316  atom1d  32335  chirredlem2  32373  cdj1i  32415  cdj3i  32423  fcnvgreu  32657  suppovss  32666  xrofsup  32754  nn0difffzod  32791  sgnmul  32823  pwrssmgc  32988  gsummpt2d  33036  gsumhashmul  33048  odpmco  33062  cycpmco2lem6  33107  cycpmco2  33109  cyc3evpm  33126  cycpmconjslem2  33131  fxpsubg  33149  fxpsdrg  33151  archirngz  33165  archiabllem2a  33170  elrgspnlem4  33219  rloc0g  33245  rloc1r  33246  domnpropd  33250  sdrgdvcl  33272  sdrginvcl  33273  lindssn  33350  lindfpropd  33354  ssdifidllem  33428  ssmxidllem  33445  rsprprmprmidlb  33495  rprmirredb  33504  1arithufd  33520  ply1asclunit  33544  ply1dg1rt  33550  ply1dg3rt0irred  33553  ply1degltel  33562  ply1degleel  33563  ply1degltlss  33564  esplyind  33613  lsssra  33621  lindsun  33659  dimkerim  33661  fedgmullem2  33664  fldextrspunlem1  33709  fldextrspunfld  33710  irngss  33721  irngnzply1  33725  algextdeglem2  33752  algextdeglem4  33754  constrext2chnlem  33784  metideq  33927  metider  33928  pstmfval  33930  lmxrge0  33986  qqhval2  34016  qqhf  34020  qqhghm  34022  qqhrhm  34023  esumpcvgval  34112  esum2dlem  34126  esum2d  34127  sigainb  34170  insiga  34171  ddemeas  34270  imambfm  34296  dya2icoseg  34311  dya2iocnrect  34315  eulerpartlemgvv  34410  probun  34453  ballotlemfc0  34527  ballotlemfcc  34528  breprexplemc  34666  erdszelem8  35263  erdszelem9  35264  erdsze2lem2  35269  cnpconn  35295  txpconn  35297  ptpconn  35298  indispconn  35299  connpconn  35300  cvxpconn  35307  cnllysconn  35310  cvmcov2  35340  cvmopnlem  35343  cvmliftmolem1  35346  cvmliftlem14  35362  cvmliftlem15  35363  cvmlift2lem13  35380  cvmlift3lem2  35385  cvmlift3lem9  35392  seglerflx  36177  seglemin  36178  btwnsegle  36182  hilbert1.1  36219  neibastop2lem  36425  weiunfrlem  36529  weiunso  36531  bj-finsumval0  37350  relowlssretop  37428  wl-2sb6d  37623  tan2h  37672  poimirlem1  37681  poimirlem3  37683  poimirlem4  37684  poimirlem9  37689  poimirlem22  37702  poimirlem28  37708  heicant  37715  mblfinlem2  37718  itg2addnc  37734  ftc2nc  37762  dvasin  37764  sdclem1  37803  fdc  37805  istotbnd3  37831  sstotbnd  37835  prdstotbnd  37854  prdsbnd2  37855  cntotbnd  37856  rngoisocnv  38041  lsmsat  39127  islfld  39181  ps-2  39597  lplnexllnN  39683  4atlem9  39722  4atlem10a  39723  lnatexN  39898  2lnat  39903  pmapjat1  39972  lhpj1  40141  lhpm0atN  40148  4atexlemex2  40190  4atex  40195  4atex2-0aOLDN  40197  4atex2-0cOLDN  40199  lautcnvle  40208  lautj  40212  lautm  40213  idltrn  40269  cdleme01N  40340  cdleme0ex1N  40342  cdleme5  40359  cdleme9  40372  cdleme11c  40380  cdleme11g  40384  cdlemefrs29bpre0  40515  cdlemefrs29cpre1  40517  cdlemefrs32fva1  40520  cdleme32fva  40556  cdleme32fva1  40557  cdleme32fvaw  40558  cdleme32d  40563  cdleme32f  40565  cdleme35fnpq  40568  cdleme48d  40654  cdleme48gfv  40656  cdleme50ltrn  40676  trlord  40688  cdlemg4b1  40728  cdlemg4b2  40729  cdlemg13a  40770  cdlemg17a  40780  cdlemg17f  40785  erng1lem  41106  erngdvlem3  41109  erngdvlem4  41110  erng1r  41114  erngdvlem3-rN  41117  erngdvlem4-rN  41118  dva0g  41146  dialss  41165  dia0  41171  dia1N  41172  diaglbN  41174  diameetN  41175  diainN  41176  diaintclN  41177  dia1dim  41180  dia2dimlem5  41187  dia2dimlem7  41189  dia2dimlem9  41191  dia2dimlem10  41192  dia2dimlem12  41194  dia2dimlem13  41195  dvhopvadd  41212  dvhvaddass  41216  dvhopvsca  41221  tendolinv  41224  tendorinv  41225  dvhlveclem  41227  dvh0g  41230  dvheveccl  41231  dvhopN  41235  docaclN  41243  diaocN  41244  djajN  41256  dib0  41283  dib1dim  41284  dibglbN  41285  dibintclN  41286  dib1dim2  41287  diblss  41289  diblsmopel  41290  dicvaddcl  41309  dicvscacl  41310  diclspsn  41313  cdlemn4a  41318  cdlemn11c  41328  dihjustlem  41335  dihord1  41337  dihord2a  41338  dihord2b  41339  dihord2cN  41340  dihord11b  41341  dihord11c  41343  dihord2pre  41344  dihlsscpre  41353  dih1dimb  41359  dib2dim  41362  dih2dimb  41363  dih2dimbALTN  41364  dihvalcq2  41366  dihopelvalcpre  41367  dihord6apre  41375  dihord5b  41378  dihord5apre  41381  dih0  41399  dihmeetlem1N  41409  dihglblem5apreN  41410  dihglblem3N  41414  dihmeetlem2N  41418  dihglbcpreN  41419  dihmeetlem4preN  41425  dih1dimatlem0  41447  dih1dimatlem  41448  dihatlat  41453  dihatexv  41457  dihglb2  41461  dihmeet  41462  dihintcl  41463  dihmeet2  41465  doch2val2  41483  dochocss  41485  dihoml4c  41495  dochdmj1  41509  djhlj  41520  djhljjN  41521  djhjlj  41522  dihsumssj  41527  djhexmid  41530  djhlsmcl  41533  djhcvat42  41534  dihjatcclem4  41540  dihjat1lem  41547  dihsmsprn  41549  dihjat3  41551  dvh3dim2  41567  dvh3dim3N  41568  dochkr1OLDN  41598  lclkrlem2c  41628  lclkrlem2d  41629  mapdpglem23  41813  hdmap11lem2  41961  0prjspn  42746  mzpcompact2lem  42868  diophrw  42876  rexrabdioph  42911  eldioph4b  42928  pellexlem5  42950  pellfund14  43015  acongtr  43095  fnwe2lem3  43169  gicabl  43216  hbtlem2  43241  hbtlem4  43243  hbtlem5  43245  dgraalem  43262  aaitgo  43279  onexlimgt  43360  onexoegt  43361  oalim2cl  43406  cantnfresb  43441  onmcl  43448  tfsconcatfv  43458  tfsconcatrn  43459  ofoaid1  43475  ofoaid2  43476  ntrclsk13  44188  gneispb  44248  wessf1ornlem  45306  ltdiv23neg  45516  islptre  45743  limclner  45773  icccncfext  46009  stoweidlem1  46123  stoweidlem14  46136  stoweidlem24  46146  stoweidlem46  46168  stoweidlem57  46179  dirkercncflem2  46226  fourierdlem20  46249  fourierdlem41  46270  fourierdlem46  46274  fourierdlem48  46276  fourierdlem50  46278  fourierdlem62  46290  fourierdlem63  46291  fourierdlem64  46292  fourierdlem65  46293  fourierdlem76  46304  fourierdlem79  46307  fourierdlem103  46331  fourierdlem104  46332  etransclem47  46403  m1modmmod  47482  iccpartiun  47558  reupr  47646  sqrtpwpw2p  47662  fmtnoprmfac1lem  47688  fmtnoprmfac2lem1  47690  lighneallem4a  47732  requad2  47747  perfectALTV  47847  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  isuspgrim0lem  48017  isuspgrim0  48018  isuspgrimlem  48019  upgrimwlklem2  48022  upgrimwlklem3  48023  upgrimtrlslem1  48028  uhgrimisgrgriclem  48054  uhgrimisgrgric  48055  clnbgrgrimlem  48057  grimgrtri  48073  gpgedgvtx1  48186  gpgedg2ov  48190  gpgedg2iv  48191  gsumlsscl  48504  lincsumcl  48556  lincscmcl  48557  isldepslvec2  48610  elbigo2  48677  relogbdivb  48687  blennnt2  48714  dignn0ldlem  48727  itsclc0yqsollem2  48888  inlinecirc02p  48912  lubeldm2  49080  glbeldm2  49081  lubsscl  49084  glbsscl  49085  isclatd  49107  sectpropdlem  49161  invpropdlem  49163  isopropdlem  49165  uptrlem1  49335  fucofulem1  49435  fullthinc  49575