Theorem syl21anc 838

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl21anc.4	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl21anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 511	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	3, 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:  bibiad  840  syl1111anc  841  rspc2dv  3637  wereu2  5682  frpomin  6361  funtpg  6621  funcnvtp  6629  funcnvqp  6630  fnund  6683  fun2d  6772  fvun1  7000  iinpreima  7089  ftpg  7176  fsnunf  7205  f1prex  7304  soisores  7347  isotr  7356  off  7715  coof  7721  caofrss  7736  caonncan  7741  fvmpocurryd  8296  oaf1o  8601  omeulem1  8620  oeordi  8625  oelimcl  8638  oeeulem  8639  oeeui  8640  oaabs2  8687  omabs  8689  coflton  8709  pmresg  8910  ralxpmap  8936  domunsncan  9112  sucdom2OLD  9122  sucdom2  9243  unxpdom2  9290  sucxpdom  9291  unblem4  9331  fodomfi  9350  fodomfiOLD  9370  hartogslem1  9582  cantnflt  9712  cantnflem3  9731  cantnflem4  9732  cnfcomlem  9739  cnfcom  9740  ttrcltr  9756  infxpenlem  10053  infxpenc  10058  fseqenlem1  10064  pwsdompw  10243  cfeq0  10296  cofsmo  10309  cfsmolem  10310  ssfin4  10350  hsmexlem4  10469  hsmexlem5  10470  axdc3lem2  10491  fpwwe2  10683  wunpr  10749  mulclpi  10933  mulcanenq  11000  distrlem4pr  11066  prlem934  11073  prlem936  11087  divge0d  13117  elfznelfzob  13812  seqcaopr2  14079  facavg  14340  swrdwrdsymb  14700  cats1un  14759  f1oun2prg  14956  sqrtdiv  15304  sqrtdivd  15462  mulcn2  15632  o1of2  15649  fsumsplit  15777  sumsplit  15804  isumless  15881  demoivreALT  16237  rpnnen2lem11  16260  gcdnncl  16544  qredeu  16695  rpdvds  16697  isprm5  16744  rpexp  16759  prmdvdsbc  16763  divnumden  16785  divdenle  16786  phimullem  16816  phisum  16828  pythagtriplem4  16857  pythagtriplem8  16861  pythagtriplem9  16862  pcgcd1  16915  sumhash  16934  fldivp1  16935  pockthlem  16943  setsfun  17208  setsfun0  17209  ssc2  17866  estrreslem1  18181  estrreslem1OLD  18182  tleile  18466  sgrppropd  18744  mndpropd  18772  grpidssd  19034  grpinvssd  19035  issubg2  19159  isnsg3  19178  eqgid  19198  kerf1ghm  19265  ghmqusnsglem1  19298  ghmquskerlem1  19301  ghmqusker  19305  gass  19319  symgextres  19443  gsmsymgreqlem2  19449  sylow1lem5  19620  sylow2alem2  19636  sylow3lem3  19647  efgredlemd  19762  efgredlem  19765  frgpnabllem1  19891  frgpnabllem2  19892  subgdmdprd  20054  ablfacrplem  20085  rglcom4d  20208  issrngd  20856  lmodprop2d  20922  lsspropd  21016  pwssplit1  21058  lspvadd  21095  rhmpreimaidl  21287  znidomb  21580  znrrg  21584  lindfind  21836  lindsind  21837  mplsubglem  22019  mplind  22094  ressply1evl  22374  mat1ghm  22489  mdetunilem1  22618  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  cramerimplem2  22690  mat2pmatlin  22741  monmatcollpw  22785  cpmadugsumlemF  22882  mretopd  23100  neiptopnei  23140  neitr  23188  ufilen  23938  flimrest  23991  flimclslem  23992  fclsrest  24032  cnextcn  24075  haustsms2  24145  tsmsxplem2  24162  trust  24238  utoptop  24243  restutop  24246  ustuqtop4  24253  utopsnneiplem  24256  utop2nei  24259  utop3cls  24260  isucn2  24288  ucncn  24294  fmucnd  24301  trcfilu  24303  comet  24526  metustexhalf  24569  metustbl  24579  psmetutop  24580  nrmmetd  24587  reconnlem1  24848  reconnlem2  24849  fsumcn  24894  cmetcaulem  25322  iscmet3lem1  25325  iscmet3lem2  25326  bcthlem5  25362  cmslsschl  25411  rrxdstprj1  25443  minveclem4  25466  ovolfiniun  25536  itg1addlem4  25734  itg1addlem5  25735  itgsplitioo  25873  c1liplem1  26035  dvfsumlem1  26066  plyeq0lem  26249  quotcan  26351  psercnlem1  26469  cxplea  26738  birthdaylem3  26996  musumsum  27235  mpodvdsmulf1o  27237  dvdsmulf1o  27239  dchrelbas4  27287  dchrhash  27315  gausslemma2dlem0d  27403  gausslemma2dlem1a  27409  2lgslem1a1  27433  2sqlem8a  27469  2sqlem8  27470  2sqcoprm  27479  2sqmod  27480  chto1ub  27520  vmadivsum  27526  dchrisumlem1  27533  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  rpvmasum2  27556  mulog2sumlem2  27579  selberg2lem  27594  pntrmax  27608  pntpbnd1  27630  pntlemb  27641  pntlemj  27647  noextend  27711  cuteq0  27877  tgjustc1  28483  tgjustc2  28484  ercgrg  28525  motcgr  28544  tglineeltr  28639  colline  28657  miriso  28678  midexlem  28700  perpneq  28722  foot  28730  f1otrg  28879  axcontlem9  28987  uspgr1ewop  29265  nbupgrres  29381  structtocusgr  29463  wlkp1  29699  clwlkl1loop  29803  uspgrn2crct  29828  crctcshwlkn0lem5  29834  3trlond  30192  3pthond  30194  3spthond  30196  frgr3v  30294  vdgn1frgrv2  30315  numclwwlk3  30404  nmblolbii  30818  minvecolem3  30895  minvecolem4  30899  htthlem  30936  bcs2  31201  nmopub2tALT  31928  nmfnleub2  31945  eighmorth  31983  nmophmi  32050  nmopcoadji  32120  hstle  32249  atcvat3i  32415  opreu2reuALT  32496  iinabrex  32582  disjxpin  32601  fmptco1f1o  32643  off2  32651  xppreima2  32661  fgreu  32682  suppovss  32690  1stpreimas  32715  padct  32731  resf1o  32741  fpwrelmap  32744  xrofsup  32771  eliccelico  32779  elicoelioo  32780  iocinif  32783  difioo  32784  elfzodif0  32796  suppssnn0  32809  hashpss  32813  2exple2exp  32834  indsupp  32852  ccatf1  32933  pfxlsw2ccat  32935  wrdt2ind  32938  ressprs  32954  chnind  33001  xrge0addgt0  33022  xrge0adddir  33023  mndlactf1o  33035  mndractf1o  33036  gsumhashmul  33064  omndmul3  33090  gsumle  33101  symgcom  33103  pmtrcnel  33109  pmtrcnel2  33110  pmtrcnelor  33111  cycpmfv2  33134  trsp2cyc  33143  cycpmco2lem7  33152  cyc3genpm  33172  cycpmconjslem2  33175  cyc3conja  33177  archirng  33195  archirngz  33196  rlocf1  33277  rrgsubm  33287  fracerl  33308  idomsubr  33311  orngmul  33333  linds2eq  33409  nsgqusf1olem3  33443  lidlunitel  33451  unitpidl1  33452  elrspunidl  33456  drngidl  33461  isprmidlc  33475  qsidomlem1  33480  qsidomlem2  33481  qsnzr  33483  mxidlirredi  33499  mxidlirred  33500  qsdrngi  33523  qsdrnglem2  33524  rprmasso  33553  1arithidomlem2  33564  1arithufdlem4  33575  zringidom  33579  deg1le0eq0  33598  ply1unit  33600  ply1dg1rt  33604  ply1dg3rt0irred  33607  m1pmeq  33608  ply1degltdimlem  33673  ply1degltdim  33674  lindsunlem  33675  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  assalactf1o  33686  ply1annprmidl  33750  minplyirredlem  33753  irngnminplynz  33755  algextdeglem4  33761  constrconj  33786  1smat1  33803  madjusmdetlem2  33827  qtophaus  33835  locfinref  33840  zarclssn  33872  zar0ring  33877  zarmxt1  33879  rhmpreimacnlem  33883  rhmpreimacn  33884  metideq  33892  sqsscirc2  33908  tpr2rico  33911  fmcncfil  33930  lmxrge0  33951  lmdvg  33952  qqhval2lem  33982  qqhf  33987  qqhnm  33991  esumle  34059  gsumesum  34060  esumlef  34063  esumrnmpt2  34069  esumpcvgval  34079  esum2d  34094  ofcf  34104  ldsysgenld  34161  ldgenpisyslem1  34164  unelros  34172  difelros  34173  inelsros  34179  diffiunisros  34180  imambfm  34264  omssubadd  34302  inelcarsg  34313  carsgsigalem  34317  carsggect  34320  carsgclctunlem2  34321  oddpwdc  34356  eulerpartlems  34362  eulerpartlemb  34370  eulerpartlemt  34373  iwrdsplit  34389  sseqf  34394  sseqfres  34395  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemfrcn0  34532  sgnsub  34547  plymulx0  34562  signsplypnf  34565  signsvtn0  34585  signstfvneq0  34587  signsvtp  34598  signsvtn  34599  fsum2dsub  34622  reprlt  34634  hashreprin  34635  reprgt  34636  reprpmtf1o  34641  chtvalz  34644  breprexplema  34645  breprexplemc  34647  breprexp  34648  circlemeth  34655  logdivsqrle  34665  hgt750lemb  34671  lpadlem3  34693  lpadleft  34698  bnj1536  34868  bnj1001  34973  bnj1280  35034  satffunlem1  35412  satffunlem2  35413  elmrsubrn  35525  neibastop3  36363  finxpsuclem  37398  poimirlem16  37643  poimirlem19  37646  poimirlem20  37647  poimirlem29  37656  mblfinlem3  37666  itg2addnclem3  37680  ftc1cnnclem  37698  lautlt  40093  lautcvr  40094  lauteq  40097  lautco  40099  ltrncl  40127  ltrncnvleN  40132  trljat2  40169  cdlemc6  40198  cdleme20c  40313  cdleme20j  40320  cdleme22e  40346  cdleme22eALTN  40347  cdlemg7aN  40627  cdlemg12e  40649  cdlemg17dALTN  40666  cdlemh  40819  cdlemkfid1N  40923  dibglbN  41168  diblss  41172  diclspsn  41196  dih1  41288  dihglbcpreN  41302  dihmeetlem4preN  41308  lcfrlem19  41563  aks4d1p8d1  42085  evlsvvval  42573  fsuppind  42600  mapfzcons  42727  mzpcl34  42742  mzpindd  42757  mzpsubst  42759  diophrw  42770  diophren  42824  irrapxlem1  42833  pellexlem5  42844  acongrep  42992  pwssplit4  43101  omlimcl2  43254  onexoegt  43256  oasubex  43299  omlim2  43312  nnoeomeqom  43325  nnawordexg  43340  succlg  43341  oacl2g  43343  onmcl  43344  omabs2  43345  omcl2  43346  tfsconcatrev  43361  ofoafg  43367  ofoaf  43368  ofoaass  43373  naddcnfass  43382  naddwordnexlem4  43414  omssrncard  43553  brtrclfv2  43740  rfovcnvf1od  44017  ntrk0kbimka  44052  isotone1  44061  isotone2  44062  4an4132  44519  modelaxrep  44998  mulltgt0  45027  fnchoice  45034  3adantlr3  45045  3adantll2  45046  3adantll3  45047  uzwo4  45058  disjf1o  45196  supxrgelem  45348  infleinflem2  45382  xrralrecnnle  45394  supxrunb3  45410  unb2ltle  45426  infrpgernmpt  45476  iooiinicc  45555  iooiinioc  45569  fmuldfeq  45598  mccl  45613  limccog  45635  limcrecl  45644  lptioo1  45647  islpcn  45654  limsupre  45656  neglimc  45662  0ellimcdiv  45664  limclner  45666  climleltrp  45691  climinf3  45731  liminflimsupclim  45822  xlimpnfxnegmnf  45829  icccncfext  45902  fprodcncf  45915  dvnmptdivc  45953  dvnmul  45958  dvmptfprod  45960  dvnprodlem3  45963  stoweidlem25  46040  stoweidlem34  46049  stoweidlem38  46053  stoweidlem44  46059  stoweidlem48  46063  stoweidlem49  46064  stoweidlem59  46074  stoweidlem60  46075  wallispilem4  46083  stirlinglem5  46093  dirkercncflem2  46119  fourierdlem39  46161  fourierdlem42  46164  fourierdlem46  46167  fourierdlem47  46168  fourierdlem48  46169  fourierdlem50  46171  fourierdlem51  46172  fourierdlem64  46185  fourierdlem73  46194  fourierdlem74  46195  fourierdlem77  46198  fourierdlem80  46201  fourierdlem87  46208  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  etransclem32  46281  rrxsnicc  46315  sge0cl  46396  sge0f1o  46397  nnfoctbdjlem  46470  ismeannd  46482  omeiunltfirp  46534  hoicvr  46563  ovncvrrp  46579  hoidmvlelem2  46611  hoidmvlelem5  46614  hspdifhsp  46631  hoiqssbllem2  46638  hspmbllem2  46642  vonicclem2  46699  smflimsuplem7  46841  fundcmpsurbijinj  47397  sqrtpwpw2p  47525  lincresunit2  48395  nnpw2pmod  48504  dignn0flhalflem1  48536  dignn0flhalf  48539  rrx2linest  48663  itsclc0yqsol  48685  itsclc0b  48693  brab2dd  48741  oppcendc  48906  oppcthinendcALT  49090  functhinclem1  49093  functhinclem2  49094  fullthinc2  49100