Theorem syl21anc 837

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl1111anc  839  wereu2  5522  funtpg  6391  funcnvtp  6399  funcnvqp  6400  fnund  6447  fun2d  6528  fvun1  6744  iinpreima  6829  ftpg  6910  fsnunf  6939  f1prex  7033  soisores  7075  isotr  7084  off  7423  caofrss  7441  caonncan  7446  fvmpocurryd  7948  oaf1o  8200  omeulem1  8219  oeordi  8224  oelimcl  8237  oeeulem  8238  oeeui  8239  oaabs2  8283  omabs  8285  pmresg  8453  ralxpmap  8479  domunsncan  8639  sucdom2  8649  unxpdom2  8765  sucxpdom  8766  unblem4  8807  fodomfi  8831  hartogslem1  9040  cantnflt  9169  cantnflem3  9188  cantnflem4  9189  cnfcomlem  9196  cnfcom  9197  infxpenlem  9474  infxpenc  9479  fseqenlem1  9485  pwsdompw  9665  cfeq0  9717  cofsmo  9730  cfsmolem  9731  ssfin4  9771  hsmexlem4  9890  hsmexlem5  9891  axdc3lem2  9912  fpwwe2  10104  wunpr  10170  mulclpi  10354  mulcanenq  10421  distrlem4pr  10487  prlem934  10494  prlem936  10508  divge0d  12513  elfznelfzob  13193  seqcaopr2  13457  facavg  13712  swrdwrdsymb  14072  cats1un  14131  f1oun2prg  14327  sqrtdiv  14674  sqrtdivd  14832  mulcn2  15001  o1of2  15018  fsumsplit  15146  sumsplit  15172  isumless  15249  demoivreALT  15603  rpnnen2lem11  15626  gcdnncl  15907  qredeu  16055  rpdvds  16057  isprm5  16104  rpexp  16119  divnumden  16144  divdenle  16145  phimullem  16172  phisum  16183  pythagtriplem4  16212  pythagtriplem8  16216  pythagtriplem9  16217  pcgcd1  16269  sumhash  16288  fldivp1  16289  pockthlem  16297  setsfun  16577  setsfun0  16578  ssc2  17152  estrreslem1  17454  mndpropd  18003  grpidssd  18243  grpinvssd  18244  issubg2  18362  isnsg3  18380  eqgid  18400  gass  18499  symgextres  18621  gsmsymgreqlem2  18627  sylow1lem5  18795  sylow2alem2  18811  sylow3lem3  18822  efgredlemd  18938  efgredlem  18941  frgpnabllem1  19062  frgpnabllem2  19063  subgdmdprd  19225  ablfacrplem  19256  kerf1ghm  19567  issrngd  19701  lmodprop2d  19765  lsspropd  19858  pwssplit1  19900  lspvadd  19937  znidomb  20330  znrrg  20334  lindfind  20582  lindsind  20583  mplsubglem  20765  mplind  20832  mat1ghm  21184  mdetunilem1  21313  mdetunilem3  21315  mdetunilem4  21316  mdetunilem9  21321  cramerimplem2  21385  mat2pmatlin  21436  monmatcollpw  21480  cpmadugsumlemF  21577  mretopd  21793  neiptopnei  21833  neitr  21881  ufilen  22631  flimrest  22684  flimclslem  22685  fclsrest  22725  cnextcn  22768  haustsms2  22838  tsmsxplem2  22855  trust  22931  utoptop  22936  restutop  22939  ustuqtop4  22946  utopsnneiplem  22949  utop2nei  22952  utop3cls  22953  isucn2  22981  ucncn  22987  fmucnd  22994  trcfilu  22996  comet  23216  metustexhalf  23259  metustbl  23269  psmetutop  23270  nrmmetd  23277  reconnlem1  23528  reconnlem2  23529  fsumcn  23572  cmetcaulem  23989  iscmet3lem1  23992  iscmet3lem2  23993  bcthlem5  24029  cmslsschl  24078  rrxdstprj1  24110  minveclem4  24133  ovolfiniun  24202  itg1addlem4  24400  itg1addlem5  24401  itgsplitioo  24538  c1liplem1  24696  dvfsumlem1  24726  plyeq0lem  24907  quotcan  25005  psercnlem1  25120  cxplea  25387  birthdaylem3  25639  musumsum  25877  dvdsmulf1o  25879  dchrelbas4  25927  dchrhash  25955  gausslemma2dlem0d  26043  gausslemma2dlem1a  26049  2lgslem1a1  26073  2sqlem8a  26109  2sqlem8  26110  2sqcoprm  26119  2sqmod  26120  chto1ub  26160  vmadivsum  26166  dchrisumlem1  26173  dchrvmasumlem2  26182  dchrvmasumiflem1  26185  rpvmasum2  26196  mulog2sumlem2  26219  selberg2lem  26234  pntrmax  26248  pntpbnd1  26270  pntlemb  26281  pntlemj  26287  tgjustc1  26369  tgjustc2  26370  ercgrg  26411  motcgr  26430  tglineeltr  26525  colline  26543  miriso  26564  midexlem  26586  perpneq  26608  foot  26616  f1otrg  26765  axcontlem9  26866  uspgr1ewop  27138  nbupgrres  27254  structtocusgr  27336  wlkp1  27571  clwlkl1loop  27672  uspgrn2crct  27694  crctcshwlkn0lem5  27700  3trlond  28058  3pthond  28060  3spthond  28062  frgr3v  28160  vdgn1frgrv2  28181  numclwwlk3  28270  nmblolbii  28682  minvecolem3  28759  minvecolem4  28763  htthlem  28800  bcs2  29065  nmopub2tALT  29792  nmfnleub2  29809  eighmorth  29847  nmophmi  29914  nmopcoadji  29984  hstle  30113  atcvat3i  30279  opreu2reuALT  30347  iinabrex  30431  disjxpin  30450  fmptco1f1o  30491  off2  30501  xppreima2  30512  fgreu  30534  suppovss  30542  1stpreimas  30563  padct  30579  resf1o  30590  fpwrelmap  30593  xrofsup  30615  eliccelico  30623  elicoelioo  30624  iocinif  30627  difioo  30628  prmdvdsbc  30655  ccatf1  30748  pfxlsw2ccat  30749  wrdt2ind  30750  ressprs  30765  tleile  30771  xrge0addgt0  30827  xrge0adddir  30828  gsumhashmul  30843  omndmul3  30866  gsumle  30877  symgcom  30879  pmtrcnel  30885  pmtrcnel2  30886  pmtrcnelor  30887  cycpmfv2  30908  trsp2cyc  30917  cycpmco2lem7  30926  cyc3genpm  30946  cycpmconjslem2  30949  cyc3conja  30951  archirng  30969  archirngz  30970  orngmul  31029  linds2eq  31097  nsgqusf1olem3  31122  rhmpreimaidl  31125  elrspunidl  31128  isprmidlc  31145  qsidomlem1  31150  qsidomlem2  31151  lindsunlem  31227  lbsdiflsp0  31229  fedgmullem1  31232  fedgmullem2  31233  1smat1  31276  madjusmdetlem2  31300  qtophaus  31308  locfinref  31313  zarclssn  31345  zar0ring  31350  zarmxt1  31352  rhmpreimacnlem  31356  rhmpreimacn  31357  metideq  31365  sqsscirc2  31381  tpr2rico  31384  fmcncfil  31403  lmxrge0  31424  lmdvg  31425  qqhval2lem  31451  qqhf  31456  qqhnm  31460  esumle  31546  gsumesum  31547  esumlef  31550  esumrnmpt2  31556  esumpcvgval  31566  esum2d  31581  ofcf  31591  ldsysgenld  31648  ldgenpisyslem1  31651  unelros  31659  difelros  31660  inelsros  31666  diffiunisros  31667  imambfm  31749  omssubadd  31787  inelcarsg  31798  carsgsigalem  31802  carsggect  31805  carsgclctunlem2  31806  oddpwdc  31841  eulerpartlems  31847  eulerpartlemb  31855  eulerpartlemt  31858  iwrdsplit  31874  sseqf  31879  sseqfres  31880  ballotlemfc0  31979  ballotlemfcc  31980  ballotlemfrcn0  32016  sgnsub  32031  plymulx0  32046  signsplypnf  32049  signsvtn0  32069  signstfvneq0  32071  signsvtp  32082  signsvtn  32083  fsum2dsub  32107  reprlt  32119  hashreprin  32120  reprgt  32121  reprpmtf1o  32126  chtvalz  32129  breprexplema  32130  breprexplemc  32132  breprexp  32133  circlemeth  32140  logdivsqrle  32150  hgt750lemb  32156  lpadlem3  32178  lpadleft  32183  bnj1536  32355  bnj1001  32460  bnj1280  32521  cvxsconn  32722  satffunlem1  32886  satffunlem2  32887  elmrsubrn  32999  frpomin  33326  noextend  33435  neibastop3  34101  finxpsuclem  35095  poimirlem16  35354  poimirlem19  35357  poimirlem20  35358  poimirlem29  35367  mblfinlem3  35377  itg2addnclem3  35391  ftc1cnnclem  35409  lautlt  37668  lautcvr  37669  lauteq  37672  lautco  37674  ltrncl  37702  ltrncnvleN  37707  trljat2  37744  cdlemc6  37773  cdleme20c  37888  cdleme20j  37895  cdleme22e  37921  cdleme22eALTN  37922  cdlemg7aN  38202  cdlemg12e  38224  cdlemg17dALTN  38241  cdlemh  38394  cdlemkfid1N  38498  dibglbN  38743  diblss  38747  diclspsn  38771  dih1  38863  dihglbcpreN  38877  dihmeetlem4preN  38883  lcfrlem19  39138  fsuppind  39785  mapfzcons  40031  mzpcl34  40046  mzpindd  40061  mzpsubst  40063  diophrw  40074  diophren  40128  irrapxlem1  40137  pellexlem5  40148  acongrep  40295  pwssplit4  40407  brtrclfv2  40802  rfovcnvf1od  41079  ntrk0kbimka  41116  isotone1  41125  isotone2  41126  4an4132  41579  mulltgt0  42025  fnchoice  42032  3adantlr3  42044  3adantll2  42046  3adantll3  42047  uzwo4  42061  disjf1o  42189  supxrgelem  42338  infleinflem2  42372  xrralrecnnle  42386  supxrunb3  42403  unb2ltle  42419  infrpgernmpt  42471  iooiinicc  42546  iooiinioc  42560  fmuldfeq  42592  mccl  42607  limccog  42629  limcrecl  42638  lptioo1  42641  islpcn  42648  limsupre  42650  neglimc  42656  0ellimcdiv  42658  limclner  42660  climleltrp  42685  climinf3  42725  liminflimsupclim  42816  xlimpnfxnegmnf  42823  icccncfext  42896  fprodcncf  42909  dvnmptdivc  42947  dvnmul  42952  dvmptfprod  42954  dvnprodlem3  42957  stoweidlem25  43034  stoweidlem34  43043  stoweidlem38  43047  stoweidlem44  43053  stoweidlem48  43057  stoweidlem49  43058  stoweidlem59  43068  stoweidlem60  43069  wallispilem4  43077  stirlinglem5  43087  dirkercncflem2  43113  fourierdlem39  43155  fourierdlem42  43158  fourierdlem46  43161  fourierdlem47  43162  fourierdlem48  43163  fourierdlem50  43165  fourierdlem51  43166  fourierdlem64  43179  fourierdlem73  43188  fourierdlem74  43189  fourierdlem77  43192  fourierdlem80  43195  fourierdlem87  43202  fourierdlem94  43209  fourierdlem103  43218  fourierdlem104  43219  etransclem32  43275  rrxsnicc  43309  sge0cl  43387  sge0f1o  43388  nnfoctbdjlem  43461  ismeannd  43473  omeiunltfirp  43525  hoicvr  43554  ovncvrrp  43570  hoidmvlelem2  43602  hoidmvlelem5  43605  hspdifhsp  43622  hoiqssbllem2  43629  hspmbllem2  43633  vonicclem2  43690  smflimsuplem7  43824  fundcmpsurbijinj  44296  sqrtpwpw2p  44424  isomgrref  44721  lincresunit2  45253  nnpw2pmod  45363  dignn0flhalflem1  45395  dignn0flhalf  45398  rrx2linest  45522  itsclc0yqsol  45544  itsclc0b  45552