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  4473  raaanv  4474  raaan2  4477  copsex2dv  5465  soltmin  6129  xpdifid  6158  xpdifcnvepel  6159  reuop  6296  f1dom3fv3dif  7273  f1prex  7293  cocan1  7300  fliftfun  7321  soisores  7336  soisoi  7337  isopolem  7354  f1oiso2  7361  weniso  7365  caovcld  7615  caovcomd  7618  onminex  7817  fnwe2lem4  8151  poxp2  8163  poxp3  8170  poseq  8178  tfrlem12  8401  omeulem1  8594  nnaordex2  8652  oaabs2  8662  omabs  8664  eldifsucnn  8677  naddcllem  8689  erov  8839  findcard2d  9186  frfi  9280  finsschain  9352  suplub2  9457  supgtoreq  9467  supisolem  9470  ordiso2  9513  ordtypelem7  9522  wemaplem2  9545  wemapsolem  9548  cantnflt  9677  cantnfp1lem3  9685  cantnflem1b  9691  cantnflem1  9694  wemapwe  9702  cnfcomlem  9704  cnfcom  9705  cnfcom3lem  9708  infxpenlem  10096  fseqenlem1  10107  dfac12lem2  10227  infpssrlem4  10388  enfin2i  10403  isf34lem7  10461  isf34lem6  10462  fin1a2lem7  10488  fin1a2lem10  10491  fin1a2lem11  10492  fin1a2lem13  10494  ttukeylem6  10596  ttukeylem7  10597  iundom2g  10628  fpwwe2lem5  10724  fpwwe2lem6  10725  fpwwe2lem8  10727  fpwwe2lem11  10730  fpwwe2  10732  canthnumlem  10737  canthwelem  10739  canthp1lem2  10742  pwfseqlem4  10751  inar1  10864  intgru  10903  distrlem4pr  11115  conjmul  12038  lediv12a  12214  recp1lt1  12219  cju  12320  gtndiv  12780  zsupss  13068  uzsupss  13071  icc0  13528  iccssioo2  13554  fzrev3  13728  ico01fl0  13963  fldiv  14004  modabs  14048  modltm1p1mod  14070  modifeq2int  14080  modsumfzodifsn  14091  seqcaopr  14186  seqf1olem1  14188  seqof2  14207  crreczi  14376  seqcoll  14613  seqcoll2  14614  hashtpg  14634  swrdccat3b  14894  sgnmul  15266  01sqrexlem2  15416  resqrex  15423  abs1m  15509  isercoll  15841  zsum  15890  fsum2dlem  15942  fsumcom2  15946  fprod2dlem  16153  fprodcom2  16157  efsub  16274  bitsinv2  16619  sqgcd  16742  expgcd  16743  qredeu  16839  isprm7  16890  pcpremul  17027  pceulem  17029  pczpre  17031  pcdiv  17036  pcqmul  17037  pcqdiv  17041  pcexp  17043  pcdvdsb  17053  pcneg  17058  pcdvdstr  17060  pcgcd1  17061  pc2dvds  17063  pcz  17065  pcaddlem  17072  pcadd  17073  qexpz  17085  expnprm  17086  infpnlem2  17095  ramub2  17198  ramub1lem1  17210  setsstruct2  17358  f1ocpbllem  17702  f1ovscpbl  17704  mreexexlem3d  17826  mreexexlem4d  17827  fthi  18101  ipodrsima  18721  chnind  18801  mgmpropd  18835  sgrppropd  18926  mndpropd  18957  grpsubpropd2  19262  f1ghm0to0  19465  ghmqusker  19507  symgfvne  19601  f1omvdmvd  19663  f1otrspeq  19667  pmtrdifwrdel  19705  pmtrdifwrdel2  19706  psgnunilem2  19715  psgnunilem3  19716  psgnvalii  19729  odf1  19782  lsmpropd  19897  ablnnncan  20042  gsummptshft  20156  dprdf1o  20254  pgpfac1lem3  20299  pgpfac1lem5  20301  pgpfaclem1  20303  ablfaclem2  20308  rngpropd  20402  srgbinomlem3  20460  ringpropd  20525  orngsqr  21129  ornglmullt  21132  orngrmullt  21133  lmodprop2d  21205  lsspropd  21298  lmhmpropd  21354  lbspropd  21380  lbsextlem3  21444  unichnlidl  21522  ssdifidllem  21646  iporthcom  21947  obslbs  22042  assapropd  22185  psrass1  22277  psrass23l  22280  psrass23  22282  mplsubrg  22318  mplmon  22350  mplmonmul  22351  mplcoe1  22352  mplbas2  22357  mplind  22385  evlslem2  22394  mpfind  22430  gsumply1subr  22557  psrplusgpropd  22559  ply1scln0  22616  evls1addd  22695  evls1muld  22696  evls1vsca  22697  asclply1subcl  22698  scmataddcl  22837  scmatsubcl  22838  scmatmulcl  22839  smatvscl  22845  scmatrhmcl  22849  mat1scmat  22860  smadiadetglem2  22993  cramerimplem2  23008  cramerimplem3  23009  cramerimp  23010  1pmatscmul  23026  mat2pmatf1  23053  pm2mp  23149  chmatcl  23152  chmatval  23153  chmaidscmat  23172  chfacfisf  23178  cayhamlem1  23190  cpmidgsumm2pm  23193  cpmidpmat  23197  cpmadugsumfi  23201  cpmadumatpoly  23207  cayhamlem3  23211  pptbas  23332  elcls  23397  neiint  23428  neiptopnei  23456  restbas  23482  neitr  23504  iscnp4  23587  cnconst2  23607  cnpdis  23617  cnt0  23670  cnhaus  23678  cmpcovf  23715  hauscmplem  23730  conncompid  23755  2ndci  23772  2ndc1stc  23775  1stcrest  23777  2ndcctbss  23780  2ndcomap  23783  2ndcsep  23784  dis2ndc  23785  restlly  23808  islly2  23809  lly1stc  23821  dislly  23822  finlocfin  23845  dissnlocfin  23854  locfindis  23855  llycmpkgen2  23875  ptbasfi  23906  neitx  23932  ptpjopn  23937  ptcnplem  23946  upxp  23948  txlly  23961  txtube  23965  tx1stc  23975  txkgen  23977  xkococnlem  23984  kqreglem1  24066  kqreglem2  24067  kqnrmlem1  24068  kqnrmlem2  24069  hmeoimaf1o  24095  reghmph  24118  nrmhmph  24119  ordthmeolem  24126  trfil2  24212  fmfnfm  24283  hauspwpwf1  24312  fclsfnflim  24352  cnextf  24391  cnextcn  24392  tmdgsum2  24421  symgtgp  24431  subgntr  24432  opnsubg  24433  ghmcnp  24440  qustgpopn  24445  tsmsf1o  24470  tsmsxplem1  24478  tsmsxplem2  24479  tsmsxp  24480  ustexsym  24541  restutop  24562  imasdsf1olem  24698  blssexps  24751  blssex  24752  ssblex  24753  imasf1oxms  24814  blcld  24830  stdbdmopn  24843  met1stc  24846  met2ndci  24847  prdsxmslem2  24854  metcnp3  24865  cfilucfil  24884  ngptgp  24961  tgioo  25121  tgqioo  25125  zdis  25142  iccpnfhmeo  25272  xrhmeo  25273  cnheibor  25282  elpi1i  25373  cmetcusp  25681  bncssbn  25701  pjthlem2  25765  ivthlem2  25779  ovolicc1  25843  ovolicc2lem3  25846  ovolicc2lem4  25847  volsup  25883  volivth  25934  vitalilem3  25937  mbflimsup  25993  mbfi1fseqlem1  26042  mbfi1fseqlem3  26044  mbfi1fseqlem5  26046  limcnlp  26204  limcflf  26207  limciun  26220  dvmptfsum  26301  dvcnvlem  26302  dvcvx  26346  facth1  26491  elply2  26520  plypf1  26537  coeeq  26552  aaliou3lem8  26678  ulm2  26718  mtestbdd  26738  reeff1o  26780  logbgcd1irr  27128  dcubic2  27178  quart  27195  xrlimcnp  27302  amgm  27324  harmonicbnd4  27344  perfect  27564  dchrptlem1  27597  bposlem2  27618  lgsfcl2  27636  lgsdir  27665  lgsdi  27667  lgsne0  27668  2lgslem1a1  27722  2sqmod  27769  dchrvmasumlem2  27831  chpdifbndlem2  27887  pntpbnd1  27919  pntpbnd2  27920  padicabv  27963  ltsres  28025  nolesgn2o  28034  nogesgn1o  28036  nodense  28055  nosupbnd1lem3  28073  nosupbnd1lem5  28075  nosupbnd2lem1  28078  noinfres  28085  noinfbnd1lem3  28088  noinfbnd1lem5  28090  noinfbnd2lem1  28093  noetalem1  28104  nocvxmin  28147  noeta2  28153  oncutlt  28656  eucliddivs  28768  readdscl  28891  tgcgrxfr  28987  idmot  29006  legid  29056  btwnleg  29057  leg0  29061  tghilberti1  29111  mirreu3  29132  colperpex  29215  lnopp2hpgb  29247  dfprlng2  29431  axcgrrflx  29498  axsegconlem1  29501  axcontlem2  29549  axcontlem12  29559  eengtrkg  29570  wwlksnredwwlkn  30490  0wlkon  30717  0trlon  30721  upgr3v3e3cycl  30787  frgrogt3nreg  31004  nvpi  31275  nmlno0lem  31401  fh1  32226  fh2  32227  nmlnop0iALT  32603  nmopun  32622  branmfn  32713  opsqrlem1  32748  opsqrlem6  32753  mdslmd1lem1  32933  csmdsymi  32942  atom1d  32961  chirredlem2  32999  cdj1i  33041  cdj3i  33049  fcnvgreu  33314  suppovss  33322  xrofsup  33406  nn0difffzod  33443  pwrssmgc  33608  gsummpt2d  33657  gsumhashmul  33675  odpmco  33694  cycpmco2lem6  33739  cycpmco2  33741  cyc3evpm  33758  cycpmconjslem2  33763  fxpsubg  33781  fxpsdrg  33783  archirngz  33797  archiabllem2a  33802  elrgspnlem4  33853  rloc0g  33880  rloc1r  33881  domnpropd  33888  sdrgdvcl  33908  sdrginvcl  33909  lindssn  33980  lindfpropd  33984  ssmxidllem  34045  drnglring  34071  dflring2  34072  rsprprmprmidlb  34102  rprmirredb  34111  1arithufd  34127  ply1asclunit  34153  ply1dg1rt  34159  ply1dg3rt0irred  34163  ply1degltel  34173  ply1degleel  34174  ply1degltlss  34175  psrmonmul  34229  esplyind  34254  esplyindfv  34255  lsssra  34267  lindsun  34304  dimkerim  34306  fedgmullem2  34309  fldextrspunlem1  34354  fldextrspunfld  34355  irngss  34366  irngnzply1  34370  algextdeglem2  34397  algextdeglem4  34399  constrext2chnlem  34429  metideq  34572  metider  34573  pstmfval  34575  lmxrge0  34631  qqhval2  34661  qqhf  34665  qqhghm  34667  qqhrhm  34668  esumpcvgval  34757  esum2dlem  34771  esum2d  34772  sigainb  34816  insiga  34817  ddemeas  34916  imambfm  34941  dya2icoseg  34956  dya2iocnrect  34960  eulerpartlemgvv  35055  probun  35098  ballotlemfc0  35172  ballotlemfcc  35173  breprexplemc  35308  erdszelem8  36050  erdszelem9  36051  erdsze2lem2  36056  cnpconn  36082  txpconn  36084  ptpconn  36085  indispconn  36086  connpconn  36087  cvxpconn  36094  cnllysconn  36097  cvmcov2  36127  cvmopnlem  36130  cvmliftmolem1  36133  cvmliftlem14  36149  cvmliftlem15  36150  cvmlift2lem13  36167  cvmlift3lem2  36172  cvmlift3lem9  36179  seglerflx  36970  seglemin  36971  btwnsegle  36975  hilbert1.1  37012  neibastop2lem  37241  weiunfrlem  37345  weiunso  37347  mh-inf3f1  37422  bj-finsumval0  38300  qdiff  38342  relowlssretop  38380  wl-2sb6d  38584  tan2h  38629  poimirlem1  38633  poimirlem3  38635  poimirlem4  38636  poimirlem9  38641  poimirlem22  38654  poimirlem28  38660  heicant  38667  mblfinlem2  38670  itg2addnc  38686  ftc2nc  38714  dvasin  38716  sdclem1  38771  fdc  38773  istotbnd3  38799  sstotbnd  38803  prdstotbnd  38822  prdsbnd2  38823  cntotbnd  38824  rngoisocnv  39009  lsmsat  40159  islfld  40213  ps-2  40629  lplnexllnN  40715  4atlem9  40754  4atlem10a  40755  lnatexN  40930  2lnat  40935  pmapjat1  41004  lhpj1  41173  lhpm0atN  41180  4atexlemex2  41222  4atex  41227  4atex2-0aOLDN  41229  4atex2-0cOLDN  41231  lautcnvle  41240  lautj  41244  lautm  41245  idltrn  41301  cdleme01N  41372  cdleme0ex1N  41374  cdleme5  41391  cdleme9  41404  cdleme11c  41412  cdleme11g  41416  cdlemefrs29bpre0  41547  cdlemefrs29cpre1  41549  cdlemefrs32fva1  41552  cdleme32fva  41588  cdleme32fva1  41589  cdleme32fvaw  41590  cdleme32d  41595  cdleme32f  41597  cdleme35fnpq  41600  cdleme48d  41686  cdleme48gfv  41688  cdleme50ltrn  41708  trlord  41720  cdlemg4b1  41760  cdlemg4b2  41761  cdlemg13a  41802  cdlemg17a  41812  cdlemg17f  41817  erng1lem  42138  erngdvlem3  42141  erngdvlem4  42142  erng1r  42146  erngdvlem3-rN  42149  erngdvlem4-rN  42150  dva0g  42178  dialss  42197  dia0  42203  dia1N  42204  diaglbN  42206  diameetN  42207  diainN  42208  diaintclN  42209  dia1dim  42212  dia2dimlem5  42219  dia2dimlem7  42221  dia2dimlem9  42223  dia2dimlem10  42224  dia2dimlem12  42226  dia2dimlem13  42227  dvhopvadd  42244  dvhvaddass  42248  dvhopvsca  42253  tendolinv  42256  tendorinv  42257  dvhlveclem  42259  dvh0g  42262  dvheveccl  42263  dvhopN  42267  docaclN  42275  diaocN  42276  djajN  42288  dib0  42315  dib1dim  42316  dibglbN  42317  dibintclN  42318  dib1dim2  42319  diblss  42321  diblsmopel  42322  dicvaddcl  42341  dicvscacl  42342  diclspsn  42345  cdlemn4a  42350  cdlemn11c  42360  dihjustlem  42367  dihord1  42369  dihord2a  42370  dihord2b  42371  dihord2cN  42372  dihord11b  42373  dihord11c  42375  dihord2pre  42376  dihlsscpre  42385  dih1dimb  42391  dib2dim  42394  dih2dimb  42395  dih2dimbALTN  42396  dihvalcq2  42398  dihopelvalcpre  42399  dihord6apre  42407  dihord5b  42410  dihord5apre  42413  dih0  42431  dihmeetlem1N  42441  dihglblem5apreN  42442  dihglblem3N  42446  dihmeetlem2N  42450  dihglbcpreN  42451  dihmeetlem4preN  42457  dih1dimatlem0  42479  dih1dimatlem  42480  dihatlat  42485  dihatexv  42489  dihglb2  42493  dihmeet  42494  dihintcl  42495  dihmeet2  42497  doch2val2  42515  dochocss  42517  dihoml4c  42527  dochdmj1  42541  djhlj  42552  djhljjN  42553  djhjlj  42554  dihsumssj  42559  djhexmid  42562  djhlsmcl  42565  djhcvat42  42566  dihjatcclem4  42572  dihjat1lem  42579  dihsmsprn  42581  dihjat3  42583  dvh3dim2  42599  dvh3dim3N  42600  dochkr1OLDN  42630  lclkrlem2c  42660  lclkrlem2d  42661  mapdpglem23  42845  hdmap11lem2  42993  0prjspn  43758  mzpcompact2lem  43856  diophrw  43864  rexrabdioph  43895  eldioph4b  43912  pellexlem5  43934  pellfund14  43999  acongtr  44079  gicabl  44195  hbtlem2  44220  hbtlem4  44222  hbtlem5  44224  dgraalem  44241  aaitgo  44258  onexlimgt  44339  onexoegt  44340  oalim2cl  44385  cantnfresb  44420  onmcl  44427  tfsconcatfv  44437  tfsconcatrn  44438  ofoaid1  44454  ofoaid2  44455  ntrclsk13  45165  gneispb  45225  wessf1ornlem  46294  ltdiv23neg  46499  islptre  46725  limclner  46755  icccncfext  46991  stoweidlem1  47105  stoweidlem14  47118  stoweidlem24  47128  stoweidlem46  47150  stoweidlem57  47161  dirkercncflem2  47208  fourierdlem20  47231  fourierdlem41  47252  fourierdlem46  47256  fourierdlem48  47258  fourierdlem50  47260  fourierdlem62  47272  fourierdlem63  47273  fourierdlem64  47274  fourierdlem65  47275  fourierdlem76  47286  fourierdlem79  47289  fourierdlem103  47313  fourierdlem104  47314  etransclem47  47385  m1modmmod  48528  iccpartiun  48610  reupr  48698  sqrtpwpw2p  48717  fmtnoprmfac1lem  48743  fmtnoprmfac2lem1  48745  lighneallem4a  48787  requad2  48815  perfectALTV  48915  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  isuspgrim0lem  49085  isuspgrim0  49086  isuspgrimlem  49087  upgrimwlklem2  49090  upgrimwlklem3  49091  upgrimtrlslem1  49096  uhgrimisgrgriclem  49122  uhgrimisgrgric  49123  clnbgrgrimlem  49125  grimgrtri  49141  gpgedgvtx1  49254  gpgedg2ov  49258  gpgedg2iv  49259  gsumlsscl  49586  lincsumcl  49637  lincscmcl  49638  isldepslvec2  49691  elbigo2  49758  relogbdivb  49768  blennnt2  49795  dignn0ldlem  49808  itsclc0yqsollem2  49969  inlinecirc02p  49993  lubeldm2  50164  glbeldm2  50165  lubsscl  50168  glbsscl  50169  isclatd  50191  sectpropdlem  50244  invpropdlem  50246  isopropdlem  50248  uptrlem1  50420  fucofulem1  50526  fullthinc  50679