Theorem syl12anc 850

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl22anc  852  raaan  4481  raaanv  4482  raaan2  4485  copsex2dv  5479  soltmin  6138  xpdifid  6167  xpdifcnvepel  6168  reuop  6298  f1dom3fv3dif  7268  f1prex  7288  cocan1  7295  fliftfun  7316  soisores  7331  soisoi  7332  isopolem  7349  f1oiso2  7356  weniso  7360  caovcld  7609  caovcomd  7612  onminex  7803  poxp2  8141  poxp3  8148  poseq  8156  tfrlem12  8378  omeulem1  8569  nnaordex2  8627  oaabs2  8637  omabs  8639  eldifsucnn  8652  naddcllem  8664  erov  8814  findcard2d  9154  frfi  9248  finsschain  9319  suplub2  9424  supgtoreq  9434  supisolem  9437  ordiso2  9480  ordtypelem7  9489  wemaplem2  9512  wemapsolem  9515  cantnflt  9644  cantnfp1lem3  9652  cantnflem1b  9658  cantnflem1  9661  wemapwe  9669  cnfcomlem  9671  cnfcom  9672  cnfcom3lem  9675  infxpenlem  10009  fseqenlem1  10020  dfac12lem2  10140  infpssrlem4  10301  enfin2i  10316  isf34lem7  10374  isf34lem6  10375  fin1a2lem7  10401  fin1a2lem10  10404  fin1a2lem11  10405  fin1a2lem13  10407  ttukeylem6  10509  ttukeylem7  10510  iundom2g  10535  fpwwe2lem5  10631  fpwwe2lem6  10632  fpwwe2lem8  10634  fpwwe2lem11  10637  fpwwe2  10639  canthnumlem  10644  canthwelem  10646  canthp1lem2  10649  pwfseqlem4  10658  inar1  10771  intgru  10810  distrlem4pr  11022  conjmul  11943  lediv12a  12119  recp1lt1  12124  cju  12225  gtndiv  12684  zsupss  12972  uzsupss  12975  icc0  13431  iccssioo2  13457  fzrev3  13630  ico01fl0  13865  fldiv  13906  modabs  13950  modltm1p1mod  13972  modifeq2int  13982  modsumfzodifsn  13993  seqcaopr  14088  seqf1olem1  14090  seqof2  14109  crreczi  14277  seqcoll  14514  seqcoll2  14515  hashtpg  14535  swrdccat3b  14794  sgnmul  15163  01sqrexlem2  15313  resqrex  15320  abs1m  15406  isercoll  15738  zsum  15787  fsum2dlem  15839  fsumcom2  15843  fprod2dlem  16052  fprodcom2  16056  efsub  16173  bitsinv2  16518  sqgcd  16637  expgcd  16638  qredeu  16733  isprm7  16784  pcpremul  16920  pceulem  16922  pczpre  16924  pcdiv  16929  pcqmul  16930  pcqdiv  16934  pcexp  16936  pcdvdsb  16946  pcneg  16951  pcdvdstr  16953  pcgcd1  16954  pc2dvds  16956  pcz  16958  pcaddlem  16965  pcadd  16966  qexpz  16978  expnprm  16979  infpnlem2  16988  ramub2  17091  ramub1lem1  17103  setsstruct2  17251  f1ocpbllem  17595  f1ovscpbl  17597  mreexexlem3d  17719  mreexexlem4d  17720  fthi  17994  ipodrsima  18614  chnind  18694  mgmpropd  18726  sgrppropd  18810  mndpropd  18838  grpsubpropd2  19135  f1ghm0to0  19338  ghmqusker  19380  symgfvne  19474  f1omvdmvd  19536  f1otrspeq  19540  pmtrdifwrdel  19578  pmtrdifwrdel2  19579  psgnunilem2  19588  psgnunilem3  19589  psgnvalii  19602  odf1  19655  lsmpropd  19770  ablnnncan  19915  gsummptshft  20029  dprdf1o  20127  pgpfac1lem3  20172  pgpfac1lem5  20174  pgpfaclem1  20176  ablfaclem2  20181  rngpropd  20275  srgbinomlem3  20333  ringpropd  20396  orngsqr  20998  ornglmullt  21001  orngrmullt  21002  lmodprop2d  21074  lsspropd  21167  lmhmpropd  21223  lbspropd  21249  lbsextlem3  21313  unichnlidl  21391  ssdifidllem  21513  iporthcom  21814  obslbs  21909  assapropd  22050  psrass1  22142  psrass23l  22145  psrass23  22147  mplsubrg  22183  mplmon  22215  mplmonmul  22216  mplcoe1  22217  mplbas2  22222  mplind  22250  evlslem2  22259  mpfind  22295  gsumply1subr  22422  psrplusgpropd  22424  ply1scln0  22481  evls1addd  22560  evls1muld  22561  evls1vsca  22562  asclply1subcl  22563  scmataddcl  22702  scmatsubcl  22703  scmatmulcl  22704  smatvscl  22710  scmatrhmcl  22714  mat1scmat  22725  smadiadetglem2  22858  cramerimplem2  22870  cramerimplem3  22871  cramerimp  22872  1pmatscmul  22888  mat2pmatf1  22915  pm2mp  23011  chmatcl  23014  chmatval  23015  chmaidscmat  23034  chfacfisf  23040  cayhamlem1  23052  cpmidgsumm2pm  23055  cpmidpmat  23059  cpmadugsumfi  23063  cpmadumatpoly  23069  cayhamlem3  23073  pptbas  23194  elcls  23259  neiint  23290  neiptopnei  23318  restbas  23344  neitr  23366  iscnp4  23449  cnconst2  23469  cnpdis  23479  cnt0  23532  cnhaus  23540  cmpcovf  23577  hauscmplem  23592  conncompid  23617  2ndci  23634  2ndc1stc  23637  1stcrest  23639  2ndcctbss  23641  2ndcomap  23644  2ndcsep  23645  dis2ndc  23646  restlly  23669  islly2  23670  lly1stc  23682  dislly  23683  finlocfin  23706  dissnlocfin  23715  locfindis  23716  llycmpkgen2  23736  ptbasfi  23767  neitx  23793  ptpjopn  23798  ptcnplem  23807  upxp  23809  txlly  23822  txtube  23826  tx1stc  23836  txkgen  23838  xkococnlem  23845  kqreglem1  23927  kqreglem2  23928  kqnrmlem1  23929  kqnrmlem2  23930  hmeoimaf1o  23956  reghmph  23979  nrmhmph  23980  ordthmeolem  23987  trfil2  24073  fmfnfm  24144  hauspwpwf1  24173  fclsfnflim  24213  cnextf  24252  cnextcn  24253  tmdgsum2  24282  symgtgp  24292  subgntr  24293  opnsubg  24294  ghmcnp  24301  qustgpopn  24306  tsmsf1o  24331  tsmsxplem1  24339  tsmsxplem2  24340  tsmsxp  24341  ustexsym  24402  restutop  24423  imasdsf1olem  24559  blssexps  24612  blssex  24613  ssblex  24614  imasf1oxms  24675  blcld  24691  stdbdmopn  24704  met1stc  24707  met2ndci  24708  prdsxmslem2  24715  metcnp3  24726  cfilucfil  24745  ngptgp  24822  tgioo  24982  tgqioo  24986  zdis  25003  iccpnfhmeo  25133  xrhmeo  25134  cnheibor  25143  elpi1i  25234  cmetcusp  25542  bncssbn  25562  pjthlem2  25626  ivthlem2  25640  ovolicc1  25704  ovolicc2lem3  25707  ovolicc2lem4  25708  volsup  25744  volivth  25795  vitalilem3  25798  mbflimsup  25854  mbfi1fseqlem1  25903  mbfi1fseqlem3  25905  mbfi1fseqlem5  25907  limcnlp  26066  limcflf  26069  limciun  26082  dvmptfsum  26163  dvcnvlem  26164  dvcvx  26208  facth1  26353  elply2  26382  plypf1  26398  coeeq  26413  aaliou3lem8  26537  ulm2  26577  mtestbdd  26597  reeff1o  26639  logbgcd1irr  26988  dcubic2  27038  quart  27055  xrlimcnp  27162  amgm  27184  harmonicbnd4  27204  perfect  27424  dchrptlem1  27457  bposlem2  27478  lgsfcl2  27496  lgsdir  27525  lgsdi  27527  lgsne0  27528  2lgslem1a1  27582  2sqmod  27629  dchrvmasumlem2  27691  chpdifbndlem2  27747  pntpbnd1  27779  pntpbnd2  27780  padicabv  27823  ltsres  27855  nolesgn2o  27864  nogesgn1o  27866  nodense  27885  nosupbnd1lem3  27903  nosupbnd1lem5  27905  nosupbnd2lem1  27908  noinfres  27915  noinfbnd1lem3  27918  noinfbnd1lem5  27920  noinfbnd2lem1  27923  noetalem1  27934  nocvxmin  27977  noeta2  27983  oncutlt  28486  eucliddivs  28598  readdscl  28721  tgcgrxfr  28816  idmot  28835  legid  28885  btwnleg  28886  leg0  28890  tghilberti1  28939  mirreu3  28960  colperpex  29043  lnopp2hpgb  29074  dfprlng2  29226  axcgrrflx  29293  axsegconlem1  29296  axcontlem2  29344  axcontlem12  29354  eengtrkg  29365  wwlksnredwwlkn  30273  0wlkon  30500  0trlon  30504  upgr3v3e3cycl  30560  frgrogt3nreg  30777  nvpi  31048  nmlno0lem  31174  fh1  31999  fh2  32000  nmlnop0iALT  32376  nmopun  32395  branmfn  32486  opsqrlem1  32521  opsqrlem6  32526  mdslmd1lem1  32706  csmdsymi  32715  atom1d  32734  chirredlem2  32772  cdj1i  32814  cdj3i  32822  fcnvgreu  33046  suppovss  33055  xrofsup  33141  nn0difffzod  33178  pwrssmgc  33343  gsummpt2d  33392  gsumhashmul  33410  odpmco  33429  cycpmco2lem6  33474  cycpmco2  33476  cyc3evpm  33493  cycpmconjslem2  33498  fxpsubg  33516  fxpsdrg  33518  archirngz  33532  archiabllem2a  33537  elrgspnlem4  33588  rloc0g  33615  rloc1r  33616  domnpropd  33623  sdrgdvcl  33643  sdrginvcl  33644  lindssn  33714  lindfpropd  33718  ssmxidllem  33779  drnglring  33805  dflring2  33806  rsprprmprmidlb  33836  rprmirredb  33845  1arithufd  33861  ply1asclunit  33887  ply1dg1rt  33893  ply1dg3rt0irred  33897  ply1degltel  33907  ply1degleel  33908  ply1degltlss  33909  psrmonmul  33963  esplyind  33988  esplyindfv  33989  lsssra  34001  lindsun  34038  dimkerim  34040  fedgmullem2  34043  fldextrspunlem1  34088  fldextrspunfld  34089  irngss  34100  irngnzply1  34104  algextdeglem2  34131  algextdeglem4  34133  constrext2chnlem  34163  metideq  34306  metider  34307  pstmfval  34309  lmxrge0  34365  qqhval2  34395  qqhf  34399  qqhghm  34401  qqhrhm  34402  esumpcvgval  34491  esum2dlem  34505  esum2d  34506  sigainb  34550  insiga  34551  ddemeas  34650  imambfm  34676  dya2icoseg  34691  dya2iocnrect  34695  eulerpartlemgvv  34790  probun  34833  ballotlemfc0  34907  ballotlemfcc  34908  breprexplemc  35043  erdszelem8  35703  erdszelem9  35704  erdsze2lem2  35709  cnpconn  35735  txpconn  35737  ptpconn  35738  indispconn  35739  connpconn  35740  cvxpconn  35747  cnllysconn  35750  cvmcov2  35780  cvmopnlem  35783  cvmliftmolem1  35786  cvmliftlem14  35802  cvmliftlem15  35803  cvmlift2lem13  35820  cvmlift3lem2  35825  cvmlift3lem9  35832  seglerflx  36617  seglemin  36618  btwnsegle  36622  hilbert1.1  36659  neibastop2lem  36904  weiunfrlem  37008  weiunso  37010  mh-inf3f1  37085  bj-finsumval0  37962  qdiff  38004  relowlssretop  38042  wl-2sb6d  38246  tan2h  38296  poimirlem1  38305  poimirlem3  38307  poimirlem4  38308  poimirlem9  38313  poimirlem22  38326  poimirlem28  38332  heicant  38339  mblfinlem2  38342  itg2addnc  38358  ftc2nc  38386  dvasin  38388  sdclem1  38427  fdc  38429  istotbnd3  38455  sstotbnd  38459  prdstotbnd  38478  prdsbnd2  38479  cntotbnd  38480  rngoisocnv  38665  lsmsat  39815  islfld  39869  ps-2  40285  lplnexllnN  40371  4atlem9  40410  4atlem10a  40411  lnatexN  40586  2lnat  40591  pmapjat1  40660  lhpj1  40829  lhpm0atN  40836  4atexlemex2  40878  4atex  40883  4atex2-0aOLDN  40885  4atex2-0cOLDN  40887  lautcnvle  40896  lautj  40900  lautm  40901  idltrn  40957  cdleme01N  41028  cdleme0ex1N  41030  cdleme5  41047  cdleme9  41060  cdleme11c  41068  cdleme11g  41072  cdlemefrs29bpre0  41203  cdlemefrs29cpre1  41205  cdlemefrs32fva1  41208  cdleme32fva  41244  cdleme32fva1  41245  cdleme32fvaw  41246  cdleme32d  41251  cdleme32f  41253  cdleme35fnpq  41256  cdleme48d  41342  cdleme48gfv  41344  cdleme50ltrn  41364  trlord  41376  cdlemg4b1  41416  cdlemg4b2  41417  cdlemg13a  41458  cdlemg17a  41468  cdlemg17f  41473  erng1lem  41794  erngdvlem3  41797  erngdvlem4  41798  erng1r  41802  erngdvlem3-rN  41805  erngdvlem4-rN  41806  dva0g  41834  dialss  41853  dia0  41859  dia1N  41860  diaglbN  41862  diameetN  41863  diainN  41864  diaintclN  41865  dia1dim  41868  dia2dimlem5  41875  dia2dimlem7  41877  dia2dimlem9  41879  dia2dimlem10  41880  dia2dimlem12  41882  dia2dimlem13  41883  dvhopvadd  41900  dvhvaddass  41904  dvhopvsca  41909  tendolinv  41912  tendorinv  41913  dvhlveclem  41915  dvh0g  41918  dvheveccl  41919  dvhopN  41923  docaclN  41931  diaocN  41932  djajN  41944  dib0  41971  dib1dim  41972  dibglbN  41973  dibintclN  41974  dib1dim2  41975  diblss  41977  diblsmopel  41978  dicvaddcl  41997  dicvscacl  41998  diclspsn  42001  cdlemn4a  42006  cdlemn11c  42016  dihjustlem  42023  dihord1  42025  dihord2a  42026  dihord2b  42027  dihord2cN  42028  dihord11b  42029  dihord11c  42031  dihord2pre  42032  dihlsscpre  42041  dih1dimb  42047  dib2dim  42050  dih2dimb  42051  dih2dimbALTN  42052  dihvalcq2  42054  dihopelvalcpre  42055  dihord6apre  42063  dihord5b  42066  dihord5apre  42069  dih0  42087  dihmeetlem1N  42097  dihglblem5apreN  42098  dihglblem3N  42102  dihmeetlem2N  42106  dihglbcpreN  42107  dihmeetlem4preN  42113  dih1dimatlem0  42135  dih1dimatlem  42136  dihatlat  42141  dihatexv  42145  dihglb2  42149  dihmeet  42150  dihintcl  42151  dihmeet2  42153  doch2val2  42171  dochocss  42173  dihoml4c  42183  dochdmj1  42197  djhlj  42208  djhljjN  42209  djhjlj  42210  dihsumssj  42215  djhexmid  42218  djhlsmcl  42221  djhcvat42  42222  dihjatcclem4  42228  dihjat1lem  42235  dihsmsprn  42237  dihjat3  42239  dvh3dim2  42255  dvh3dim3N  42256  dochkr1OLDN  42286  lclkrlem2c  42316  lclkrlem2d  42317  mapdpglem23  42501  hdmap11lem2  42649  0prjspn  43393  mzpcompact2lem  43515  diophrw  43523  rexrabdioph  43554  eldioph4b  43571  pellexlem5  43593  pellfund14  43658  acongtr  43738  fnwe2lem3  43812  gicabl  43859  hbtlem2  43884  hbtlem4  43886  hbtlem5  43888  dgraalem  43905  aaitgo  43922  onexlimgt  44003  onexoegt  44004  oalim2cl  44049  cantnfresb  44084  onmcl  44091  tfsconcatfv  44101  tfsconcatrn  44102  ofoaid1  44118  ofoaid2  44119  ntrclsk13  44830  gneispb  44890  wessf1ornlem  45936  ltdiv23neg  46142  islptre  46368  limclner  46398  icccncfext  46634  stoweidlem1  46748  stoweidlem14  46761  stoweidlem24  46771  stoweidlem46  46793  stoweidlem57  46804  dirkercncflem2  46851  fourierdlem20  46874  fourierdlem41  46895  fourierdlem46  46899  fourierdlem48  46901  fourierdlem50  46903  fourierdlem62  46915  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem76  46929  fourierdlem79  46932  fourierdlem103  46956  fourierdlem104  46957  etransclem47  47028  m1modmmod  48134  iccpartiun  48216  reupr  48304  sqrtpwpw2p  48323  fmtnoprmfac1lem  48349  fmtnoprmfac2lem1  48351  lighneallem4a  48393  requad2  48421  perfectALTV  48521  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  isuspgrim0lem  48691  isuspgrim0  48692  isuspgrimlem  48693  upgrimwlklem2  48696  upgrimwlklem3  48697  upgrimtrlslem1  48702  uhgrimisgrgriclem  48728  uhgrimisgrgric  48729  clnbgrgrimlem  48731  grimgrtri  48747  gpgedgvtx1  48860  gpgedg2ov  48864  gpgedg2iv  48865  gsumlsscl  49193  lincsumcl  49244  lincscmcl  49245  isldepslvec2  49298  elbigo2  49365  relogbdivb  49375  blennnt2  49402  dignn0ldlem  49415  itsclc0yqsollem2  49576  inlinecirc02p  49600  lubeldm2  49767  glbeldm2  49768  lubsscl  49771  glbsscl  49772  isclatd  49794  sectpropdlem  49847  invpropdlem  49849  isopropdlem  49851  uptrlem1  50021  fucofulem1  50121  fullthinc  50261