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  4470  raaanv  4471  raaan2  4474  copsex2dv  5441  soltmin  6089  xpdifid  6121  reuop  6245  f1dom3fv3dif  7209  f1prex  7225  cocan1  7232  fliftfun  7253  soisores  7268  soisoi  7269  isopolem  7286  f1oiso2  7293  weniso  7295  caovcld  7546  caovcomd  7549  onminex  7742  poxp2  8083  poxp3  8090  poseq  8098  tfrlem12  8318  omeulem1  8507  nnaordex2  8564  oaabs2  8574  omabs  8576  eldifsucnn  8589  naddcllem  8601  erov  8748  findcard2d  9090  frfi  9190  finsschain  9268  suplub2  9370  supgtoreq  9380  supisolem  9383  ordiso2  9426  ordtypelem7  9435  wemaplem2  9458  wemapsolem  9461  cantnflt  9587  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1  9604  wemapwe  9612  cnfcomlem  9614  cnfcom  9615  cnfcom3lem  9618  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  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  fpwwe2lem11  10554  fpwwe2  10556  canthnumlem  10561  canthwelem  10563  canthp1lem2  10566  pwfseqlem4  10575  inar1  10688  intgru  10727  distrlem4pr  10939  conjmul  11859  lediv12a  12036  recp1lt1  12041  cju  12142  gtndiv  12571  zsupss  12856  uzsupss  12859  icc0  13314  iccssioo2  13340  fzrev3  13511  ico01fl0  13741  fldiv  13782  modabs  13826  modltm1p1mod  13848  modifeq2int  13858  modsumfzodifsn  13869  seqcaopr  13964  seqf1olem1  13966  seqof2  13985  crreczi  14153  seqcoll  14389  seqcoll2  14390  hashtpg  14410  swrdccat3b  14664  01sqrexlem2  15168  resqrex  15175  abs1m  15261  isercoll  15593  zsum  15643  fsum2dlem  15695  fsumcom2  15699  fprod2dlem  15905  fprodcom2  15909  efsub  16027  bitsinv2  16372  sqgcd  16491  expgcd  16492  qredeu  16587  isprm7  16637  pcpremul  16773  pceulem  16775  pczpre  16777  pcdiv  16782  pcqmul  16783  pcqdiv  16787  pcexp  16789  pcdvdsb  16799  pcneg  16804  pcdvdstr  16806  pcgcd1  16807  pc2dvds  16809  pcz  16811  pcaddlem  16818  pcadd  16819  qexpz  16831  expnprm  16832  infpnlem2  16841  ramub2  16944  ramub1lem1  16956  setsstruct2  17103  f1ocpbllem  17446  f1ovscpbl  17448  mreexexlem3d  17570  mreexexlem4d  17571  fthi  17845  ipodrsima  18465  mgmpropd  18543  sgrppropd  18623  mndpropd  18651  grpsubpropd2  18943  f1ghm0to0  19142  ghmqusker  19184  symgfvne  19278  f1omvdmvd  19340  f1otrspeq  19344  pmtrdifwrdel  19382  pmtrdifwrdel2  19383  psgnunilem2  19392  psgnunilem3  19393  psgnvalii  19406  odf1  19459  lsmpropd  19574  ablnnncan  19719  gsummptshft  19833  dprdf1o  19931  pgpfac1lem3  19976  pgpfac1lem5  19978  pgpfaclem1  19980  ablfaclem2  19985  rngpropd  20077  srgbinomlem3  20131  ringpropd  20191  orngsqr  20769  ornglmullt  20772  orngrmullt  20773  lmodprop2d  20845  lsspropd  20939  lmhmpropd  20995  lbspropd  21021  lbsextlem3  21085  iporthcom  21560  obslbs  21655  assapropd  21797  psrass1  21889  psrass23l  21892  psrass23  21894  mplsubrg  21930  mplmon  21958  mplmonmul  21959  mplcoe1  21960  mplbas2  21965  mplind  21993  evlslem2  22002  mpfind  22030  gsumply1subr  22134  psrplusgpropd  22136  ply1scln0  22194  evls1addd  22274  evls1muld  22275  evls1vsca  22276  asclply1subcl  22277  scmataddcl  22419  scmatsubcl  22420  scmatmulcl  22421  smatvscl  22427  scmatrhmcl  22431  mat1scmat  22442  smadiadetglem2  22575  cramerimplem2  22587  cramerimplem3  22588  cramerimp  22589  1pmatscmul  22605  mat2pmatf1  22632  pm2mp  22728  chmatcl  22731  chmatval  22732  chmaidscmat  22751  chfacfisf  22757  cayhamlem1  22769  cpmidgsumm2pm  22772  cpmidpmat  22776  cpmadugsumfi  22780  cpmadumatpoly  22786  cayhamlem3  22790  pptbas  22911  elcls  22976  neiint  23007  neiptopnei  23035  restbas  23061  neitr  23083  iscnp4  23166  cnconst2  23186  cnpdis  23196  cnt0  23249  cnhaus  23257  cmpcovf  23294  hauscmplem  23309  conncompid  23334  2ndci  23351  2ndc1stc  23354  1stcrest  23356  2ndcctbss  23358  2ndcomap  23361  2ndcsep  23362  dis2ndc  23363  restlly  23386  islly2  23387  lly1stc  23399  dislly  23400  finlocfin  23423  dissnlocfin  23432  locfindis  23433  llycmpkgen2  23453  ptbasfi  23484  neitx  23510  ptpjopn  23515  ptcnplem  23524  upxp  23526  txlly  23539  txtube  23543  tx1stc  23553  txkgen  23555  xkococnlem  23562  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  hmeoimaf1o  23673  reghmph  23696  nrmhmph  23697  ordthmeolem  23704  trfil2  23790  fmfnfm  23861  hauspwpwf1  23890  fclsfnflim  23930  cnextf  23969  cnextcn  23970  tmdgsum2  23999  symgtgp  24009  subgntr  24010  opnsubg  24011  ghmcnp  24018  qustgpopn  24023  tsmsf1o  24048  tsmsxplem1  24056  tsmsxplem2  24057  tsmsxp  24058  ustexsym  24119  restutop  24141  imasdsf1olem  24277  blssexps  24330  blssex  24331  ssblex  24332  imasf1oxms  24393  blcld  24409  stdbdmopn  24422  met1stc  24425  met2ndci  24426  prdsxmslem2  24433  metcnp3  24444  cfilucfil  24463  ngptgp  24540  tgioo  24700  tgqioo  24704  zdis  24721  iccpnfhmeo  24859  xrhmeo  24860  cnheibor  24870  elpi1i  24962  cmetcusp  25270  bncssbn  25290  pjthlem2  25354  ivthlem2  25369  ovolicc1  25433  ovolicc2lem3  25436  ovolicc2lem4  25437  volsup  25473  volivth  25524  vitalilem3  25527  mbflimsup  25583  mbfi1fseqlem1  25632  mbfi1fseqlem3  25634  mbfi1fseqlem5  25636  limcnlp  25795  limcflf  25798  limciun  25811  dvmptfsum  25895  dvcnvlem  25896  dvcvx  25941  facth1  26088  elply2  26117  plypf1  26133  coeeq  26148  aaliou3lem8  26269  ulm2  26310  mtestbdd  26330  reeff1o  26373  logbgcd1irr  26720  dcubic2  26770  quart  26787  xrlimcnp  26894  amgm  26917  harmonicbnd4  26937  perfect  27158  dchrptlem1  27191  bposlem2  27212  lgsfcl2  27230  lgsdir  27259  lgsdi  27261  lgsne0  27262  2lgslem1a1  27316  2sqmod  27363  dchrvmasumlem2  27425  chpdifbndlem2  27481  pntpbnd1  27513  pntpbnd2  27514  padicabv  27557  sltres  27590  nolesgn2o  27599  nogesgn1o  27601  nodense  27620  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfres  27650  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2lem1  27658  noetalem1  27669  nocvxmin  27707  noeta2  27713  onscutlt  28188  eucliddivs  28288  readdscl  28386  tgcgrxfr  28481  idmot  28500  legid  28550  btwnleg  28551  leg0  28555  tghilberti1  28600  mirreu3  28617  colperpex  28696  lnopp2hpgb  28726  axcgrrflx  28877  axsegconlem1  28880  axcontlem2  28928  axcontlem12  28938  eengtrkg  28949  wwlksnredwwlkn  29858  0wlkon  30082  0trlon  30086  upgr3v3e3cycl  30142  frgrogt3nreg  30359  nvpi  30629  nmlno0lem  30755  fh1  31580  fh2  31581  nmlnop0iALT  31957  nmopun  31976  branmfn  32067  opsqrlem1  32102  opsqrlem6  32107  mdslmd1lem1  32287  csmdsymi  32296  atom1d  32315  chirredlem2  32353  cdj1i  32395  cdj3i  32403  fcnvgreu  32630  suppovss  32637  xrofsup  32723  nn0difffzod  32762  sgnmul  32793  pwrssmgc  32955  chnind  32966  gsummpt2d  33015  gsumhashmul  33027  odpmco  33041  cycpmco2lem6  33086  cycpmco2  33088  cyc3evpm  33105  cycpmconjslem2  33110  archirngz  33141  archiabllem2a  33146  elrgspnlem4  33195  rloc0g  33221  rloc1r  33222  domnpropd  33226  sdrgdvcl  33248  sdrginvcl  33249  lindssn  33325  lindfpropd  33329  ssdifidllem  33403  ssmxidllem  33420  rsprprmprmidlb  33470  rprmirredb  33479  1arithufd  33495  ply1asclunit  33519  ply1dg1rt  33524  ply1dg3rt0irred  33527  ply1degltel  33536  ply1degleel  33537  ply1degltlss  33538  lsssra  33560  lindsun  33597  dimkerim  33599  fedgmullem2  33602  fldextrspunlem1  33646  fldextrspunfld  33647  irngss  33658  irngnzply1  33662  algextdeglem2  33684  algextdeglem4  33686  constrext2chnlem  33716  metideq  33859  metider  33860  pstmfval  33862  lmxrge0  33918  qqhval2  33948  qqhf  33952  qqhghm  33954  qqhrhm  33955  esumpcvgval  34044  esum2dlem  34058  esum2d  34059  sigainb  34102  insiga  34103  ddemeas  34202  imambfm  34229  dya2icoseg  34244  dya2iocnrect  34248  eulerpartlemgvv  34343  probun  34386  ballotlemfc0  34460  ballotlemfcc  34461  breprexplemc  34599  erdszelem8  35170  erdszelem9  35171  erdsze2lem2  35176  cnpconn  35202  txpconn  35204  ptpconn  35205  indispconn  35206  connpconn  35207  cvxpconn  35214  cnllysconn  35217  cvmcov2  35247  cvmopnlem  35250  cvmliftmolem1  35253  cvmliftlem14  35269  cvmliftlem15  35270  cvmlift2lem13  35287  cvmlift3lem2  35292  cvmlift3lem9  35299  seglerflx  36085  seglemin  36086  btwnsegle  36090  hilbert1.1  36127  neibastop2lem  36333  weiunfrlem  36437  weiunso  36439  bj-finsumval0  37258  relowlssretop  37336  wl-2sb6d  37531  tan2h  37591  poimirlem1  37600  poimirlem3  37602  poimirlem4  37603  poimirlem9  37608  poimirlem22  37621  poimirlem28  37627  heicant  37634  mblfinlem2  37637  itg2addnc  37653  ftc2nc  37681  dvasin  37683  sdclem1  37722  fdc  37724  istotbnd3  37750  sstotbnd  37754  prdstotbnd  37773  prdsbnd2  37774  cntotbnd  37775  rngoisocnv  37960  lsmsat  38986  islfld  39040  ps-2  39457  lplnexllnN  39543  4atlem9  39582  4atlem10a  39583  lnatexN  39758  2lnat  39763  pmapjat1  39832  lhpj1  40001  lhpm0atN  40008  4atexlemex2  40050  4atex  40055  4atex2-0aOLDN  40057  4atex2-0cOLDN  40059  lautcnvle  40068  lautj  40072  lautm  40073  idltrn  40129  cdleme01N  40200  cdleme0ex1N  40202  cdleme5  40219  cdleme9  40232  cdleme11c  40240  cdleme11g  40244  cdlemefrs29bpre0  40375  cdlemefrs29cpre1  40377  cdlemefrs32fva1  40380  cdleme32fva  40416  cdleme32fva1  40417  cdleme32fvaw  40418  cdleme32d  40423  cdleme32f  40425  cdleme35fnpq  40428  cdleme48d  40514  cdleme48gfv  40516  cdleme50ltrn  40536  trlord  40548  cdlemg4b1  40588  cdlemg4b2  40589  cdlemg13a  40630  cdlemg17a  40640  cdlemg17f  40645  erng1lem  40966  erngdvlem3  40969  erngdvlem4  40970  erng1r  40974  erngdvlem3-rN  40977  erngdvlem4-rN  40978  dva0g  41006  dialss  41025  dia0  41031  dia1N  41032  diaglbN  41034  diameetN  41035  diainN  41036  diaintclN  41037  dia1dim  41040  dia2dimlem5  41047  dia2dimlem7  41049  dia2dimlem9  41051  dia2dimlem10  41052  dia2dimlem12  41054  dia2dimlem13  41055  dvhopvadd  41072  dvhvaddass  41076  dvhopvsca  41081  tendolinv  41084  tendorinv  41085  dvhlveclem  41087  dvh0g  41090  dvheveccl  41091  dvhopN  41095  docaclN  41103  diaocN  41104  djajN  41116  dib0  41143  dib1dim  41144  dibglbN  41145  dibintclN  41146  dib1dim2  41147  diblss  41149  diblsmopel  41150  dicvaddcl  41169  dicvscacl  41170  diclspsn  41173  cdlemn4a  41178  cdlemn11c  41188  dihjustlem  41195  dihord1  41197  dihord2a  41198  dihord2b  41199  dihord2cN  41200  dihord11b  41201  dihord11c  41203  dihord2pre  41204  dihlsscpre  41213  dih1dimb  41219  dib2dim  41222  dih2dimb  41223  dih2dimbALTN  41224  dihvalcq2  41226  dihopelvalcpre  41227  dihord6apre  41235  dihord5b  41238  dihord5apre  41241  dih0  41259  dihmeetlem1N  41269  dihglblem5apreN  41270  dihglblem3N  41274  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetlem4preN  41285  dih1dimatlem0  41307  dih1dimatlem  41308  dihatlat  41313  dihatexv  41317  dihglb2  41321  dihmeet  41322  dihintcl  41323  dihmeet2  41325  doch2val2  41343  dochocss  41345  dihoml4c  41355  dochdmj1  41369  djhlj  41380  djhljjN  41381  djhjlj  41382  dihsumssj  41387  djhexmid  41390  djhlsmcl  41393  djhcvat42  41394  dihjatcclem4  41400  dihjat1lem  41407  dihsmsprn  41409  dihjat3  41411  dvh3dim2  41427  dvh3dim3N  41428  dochkr1OLDN  41458  lclkrlem2c  41488  lclkrlem2d  41489  mapdpglem23  41673  hdmap11lem2  41821  0prjspn  42601  mzpcompact2lem  42724  diophrw  42732  rexrabdioph  42767  eldioph4b  42784  pellexlem5  42806  pellfund14  42871  acongtr  42951  fnwe2lem3  43025  gicabl  43072  hbtlem2  43097  hbtlem4  43099  hbtlem5  43101  dgraalem  43118  aaitgo  43135  onexlimgt  43216  onexoegt  43217  oalim2cl  43262  cantnfresb  43297  onmcl  43304  tfsconcatfv  43314  tfsconcatrn  43315  ofoaid1  43331  ofoaid2  43332  ntrclsk13  44044  gneispb  44104  wessf1ornlem  45163  ltdiv23neg  45374  islptre  45601  limclner  45633  icccncfext  45869  stoweidlem1  45983  stoweidlem14  45996  stoweidlem24  46006  stoweidlem46  46028  stoweidlem57  46039  dirkercncflem2  46086  fourierdlem20  46109  fourierdlem41  46130  fourierdlem46  46134  fourierdlem48  46136  fourierdlem50  46138  fourierdlem62  46150  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem76  46164  fourierdlem79  46167  fourierdlem103  46191  fourierdlem104  46192  etransclem47  46263  m1modmmod  47343  iccpartiun  47419  reupr  47507  sqrtpwpw2p  47523  fmtnoprmfac1lem  47549  fmtnoprmfac2lem1  47551  lighneallem4a  47593  requad2  47608  perfectALTV  47708  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  isuspgrim0lem  47878  isuspgrim0  47879  isuspgrimlem  47880  upgrimwlklem2  47883  upgrimwlklem3  47884  upgrimtrlslem1  47889  uhgrimisgrgriclem  47915  uhgrimisgrgric  47916  clnbgrgrimlem  47918  grimgrtri  47934  gpgedgvtx1  48047  gpgedg2ov  48051  gpgedg2iv  48052  gsumlsscl  48365  lincsumcl  48417  lincscmcl  48418  isldepslvec2  48471  elbigo2  48538  relogbdivb  48548  blennnt2  48575  dignn0ldlem  48588  itsclc0yqsollem2  48749  inlinecirc02p  48773  lubeldm2  48941  glbeldm2  48942  lubsscl  48945  glbsscl  48946  isclatd  48968  sectpropdlem  49022  invpropdlem  49024  isopropdlem  49026  uptrlem1  49196  fucofulem1  49296  fullthinc  49436