Theorem syl12anc 849

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 520	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	1, 4, 5	syl2anc 595	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl22anc  851  raaan  4480  raaanv  4481  raaan2  4484  copsex2dv  5479  soltmin  6138  xpdifid  6167  xpdifcnvepel  6168  reuop  6296  f1dom3fv3dif  7268  f1prex  7284  cocan1  7291  fliftfun  7312  soisores  7327  soisoi  7328  isopolem  7345  f1oiso2  7352  weniso  7354  caovcld  7605  caovcomd  7608  onminex  7802  poxp2  8140  poxp3  8147  poseq  8155  tfrlem12  8377  omeulem1  8568  nnaordex2  8626  oaabs2  8636  omabs  8638  eldifsucnn  8651  naddcllem  8663  erov  8813  findcard2d  9152  frfi  9246  finsschain  9317  suplub2  9422  supgtoreq  9432  supisolem  9435  ordiso2  9478  ordtypelem7  9487  wemaplem2  9510  wemapsolem  9513  cantnflt  9642  cantnfp1lem3  9650  cantnflem1b  9656  cantnflem1  9659  wemapwe  9667  cnfcomlem  9669  cnfcom  9670  cnfcom3lem  9673  infxpenlem  9998  fseqenlem1  10009  dfac12lem2  10129  infpssrlem4  10291  enfin2i  10306  isf34lem7  10364  isf34lem6  10365  fin1a2lem7  10391  fin1a2lem10  10394  fin1a2lem11  10395  fin1a2lem13  10397  ttukeylem6  10499  ttukeylem7  10500  iundom2g  10525  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem8  10624  fpwwe2lem11  10627  fpwwe2  10629  canthnumlem  10634  canthwelem  10636  canthp1lem2  10639  pwfseqlem4  10648  inar1  10761  intgru  10800  distrlem4pr  11012  conjmul  11933  lediv12a  12109  recp1lt1  12114  cju  12215  gtndiv  12674  zsupss  12962  uzsupss  12965  icc0  13421  iccssioo2  13447  fzrev3  13620  ico01fl0  13854  fldiv  13895  modabs  13939  modltm1p1mod  13961  modifeq2int  13971  modsumfzodifsn  13982  seqcaopr  14077  seqf1olem1  14079  seqof2  14098  crreczi  14266  seqcoll  14503  seqcoll2  14504  hashtpg  14524  swrdccat3b  14779  sgnmul  15146  01sqrexlem2  15296  resqrex  15303  abs1m  15389  isercoll  15721  zsum  15771  fsum2dlem  15823  fsumcom2  15827  fprod2dlem  16036  fprodcom2  16040  efsub  16157  bitsinv2  16502  sqgcd  16621  expgcd  16622  qredeu  16717  isprm7  16768  pcpremul  16904  pceulem  16906  pczpre  16908  pcdiv  16913  pcqmul  16914  pcqdiv  16918  pcexp  16920  pcdvdsb  16930  pcneg  16935  pcdvdstr  16937  pcgcd1  16938  pc2dvds  16940  pcz  16942  pcaddlem  16949  pcadd  16950  qexpz  16962  expnprm  16963  infpnlem2  16972  ramub2  17075  ramub1lem1  17087  setsstruct2  17235  f1ocpbllem  17579  f1ovscpbl  17581  mreexexlem3d  17703  mreexexlem4d  17704  fthi  17978  ipodrsima  18598  chnind  18678  mgmpropd  18710  sgrppropd  18790  mndpropd  18818  grpsubpropd2  19113  f1ghm0to0  19316  ghmqusker  19358  symgfvne  19452  f1omvdmvd  19514  f1otrspeq  19518  pmtrdifwrdel  19556  pmtrdifwrdel2  19557  psgnunilem2  19566  psgnunilem3  19567  psgnvalii  19580  odf1  19633  lsmpropd  19748  ablnnncan  19893  gsummptshft  20007  dprdf1o  20105  pgpfac1lem3  20150  pgpfac1lem5  20152  pgpfaclem1  20154  ablfaclem2  20159  rngpropd  20253  srgbinomlem3  20311  ringpropd  20372  orngsqr  20950  ornglmullt  20953  orngrmullt  20954  lmodprop2d  21026  lsspropd  21119  lmhmpropd  21175  lbspropd  21201  lbsextlem3  21265  unichnlidl  21343  ssdifidllem  21465  iporthcom  21766  obslbs  21861  assapropd  22002  psrass1  22094  psrass23l  22097  psrass23  22099  mplsubrg  22135  mplmon  22167  mplmonmul  22168  mplcoe1  22169  mplbas2  22174  mplind  22202  evlslem2  22211  mpfind  22247  gsumply1subr  22374  psrplusgpropd  22376  ply1scln0  22433  evls1addd  22512  evls1muld  22513  evls1vsca  22514  asclply1subcl  22515  scmataddcl  22654  scmatsubcl  22655  scmatmulcl  22656  smatvscl  22662  scmatrhmcl  22666  mat1scmat  22677  smadiadetglem2  22810  cramerimplem2  22822  cramerimplem3  22823  cramerimp  22824  1pmatscmul  22840  mat2pmatf1  22867  pm2mp  22963  chmatcl  22966  chmatval  22967  chmaidscmat  22986  chfacfisf  22992  cayhamlem1  23004  cpmidgsumm2pm  23007  cpmidpmat  23011  cpmadugsumfi  23015  cpmadumatpoly  23021  cayhamlem3  23025  pptbas  23146  elcls  23211  neiint  23242  neiptopnei  23270  restbas  23296  neitr  23318  iscnp4  23401  cnconst2  23421  cnpdis  23431  cnt0  23484  cnhaus  23492  cmpcovf  23529  hauscmplem  23544  conncompid  23569  2ndci  23586  2ndc1stc  23589  1stcrest  23591  2ndcctbss  23593  2ndcomap  23596  2ndcsep  23597  dis2ndc  23598  restlly  23621  islly2  23622  lly1stc  23634  dislly  23635  finlocfin  23658  dissnlocfin  23667  locfindis  23668  llycmpkgen2  23688  ptbasfi  23719  neitx  23745  ptpjopn  23750  ptcnplem  23759  upxp  23761  txlly  23774  txtube  23778  tx1stc  23788  txkgen  23790  xkococnlem  23797  kqreglem1  23879  kqreglem2  23880  kqnrmlem1  23881  kqnrmlem2  23882  hmeoimaf1o  23908  reghmph  23931  nrmhmph  23932  ordthmeolem  23939  trfil2  24025  fmfnfm  24096  hauspwpwf1  24125  fclsfnflim  24165  cnextf  24204  cnextcn  24205  tmdgsum2  24234  symgtgp  24244  subgntr  24245  opnsubg  24246  ghmcnp  24253  qustgpopn  24258  tsmsf1o  24283  tsmsxplem1  24291  tsmsxplem2  24292  tsmsxp  24293  ustexsym  24354  restutop  24375  imasdsf1olem  24511  blssexps  24564  blssex  24565  ssblex  24566  imasf1oxms  24627  blcld  24643  stdbdmopn  24656  met1stc  24659  met2ndci  24660  prdsxmslem2  24667  metcnp3  24678  cfilucfil  24697  ngptgp  24774  tgioo  24934  tgqioo  24938  zdis  24955  iccpnfhmeo  25085  xrhmeo  25086  cnheibor  25095  elpi1i  25186  cmetcusp  25494  bncssbn  25514  pjthlem2  25578  ivthlem2  25592  ovolicc1  25656  ovolicc2lem3  25659  ovolicc2lem4  25660  volsup  25696  volivth  25747  vitalilem3  25750  mbflimsup  25806  mbfi1fseqlem1  25855  mbfi1fseqlem3  25857  mbfi1fseqlem5  25859  limcnlp  26018  limcflf  26021  limciun  26034  dvmptfsum  26115  dvcnvlem  26116  dvcvx  26160  facth1  26305  elply2  26334  plypf1  26350  coeeq  26365  aaliou3lem8  26489  ulm2  26529  mtestbdd  26549  reeff1o  26591  logbgcd1irr  26940  dcubic2  26990  quart  27007  xrlimcnp  27114  amgm  27136  harmonicbnd4  27156  perfect  27376  dchrptlem1  27409  bposlem2  27430  lgsfcl2  27448  lgsdir  27477  lgsdi  27479  lgsne0  27480  2lgslem1a1  27534  2sqmod  27581  dchrvmasumlem2  27643  chpdifbndlem2  27699  pntpbnd1  27731  pntpbnd2  27732  padicabv  27775  ltsres  27807  nolesgn2o  27816  nogesgn1o  27818  nodense  27837  nosupbnd1lem3  27855  nosupbnd1lem5  27857  nosupbnd2lem1  27860  noinfres  27867  noinfbnd1lem3  27870  noinfbnd1lem5  27872  noinfbnd2lem1  27875  noetalem1  27886  nocvxmin  27929  noeta2  27935  oncutlt  28438  eucliddivs  28550  readdscl  28673  tgcgrxfr  28768  idmot  28787  legid  28837  btwnleg  28838  leg0  28842  tghilberti1  28891  mirreu3  28912  colperpex  28995  lnopp2hpgb  29026  dfprlng2  29178  axcgrrflx  29245  axsegconlem1  29248  axcontlem2  29296  axcontlem12  29306  eengtrkg  29317  wwlksnredwwlkn  30225  0wlkon  30452  0trlon  30456  upgr3v3e3cycl  30512  frgrogt3nreg  30729  nvpi  31000  nmlno0lem  31126  fh1  31951  fh2  31952  nmlnop0iALT  32328  nmopun  32347  branmfn  32438  opsqrlem1  32473  opsqrlem6  32478  mdslmd1lem1  32658  csmdsymi  32667  atom1d  32686  chirredlem2  32724  cdj1i  32766  cdj3i  32774  fcnvgreu  32998  suppovss  33007  xrofsup  33093  nn0difffzod  33130  pwrssmgc  33301  gsummpt2d  33350  gsumhashmul  33368  odpmco  33387  cycpmco2lem6  33432  cycpmco2  33434  cyc3evpm  33451  cycpmconjslem2  33456  fxpsubg  33474  fxpsdrg  33476  archirngz  33490  archiabllem2a  33495  elrgspnlem4  33546  rloc0g  33573  rloc1r  33574  domnpropd  33581  sdrgdvcl  33601  sdrginvcl  33602  lindssn  33672  lindfpropd  33676  ssmxidllem  33737  drnglring  33763  dflring2  33764  rsprprmprmidlb  33794  rprmirredb  33803  1arithufd  33819  ply1asclunit  33845  ply1dg1rt  33851  ply1dg3rt0irred  33855  ply1degltel  33865  ply1degleel  33866  ply1degltlss  33867  psrmonmul  33921  esplyind  33946  esplyindfv  33947  lsssra  33959  lindsun  33996  dimkerim  33998  fedgmullem2  34001  fldextrspunlem1  34046  fldextrspunfld  34047  irngss  34058  irngnzply1  34062  algextdeglem2  34089  algextdeglem4  34091  constrext2chnlem  34121  metideq  34264  metider  34265  pstmfval  34267  lmxrge0  34323  qqhval2  34353  qqhf  34357  qqhghm  34359  qqhrhm  34360  esumpcvgval  34449  esum2dlem  34463  esum2d  34464  sigainb  34507  insiga  34508  ddemeas  34607  imambfm  34633  dya2icoseg  34648  dya2iocnrect  34652  eulerpartlemgvv  34747  probun  34790  ballotlemfc0  34864  ballotlemfcc  34865  breprexplemc  35000  erdszelem8  35671  erdszelem9  35672  erdsze2lem2  35677  cnpconn  35703  txpconn  35705  ptpconn  35706  indispconn  35707  connpconn  35708  cvxpconn  35715  cnllysconn  35718  cvmcov2  35748  cvmopnlem  35751  cvmliftmolem1  35754  cvmliftlem14  35770  cvmliftlem15  35771  cvmlift2lem13  35788  cvmlift3lem2  35793  cvmlift3lem9  35800  seglerflx  36585  seglemin  36586  btwnsegle  36590  hilbert1.1  36627  neibastop2lem  36852  weiunfrlem  36956  weiunso  36958  mh-inf3f1  37033  bj-finsumval0  37910  qdiff  37952  relowlssretop  37990  wl-2sb6d  38194  tan2h  38244  poimirlem1  38253  poimirlem3  38255  poimirlem4  38256  poimirlem9  38261  poimirlem22  38274  poimirlem28  38280  heicant  38287  mblfinlem2  38290  itg2addnc  38306  ftc2nc  38334  dvasin  38336  sdclem1  38375  fdc  38377  istotbnd3  38403  sstotbnd  38407  prdstotbnd  38426  prdsbnd2  38427  cntotbnd  38428  rngoisocnv  38613  lsmsat  39763  islfld  39817  ps-2  40233  lplnexllnN  40319  4atlem9  40358  4atlem10a  40359  lnatexN  40534  2lnat  40539  pmapjat1  40608  lhpj1  40777  lhpm0atN  40784  4atexlemex2  40826  4atex  40831  4atex2-0aOLDN  40833  4atex2-0cOLDN  40835  lautcnvle  40844  lautj  40848  lautm  40849  idltrn  40905  cdleme01N  40976  cdleme0ex1N  40978  cdleme5  40995  cdleme9  41008  cdleme11c  41016  cdleme11g  41020  cdlemefrs29bpre0  41151  cdlemefrs29cpre1  41153  cdlemefrs32fva1  41156  cdleme32fva  41192  cdleme32fva1  41193  cdleme32fvaw  41194  cdleme32d  41199  cdleme32f  41201  cdleme35fnpq  41204  cdleme48d  41290  cdleme48gfv  41292  cdleme50ltrn  41312  trlord  41324  cdlemg4b1  41364  cdlemg4b2  41365  cdlemg13a  41406  cdlemg17a  41416  cdlemg17f  41421  erng1lem  41742  erngdvlem3  41745  erngdvlem4  41746  erng1r  41750  erngdvlem3-rN  41753  erngdvlem4-rN  41754  dva0g  41782  dialss  41801  dia0  41807  dia1N  41808  diaglbN  41810  diameetN  41811  diainN  41812  diaintclN  41813  dia1dim  41816  dia2dimlem5  41823  dia2dimlem7  41825  dia2dimlem9  41827  dia2dimlem10  41828  dia2dimlem12  41830  dia2dimlem13  41831  dvhopvadd  41848  dvhvaddass  41852  dvhopvsca  41857  tendolinv  41860  tendorinv  41861  dvhlveclem  41863  dvh0g  41866  dvheveccl  41867  dvhopN  41871  docaclN  41879  diaocN  41880  djajN  41892  dib0  41919  dib1dim  41920  dibglbN  41921  dibintclN  41922  dib1dim2  41923  diblss  41925  diblsmopel  41926  dicvaddcl  41945  dicvscacl  41946  diclspsn  41949  cdlemn4a  41954  cdlemn11c  41964  dihjustlem  41971  dihord1  41973  dihord2a  41974  dihord2b  41975  dihord2cN  41976  dihord11b  41977  dihord11c  41979  dihord2pre  41980  dihlsscpre  41989  dih1dimb  41995  dib2dim  41998  dih2dimb  41999  dih2dimbALTN  42000  dihvalcq2  42002  dihopelvalcpre  42003  dihord6apre  42011  dihord5b  42014  dihord5apre  42017  dih0  42035  dihmeetlem1N  42045  dihglblem5apreN  42046  dihglblem3N  42050  dihmeetlem2N  42054  dihglbcpreN  42055  dihmeetlem4preN  42061  dih1dimatlem0  42083  dih1dimatlem  42084  dihatlat  42089  dihatexv  42093  dihglb2  42097  dihmeet  42098  dihintcl  42099  dihmeet2  42101  doch2val2  42119  dochocss  42121  dihoml4c  42131  dochdmj1  42145  djhlj  42156  djhljjN  42157  djhjlj  42158  dihsumssj  42163  djhexmid  42166  djhlsmcl  42169  djhcvat42  42170  dihjatcclem4  42176  dihjat1lem  42183  dihsmsprn  42185  dihjat3  42187  dvh3dim2  42203  dvh3dim3N  42204  dochkr1OLDN  42234  lclkrlem2c  42264  lclkrlem2d  42265  mapdpglem23  42449  hdmap11lem2  42597  0prjspn  43343  mzpcompact2lem  43465  diophrw  43473  rexrabdioph  43504  eldioph4b  43521  pellexlem5  43543  pellfund14  43608  acongtr  43688  fnwe2lem3  43762  gicabl  43809  hbtlem2  43834  hbtlem4  43836  hbtlem5  43838  dgraalem  43855  aaitgo  43872  onexlimgt  43953  onexoegt  43954  oalim2cl  43999  cantnfresb  44034  onmcl  44041  tfsconcatfv  44051  tfsconcatrn  44052  ofoaid1  44068  ofoaid2  44069  ntrclsk13  44780  gneispb  44840  wessf1ornlem  45886  ltdiv23neg  46092  islptre  46318  limclner  46348  icccncfext  46584  stoweidlem1  46698  stoweidlem14  46711  stoweidlem24  46721  stoweidlem46  46743  stoweidlem57  46754  dirkercncflem2  46801  fourierdlem20  46824  fourierdlem41  46845  fourierdlem46  46849  fourierdlem48  46851  fourierdlem50  46853  fourierdlem62  46865  fourierdlem63  46866  fourierdlem64  46867  fourierdlem65  46868  fourierdlem76  46879  fourierdlem79  46882  fourierdlem103  46906  fourierdlem104  46907  etransclem47  46978  m1modmmod  48084  iccpartiun  48166  reupr  48254  sqrtpwpw2p  48273  fmtnoprmfac1lem  48299  fmtnoprmfac2lem1  48301  lighneallem4a  48343  requad2  48371  perfectALTV  48471  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  isuspgrim0lem  48641  isuspgrim0  48642  isuspgrimlem  48643  upgrimwlklem2  48646  upgrimwlklem3  48647  upgrimtrlslem1  48652  uhgrimisgrgriclem  48678  uhgrimisgrgric  48679  clnbgrgrimlem  48681  grimgrtri  48697  gpgedgvtx1  48810  gpgedg2ov  48814  gpgedg2iv  48815  gsumlsscl  49143  lincsumcl  49194  lincscmcl  49195  isldepslvec2  49248  elbigo2  49315  relogbdivb  49325  blennnt2  49352  dignn0ldlem  49365  itsclc0yqsollem2  49526  inlinecirc02p  49550  lubeldm2  49717  glbeldm2  49718  lubsscl  49721  glbsscl  49722  isclatd  49744  sectpropdlem  49797  invpropdlem  49799  isopropdlem  49801  uptrlem1  49971  fucofulem1  50071  fullthinc  50211