Theorem syl21anc 835

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  syl1111anc  837  wereu2  5551  funtpg  6408  funcnvtp  6416  funcnvqp  6417  fnunsn  6463  fun2d  6541  fvun1  6753  iinpreima  6836  ftpg  6917  fsnunf  6946  f1prex  7039  soisores  7079  isotr  7088  off  7423  caofrss  7441  caonncan  7446  fvmpocurryd  7936  oaf1o  8188  omeulem1  8207  oeordi  8212  oelimcl  8225  oeeulem  8226  oeeui  8227  oaabs2  8271  omabs  8273  pmresg  8433  ralxpmap  8459  domunsncan  8616  sucdom2  8713  unxpdom2  8725  sucxpdom  8726  unblem4  8772  fodomfi  8796  hartogslem1  9005  brwdom2  9036  cantnflt  9134  cantnflem3  9153  cantnflem4  9154  cnfcomlem  9161  cnfcom  9162  infxpenlem  9438  infxpenc  9443  fseqenlem1  9449  pwsdompw  9625  cfeq0  9677  cofsmo  9690  cfsmolem  9691  ssfin4  9731  hsmexlem4  9850  hsmexlem5  9851  axdc3lem2  9872  fpwwe2  10064  wunpr  10130  mulclpi  10314  mulcanenq  10381  distrlem4pr  10447  prlem934  10454  prlem936  10468  divge0d  12470  elfznelfzob  13142  seqcaopr2  13405  facavg  13660  swrdwrdsymb  14023  cats1un  14082  f1oun2prg  14278  sqrtdiv  14624  sqrtdivd  14782  mulcn2  14951  o1of2  14968  fsumsplit  15096  sumsplit  15122  isumless  15199  demoivreALT  15553  rpnnen2lem11  15576  gcdnncl  15855  qredeu  16001  rpdvds  16003  isprm5  16050  rpexp  16063  divnumden  16087  divdenle  16088  phimullem  16115  phisum  16126  pythagtriplem4  16155  pythagtriplem8  16159  pythagtriplem9  16160  pcgcd1  16212  sumhash  16231  fldivp1  16232  pockthlem  16240  setsfun  16517  setsfun0  16518  ssc2  17091  estrreslem1  17386  mndpropd  17935  grpidssd  18174  grpinvssd  18175  issubg2  18293  isnsg3  18311  eqgid  18331  gass  18430  symgextres  18552  gsmsymgreqlem2  18558  sylow1lem5  18726  sylow2alem2  18742  sylow3lem3  18753  efgredlemd  18869  efgredlem  18872  frgpnabllem1  18992  frgpnabllem2  18993  subgdmdprd  19155  ablfacrplem  19186  kerf1ghm  19496  kerf1hrmOLD  19497  issrngd  19631  lmodprop2d  19695  lsspropd  19788  pwssplit1  19830  lspvadd  19867  mplsubglem  20213  mplind  20281  znidomb  20707  znrrg  20711  lindfind  20959  lindsind  20960  mat1ghm  21091  mdetunilem1  21220  mdetunilem3  21222  mdetunilem4  21223  mdetunilem9  21228  cramerimplem2  21292  mat2pmatlin  21342  monmatcollpw  21386  cpmadugsumlemF  21483  mretopd  21699  neiptopnei  21739  neitr  21787  ufilen  22537  flimrest  22590  flimclslem  22591  fclsrest  22631  cnextcn  22674  haustsms2  22744  tsmsxplem2  22761  trust  22837  utoptop  22842  restutop  22845  ustuqtop4  22852  utopsnneiplem  22855  utop2nei  22858  utop3cls  22859  isucn2  22887  ucncn  22893  fmucnd  22900  trcfilu  22902  comet  23122  metustexhalf  23165  metustbl  23175  psmetutop  23176  nrmmetd  23183  reconnlem1  23433  reconnlem2  23434  fsumcn  23477  cmetcaulem  23890  iscmet3lem1  23893  iscmet3lem2  23894  bcthlem5  23930  cmslsschl  23979  rrxdstprj1  24011  minveclem4  24034  ovolfiniun  24101  itg1addlem4  24299  itg1addlem5  24300  itgsplitioo  24437  c1liplem1  24592  dvfsumlem1  24622  plyeq0lem  24799  quotcan  24897  psercnlem1  25012  cxplea  25278  birthdaylem3  25530  musumsum  25768  dvdsmulf1o  25770  dchrelbas4  25818  dchrhash  25846  gausslemma2dlem0d  25934  gausslemma2dlem1a  25940  2lgslem1a1  25964  2sqlem8a  26000  2sqlem8  26001  2sqcoprm  26010  2sqmod  26011  chto1ub  26051  vmadivsum  26057  dchrisumlem1  26064  dchrvmasumlem2  26073  dchrvmasumiflem1  26076  rpvmasum2  26087  mulog2sumlem2  26110  selberg2lem  26125  pntrmax  26139  pntpbnd1  26161  pntlemb  26172  pntlemj  26178  tgjustc1  26260  tgjustc2  26261  ercgrg  26302  motcgr  26321  tglineeltr  26416  colline  26434  miriso  26455  midexlem  26477  perpneq  26499  foot  26507  f1otrg  26656  axcontlem9  26757  uspgr1ewop  27029  nbupgrres  27145  structtocusgr  27227  wlkp1  27462  clwlkl1loop  27563  uspgrn2crct  27585  crctcshwlkn0lem5  27591  3trlond  27951  3pthond  27953  3spthond  27955  frgr3v  28053  vdgn1frgrv2  28074  numclwwlk3  28163  nmblolbii  28575  minvecolem3  28652  minvecolem4  28656  htthlem  28693  bcs2  28958  nmopub2tALT  29685  nmfnleub2  29702  eighmorth  29740  nmophmi  29807  nmopcoadji  29877  hstle  30006  atcvat3i  30172  opreu2reuALT  30239  disjxpin  30337  fmptco1f1o  30377  off2  30387  xppreima2  30394  fgreu  30416  suppovss  30425  1stpreimas  30440  padct  30454  resf1o  30465  fpwrelmap  30468  xrofsup  30491  eliccelico  30499  elicoelioo  30500  iocinif  30503  difioo  30504  prmdvdsbc  30531  ccatf1  30625  pfxlsw2ccat  30626  wrdt2ind  30627  ressprs  30642  tleile  30648  xrge0addgt0  30678  xrge0adddir  30679  omndmul3  30714  gsumle  30725  symgcom  30727  pmtrcnel  30733  pmtrcnel2  30734  pmtrcnelor  30735  cycpmfv2  30756  trsp2cyc  30765  cycpmco2lem7  30774  cyc3genpm  30794  cycpmconjslem2  30797  cyc3conja  30799  archirng  30817  archirngz  30818  orngmul  30876  linds2eq  30941  isprmidlc  30963  qsidomlem1  30965  qsidomlem2  30966  lindsunlem  31020  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  1smat1  31069  madjusmdetlem2  31093  qtophaus  31100  locfinref  31105  metideq  31133  sqsscirc2  31152  tpr2rico  31155  fmcncfil  31174  lmxrge0  31195  lmdvg  31196  qqhval2lem  31222  qqhf  31227  qqhnm  31231  esumle  31317  gsumesum  31318  esumlef  31321  esumrnmpt2  31327  esumpcvgval  31337  esum2d  31352  ofcf  31362  ldsysgenld  31419  ldgenpisyslem1  31422  unelros  31430  difelros  31431  inelsros  31437  diffiunisros  31438  imambfm  31520  omssubadd  31558  inelcarsg  31569  carsgsigalem  31573  carsggect  31576  carsgclctunlem2  31577  oddpwdc  31612  eulerpartlems  31618  eulerpartlemb  31626  eulerpartlemt  31629  iwrdsplit  31645  sseqfn  31648  sseqf  31650  sseqfres  31651  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemfrcn0  31787  sgnsub  31802  plymulx0  31817  signsplypnf  31820  signsvtn0  31840  signstfvneq0  31842  signsvtp  31853  signsvtn  31854  fsum2dsub  31878  reprlt  31890  hashreprin  31891  reprgt  31892  reprpmtf1o  31897  chtvalz  31900  breprexplema  31901  breprexplemc  31903  breprexp  31904  circlemeth  31911  logdivsqrle  31921  hgt750lemb  31927  lpadlem3  31949  lpadleft  31954  bnj927  32040  bnj1536  32126  bnj1001  32231  bnj1280  32292  cvxsconn  32490  satffunlem1  32654  satffunlem2  32655  elmrsubrn  32767  frpomin  33078  noextend  33173  neibastop3  33710  finxpsuclem  34677  poimirlem16  34907  poimirlem19  34910  poimirlem20  34911  poimirlem29  34920  mblfinlem3  34930  itg2addnclem3  34944  ftc1cnnclem  34964  lautlt  37226  lautcvr  37227  lauteq  37230  lautco  37232  ltrncl  37260  ltrncnvleN  37265  trljat2  37302  cdlemc6  37331  cdleme20c  37446  cdleme20j  37453  cdleme22e  37479  cdleme22eALTN  37480  cdlemg7aN  37760  cdlemg12e  37782  cdlemg17dALTN  37799  cdlemh  37952  cdlemkfid1N  38056  dibglbN  38301  diblss  38305  diclspsn  38329  dih1  38421  dihglbcpreN  38435  dihmeetlem4preN  38441  lcfrlem19  38696  mapfzcons  39311  mzpcl34  39326  mzpindd  39341  mzpsubst  39343  diophrw  39354  diophren  39408  irrapxlem1  39417  pellexlem5  39428  acongrep  39575  pwssplit4  39687  brtrclfv2  40070  rfovcnvf1od  40348  ntrk0kbimka  40387  isotone1  40396  isotone2  40397  4an4132  40831  mulltgt0  41277  fnchoice  41284  3adantlr3  41296  3adantll2  41298  3adantll3  41299  uzwo4  41313  disjf1o  41450  supxrgelem  41603  infleinflem2  41637  xrralrecnnle  41651  supxrunb3  41670  unb2ltle  41687  infrpgernmpt  41739  iooiinicc  41816  iooiinioc  41830  fmuldfeq  41862  mccl  41877  limccog  41899  limcrecl  41908  lptioo1  41911  islpcn  41918  limsupre  41920  neglimc  41926  0ellimcdiv  41928  limclner  41930  climleltrp  41955  climinf3  41995  liminflimsupclim  42086  xlimpnfxnegmnf  42093  icccncfext  42168  fprodcncf  42182  dvnmptdivc  42221  dvnmul  42226  dvmptfprod  42228  dvnprodlem3  42231  stoweidlem25  42309  stoweidlem34  42318  stoweidlem38  42322  stoweidlem44  42328  stoweidlem48  42332  stoweidlem49  42333  stoweidlem59  42343  stoweidlem60  42344  wallispilem4  42352  stirlinglem5  42362  dirkercncflem2  42388  fourierdlem39  42430  fourierdlem42  42433  fourierdlem46  42436  fourierdlem47  42437  fourierdlem48  42438  fourierdlem50  42440  fourierdlem51  42441  fourierdlem64  42454  fourierdlem73  42463  fourierdlem74  42464  fourierdlem77  42467  fourierdlem80  42470  fourierdlem87  42477  fourierdlem94  42484  fourierdlem103  42493  fourierdlem104  42494  etransclem32  42550  rrxsnicc  42584  sge0cl  42662  sge0f1o  42663  nnfoctbdjlem  42736  ismeannd  42748  omeiunltfirp  42800  hoicvr  42829  ovncvrrp  42845  hoidmvlelem2  42877  hoidmvlelem5  42880  hspdifhsp  42897  hoiqssbllem2  42904  hspmbllem2  42908  vonicclem2  42965  smflimsuplem7  43099  fundcmpsurbijinj  43569  sqrtpwpw2p  43699  isomgrref  43999  lincresunit2  44532  nnpw2pmod  44642  dignn0flhalflem1  44674  dignn0flhalf  44677  rrx2linest  44728  itsclc0yqsol  44750  itsclc0b  44758