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  4474  raaanv  4475  raaan2  4478  copsex2dv  5471  soltmin  6130  xpdifid  6160  xpdifcnvepel  6161  reuop  6291  f1dom3fv3dif  7265  f1prex  7285  cocan1  7292  fliftfun  7313  soisores  7328  soisoi  7329  isopolem  7346  f1oiso2  7353  weniso  7357  caovcld  7607  caovcomd  7610  onminex  7801  poxp2  8141  poxp3  8148  poseq  8156  tfrlem12  8378  omeulem1  8569  nnaordex2  8627  oaabs2  8637  omabs  8639  eldifsucnn  8652  naddcllem  8664  erov  8814  findcard2d  9161  frfi  9255  finsschain  9326  suplub2  9431  supgtoreq  9441  supisolem  9444  ordiso2  9487  ordtypelem7  9496  wemaplem2  9519  wemapsolem  9522  cantnflt  9651  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1  9668  wemapwe  9676  cnfcomlem  9678  cnfcom  9679  cnfcom3lem  9682  infxpenlem  10016  fseqenlem1  10027  dfac12lem2  10147  infpssrlem4  10308  enfin2i  10323  isf34lem7  10381  isf34lem6  10382  fin1a2lem7  10408  fin1a2lem10  10411  fin1a2lem11  10412  fin1a2lem13  10414  ttukeylem6  10516  ttukeylem7  10517  iundom2g  10548  fpwwe2lem5  10644  fpwwe2lem6  10645  fpwwe2lem8  10647  fpwwe2lem11  10650  fpwwe2  10652  canthnumlem  10657  canthwelem  10659  canthp1lem2  10662  pwfseqlem4  10671  inar1  10784  intgru  10823  distrlem4pr  11035  conjmul  11956  lediv12a  12132  recp1lt1  12137  cju  12238  gtndiv  12698  zsupss  12986  uzsupss  12989  icc0  13446  iccssioo2  13472  fzrev3  13645  ico01fl0  13880  fldiv  13921  modabs  13965  modltm1p1mod  13987  modifeq2int  13997  modsumfzodifsn  14008  seqcaopr  14103  seqf1olem1  14105  seqof2  14124  crreczi  14292  seqcoll  14529  seqcoll2  14530  hashtpg  14550  swrdccat3b  14809  sgnmul  15180  01sqrexlem2  15330  resqrex  15337  abs1m  15423  isercoll  15755  zsum  15804  fsum2dlem  15856  fsumcom2  15860  fprod2dlem  16067  fprodcom2  16071  efsub  16188  bitsinv2  16533  sqgcd  16652  expgcd  16653  qredeu  16748  isprm7  16799  pcpremul  16935  pceulem  16937  pczpre  16939  pcdiv  16944  pcqmul  16945  pcqdiv  16949  pcexp  16951  pcdvdsb  16961  pcneg  16966  pcdvdstr  16968  pcgcd1  16969  pc2dvds  16971  pcz  16973  pcaddlem  16980  pcadd  16981  qexpz  16993  expnprm  16994  infpnlem2  17003  ramub2  17106  ramub1lem1  17118  setsstruct2  17266  f1ocpbllem  17610  f1ovscpbl  17612  mreexexlem3d  17734  mreexexlem4d  17735  fthi  18009  ipodrsima  18629  chnind  18709  mgmpropd  18743  sgrppropd  18833  mndpropd  18864  grpsubpropd2  19169  f1ghm0to0  19372  ghmqusker  19414  symgfvne  19508  f1omvdmvd  19570  f1otrspeq  19574  pmtrdifwrdel  19612  pmtrdifwrdel2  19613  psgnunilem2  19622  psgnunilem3  19623  psgnvalii  19636  odf1  19689  lsmpropd  19804  ablnnncan  19949  gsummptshft  20063  dprdf1o  20161  pgpfac1lem3  20206  pgpfac1lem5  20208  pgpfaclem1  20210  ablfaclem2  20215  rngpropd  20309  srgbinomlem3  20367  ringpropd  20430  orngsqr  21032  ornglmullt  21035  orngrmullt  21036  lmodprop2d  21108  lsspropd  21201  lmhmpropd  21257  lbspropd  21283  lbsextlem3  21347  unichnlidl  21425  ssdifidllem  21547  iporthcom  21848  obslbs  21943  assapropd  22086  psrass1  22178  psrass23l  22181  psrass23  22183  mplsubrg  22219  mplmon  22251  mplmonmul  22252  mplcoe1  22253  mplbas2  22258  mplind  22286  evlslem2  22295  mpfind  22331  gsumply1subr  22458  psrplusgpropd  22460  ply1scln0  22517  evls1addd  22596  evls1muld  22597  evls1vsca  22598  asclply1subcl  22599  scmataddcl  22738  scmatsubcl  22739  scmatmulcl  22740  smatvscl  22746  scmatrhmcl  22750  mat1scmat  22761  smadiadetglem2  22894  cramerimplem2  22909  cramerimplem3  22910  cramerimp  22911  1pmatscmul  22927  mat2pmatf1  22954  pm2mp  23050  chmatcl  23053  chmatval  23054  chmaidscmat  23073  chfacfisf  23079  cayhamlem1  23091  cpmidgsumm2pm  23094  cpmidpmat  23098  cpmadugsumfi  23102  cpmadumatpoly  23108  cayhamlem3  23112  pptbas  23233  elcls  23298  neiint  23329  neiptopnei  23357  restbas  23383  neitr  23405  iscnp4  23488  cnconst2  23508  cnpdis  23518  cnt0  23571  cnhaus  23579  cmpcovf  23616  hauscmplem  23631  conncompid  23656  2ndci  23673  2ndc1stc  23676  1stcrest  23678  2ndcctbss  23681  2ndcomap  23684  2ndcsep  23685  dis2ndc  23686  restlly  23709  islly2  23710  lly1stc  23722  dislly  23723  finlocfin  23746  dissnlocfin  23755  locfindis  23756  llycmpkgen2  23776  ptbasfi  23807  neitx  23833  ptpjopn  23838  ptcnplem  23847  upxp  23849  txlly  23862  txtube  23866  tx1stc  23876  txkgen  23878  xkococnlem  23885  kqreglem1  23967  kqreglem2  23968  kqnrmlem1  23969  kqnrmlem2  23970  hmeoimaf1o  23996  reghmph  24019  nrmhmph  24020  ordthmeolem  24027  trfil2  24113  fmfnfm  24184  hauspwpwf1  24213  fclsfnflim  24253  cnextf  24292  cnextcn  24293  tmdgsum2  24322  symgtgp  24332  subgntr  24333  opnsubg  24334  ghmcnp  24341  qustgpopn  24346  tsmsf1o  24371  tsmsxplem1  24379  tsmsxplem2  24380  tsmsxp  24381  ustexsym  24442  restutop  24463  imasdsf1olem  24599  blssexps  24652  blssex  24653  ssblex  24654  imasf1oxms  24715  blcld  24731  stdbdmopn  24744  met1stc  24747  met2ndci  24748  prdsxmslem2  24755  metcnp3  24766  cfilucfil  24785  ngptgp  24862  tgioo  25022  tgqioo  25026  zdis  25043  iccpnfhmeo  25173  xrhmeo  25174  cnheibor  25183  elpi1i  25274  cmetcusp  25582  bncssbn  25602  pjthlem2  25666  ivthlem2  25680  ovolicc1  25744  ovolicc2lem3  25747  ovolicc2lem4  25748  volsup  25784  volivth  25835  vitalilem3  25838  mbflimsup  25894  mbfi1fseqlem1  25943  mbfi1fseqlem3  25945  mbfi1fseqlem5  25947  limcnlp  26105  limcflf  26108  limciun  26121  dvmptfsum  26202  dvcnvlem  26203  dvcvx  26247  facth1  26392  elply2  26421  plypf1  26438  coeeq  26453  aaliou3lem8  26581  ulm2  26621  mtestbdd  26641  reeff1o  26683  logbgcd1irr  27031  dcubic2  27081  quart  27098  xrlimcnp  27205  amgm  27227  harmonicbnd4  27247  perfect  27467  dchrptlem1  27500  bposlem2  27521  lgsfcl2  27539  lgsdir  27568  lgsdi  27570  lgsne0  27571  2lgslem1a1  27625  2sqmod  27672  dchrvmasumlem2  27734  chpdifbndlem2  27790  pntpbnd1  27822  pntpbnd2  27823  padicabv  27866  ltsres  27898  nolesgn2o  27907  nogesgn1o  27909  nodense  27928  nosupbnd1lem3  27946  nosupbnd1lem5  27948  nosupbnd2lem1  27951  noinfres  27958  noinfbnd1lem3  27961  noinfbnd1lem5  27963  noinfbnd2lem1  27966  noetalem1  27977  nocvxmin  28020  noeta2  28026  oncutlt  28529  eucliddivs  28641  readdscl  28764  tgcgrxfr  28860  idmot  28879  legid  28929  btwnleg  28930  leg0  28934  tghilberti1  28984  mirreu3  29005  colperpex  29088  lnopp2hpgb  29120  dfprlng2  29304  axcgrrflx  29371  axsegconlem1  29374  axcontlem2  29422  axcontlem12  29432  eengtrkg  29443  wwlksnredwwlkn  30363  0wlkon  30590  0trlon  30594  upgr3v3e3cycl  30660  frgrogt3nreg  30877  nvpi  31148  nmlno0lem  31274  fh1  32099  fh2  32100  nmlnop0iALT  32476  nmopun  32495  branmfn  32586  opsqrlem1  32621  opsqrlem6  32626  mdslmd1lem1  32806  csmdsymi  32815  atom1d  32834  chirredlem2  32872  cdj1i  32914  cdj3i  32922  fcnvgreu  33145  suppovss  33153  xrofsup  33238  nn0difffzod  33275  pwrssmgc  33440  gsummpt2d  33489  gsumhashmul  33507  odpmco  33526  cycpmco2lem6  33571  cycpmco2  33573  cyc3evpm  33590  cycpmconjslem2  33595  fxpsubg  33613  fxpsdrg  33615  archirngz  33629  archiabllem2a  33634  elrgspnlem4  33685  rloc0g  33712  rloc1r  33713  domnpropd  33720  sdrgdvcl  33740  sdrginvcl  33741  lindssn  33811  lindfpropd  33815  ssmxidllem  33876  drnglring  33902  dflring2  33903  rsprprmprmidlb  33933  rprmirredb  33942  1arithufd  33958  ply1asclunit  33984  ply1dg1rt  33990  ply1dg3rt0irred  33994  ply1degltel  34004  ply1degleel  34005  ply1degltlss  34006  psrmonmul  34060  esplyind  34085  esplyindfv  34086  lsssra  34098  lindsun  34135  dimkerim  34137  fedgmullem2  34140  fldextrspunlem1  34185  fldextrspunfld  34186  irngss  34197  irngnzply1  34201  algextdeglem2  34228  algextdeglem4  34230  constrext2chnlem  34260  metideq  34403  metider  34404  pstmfval  34406  lmxrge0  34462  qqhval2  34492  qqhf  34496  qqhghm  34498  qqhrhm  34499  esumpcvgval  34588  esum2dlem  34602  esum2d  34603  sigainb  34647  insiga  34648  ddemeas  34747  imambfm  34773  dya2icoseg  34788  dya2iocnrect  34792  eulerpartlemgvv  34887  probun  34930  ballotlemfc0  35004  ballotlemfcc  35005  breprexplemc  35140  erdszelem8  35777  erdszelem9  35778  erdsze2lem2  35783  cnpconn  35809  txpconn  35811  ptpconn  35812  indispconn  35813  connpconn  35814  cvxpconn  35821  cnllysconn  35824  cvmcov2  35854  cvmopnlem  35857  cvmliftmolem1  35860  cvmliftlem14  35876  cvmliftlem15  35877  cvmlift2lem13  35894  cvmlift3lem2  35899  cvmlift3lem9  35906  seglerflx  36692  seglemin  36693  btwnsegle  36697  hilbert1.1  36734  neibastop2lem  36979  weiunfrlem  37083  weiunso  37085  mh-inf3f1  37160  bj-finsumval0  38037  qdiff  38079  relowlssretop  38117  wl-2sb6d  38321  tan2h  38366  poimirlem1  38370  poimirlem3  38372  poimirlem4  38373  poimirlem9  38378  poimirlem22  38391  poimirlem28  38397  heicant  38404  mblfinlem2  38407  itg2addnc  38423  ftc2nc  38451  dvasin  38453  sdclem1  38493  fdc  38495  istotbnd3  38521  sstotbnd  38525  prdstotbnd  38544  prdsbnd2  38545  cntotbnd  38546  rngoisocnv  38731  lsmsat  39881  islfld  39935  ps-2  40351  lplnexllnN  40437  4atlem9  40476  4atlem10a  40477  lnatexN  40652  2lnat  40657  pmapjat1  40726  lhpj1  40895  lhpm0atN  40902  4atexlemex2  40944  4atex  40949  4atex2-0aOLDN  40951  4atex2-0cOLDN  40953  lautcnvle  40962  lautj  40966  lautm  40967  idltrn  41023  cdleme01N  41094  cdleme0ex1N  41096  cdleme5  41113  cdleme9  41126  cdleme11c  41134  cdleme11g  41138  cdlemefrs29bpre0  41269  cdlemefrs29cpre1  41271  cdlemefrs32fva1  41274  cdleme32fva  41310  cdleme32fva1  41311  cdleme32fvaw  41312  cdleme32d  41317  cdleme32f  41319  cdleme35fnpq  41322  cdleme48d  41408  cdleme48gfv  41410  cdleme50ltrn  41430  trlord  41442  cdlemg4b1  41482  cdlemg4b2  41483  cdlemg13a  41524  cdlemg17a  41534  cdlemg17f  41539  erng1lem  41860  erngdvlem3  41863  erngdvlem4  41864  erng1r  41868  erngdvlem3-rN  41871  erngdvlem4-rN  41872  dva0g  41900  dialss  41919  dia0  41925  dia1N  41926  diaglbN  41928  diameetN  41929  diainN  41930  diaintclN  41931  dia1dim  41934  dia2dimlem5  41941  dia2dimlem7  41943  dia2dimlem9  41945  dia2dimlem10  41946  dia2dimlem12  41948  dia2dimlem13  41949  dvhopvadd  41966  dvhvaddass  41970  dvhopvsca  41975  tendolinv  41978  tendorinv  41979  dvhlveclem  41981  dvh0g  41984  dvheveccl  41985  dvhopN  41989  docaclN  41997  diaocN  41998  djajN  42010  dib0  42037  dib1dim  42038  dibglbN  42039  dibintclN  42040  dib1dim2  42041  diblss  42043  diblsmopel  42044  dicvaddcl  42063  dicvscacl  42064  diclspsn  42067  cdlemn4a  42072  cdlemn11c  42082  dihjustlem  42089  dihord1  42091  dihord2a  42092  dihord2b  42093  dihord2cN  42094  dihord11b  42095  dihord11c  42097  dihord2pre  42098  dihlsscpre  42107  dih1dimb  42113  dib2dim  42116  dih2dimb  42117  dih2dimbALTN  42118  dihvalcq2  42120  dihopelvalcpre  42121  dihord6apre  42129  dihord5b  42132  dihord5apre  42135  dih0  42153  dihmeetlem1N  42163  dihglblem5apreN  42164  dihglblem3N  42168  dihmeetlem2N  42172  dihglbcpreN  42173  dihmeetlem4preN  42179  dih1dimatlem0  42201  dih1dimatlem  42202  dihatlat  42207  dihatexv  42211  dihglb2  42215  dihmeet  42216  dihintcl  42217  dihmeet2  42219  doch2val2  42237  dochocss  42239  dihoml4c  42249  dochdmj1  42263  djhlj  42274  djhljjN  42275  djhjlj  42276  dihsumssj  42281  djhexmid  42284  djhlsmcl  42287  djhcvat42  42288  dihjatcclem4  42294  dihjat1lem  42301  dihsmsprn  42303  dihjat3  42305  dvh3dim2  42321  dvh3dim3N  42322  dochkr1OLDN  42352  lclkrlem2c  42382  lclkrlem2d  42383  mapdpglem23  42567  hdmap11lem2  42715  0prjspn  43474  mzpcompact2lem  43596  diophrw  43604  rexrabdioph  43635  eldioph4b  43652  pellexlem5  43674  pellfund14  43739  acongtr  43819  fnwe2lem3  43893  gicabl  43940  hbtlem2  43965  hbtlem4  43967  hbtlem5  43969  dgraalem  43986  aaitgo  44003  onexlimgt  44084  onexoegt  44085  oalim2cl  44130  cantnfresb  44165  onmcl  44172  tfsconcatfv  44182  tfsconcatrn  44183  ofoaid1  44199  ofoaid2  44200  ntrclsk13  44911  gneispb  44971  wessf1ornlem  46017  ltdiv23neg  46223  islptre  46449  limclner  46479  icccncfext  46715  stoweidlem1  46829  stoweidlem14  46842  stoweidlem24  46852  stoweidlem46  46874  stoweidlem57  46885  dirkercncflem2  46932  fourierdlem20  46955  fourierdlem41  46976  fourierdlem46  46980  fourierdlem48  46982  fourierdlem50  46984  fourierdlem62  46996  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem76  47010  fourierdlem79  47013  fourierdlem103  47037  fourierdlem104  47038  etransclem47  47109  m1modmmod  48252  iccpartiun  48334  reupr  48422  sqrtpwpw2p  48441  fmtnoprmfac1lem  48467  fmtnoprmfac2lem1  48469  lighneallem4a  48511  requad2  48539  perfectALTV  48639  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  isuspgrim0lem  48809  isuspgrim0  48810  isuspgrimlem  48811  upgrimwlklem2  48814  upgrimwlklem3  48815  upgrimtrlslem1  48820  uhgrimisgrgriclem  48846  uhgrimisgrgric  48847  clnbgrgrimlem  48849  grimgrtri  48865  gpgedgvtx1  48978  gpgedg2ov  48982  gpgedg2iv  48983  gsumlsscl  49310  lincsumcl  49361  lincscmcl  49362  isldepslvec2  49415  elbigo2  49482  relogbdivb  49492  blennnt2  49519  dignn0ldlem  49532  itsclc0yqsollem2  49693  inlinecirc02p  49717  lubeldm2  49882  glbeldm2  49883  lubsscl  49886  glbsscl  49887  isclatd  49909  sectpropdlem  49962  invpropdlem  49964  isopropdlem  49966  uptrlem1  50136  fucofulem1  50236  fullthinc  50376