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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  syl1111anc  839  rspc2dv  3624  wereu2  5671  frpomin  6337  funtpg  6599  funcnvtp  6607  funcnvqp  6608  fnund  6660  fun2d  6751  fvun1  6977  iinpreima  7065  ftpg  7148  fsnunf  7177  f1prex  7276  soisores  7318  isotr  7327  off  7682  caofrss  7700  caonncan  7705  fvmpocurryd  8250  oaf1o  8558  omeulem1  8577  oeordi  8582  oelimcl  8595  oeeulem  8596  oeeui  8597  oaabs2  8643  omabs  8645  coflton  8665  pmresg  8859  ralxpmap  8885  domunsncan  9067  sucdom2OLD  9077  sucdom2  9201  unxpdom2  9249  sucxpdom  9250  unblem4  9293  fodomfi  9320  hartogslem1  9532  cantnflt  9662  cantnflem3  9681  cantnflem4  9682  cnfcomlem  9689  cnfcom  9690  ttrcltr  9706  infxpenlem  10003  infxpenc  10008  fseqenlem1  10014  pwsdompw  10194  cfeq0  10246  cofsmo  10259  cfsmolem  10260  ssfin4  10300  hsmexlem4  10419  hsmexlem5  10420  axdc3lem2  10441  fpwwe2  10633  wunpr  10699  mulclpi  10883  mulcanenq  10950  distrlem4pr  11016  prlem934  11023  prlem936  11037  divge0d  13051  elfznelfzob  13733  seqcaopr2  13999  facavg  14256  swrdwrdsymb  14607  cats1un  14666  f1oun2prg  14863  sqrtdiv  15207  sqrtdivd  15365  mulcn2  15535  o1of2  15552  fsumsplit  15682  sumsplit  15709  isumless  15786  demoivreALT  16139  rpnnen2lem11  16162  gcdnncl  16443  qredeu  16590  rpdvds  16592  isprm5  16639  rpexp  16654  divnumden  16679  divdenle  16680  phimullem  16707  phisum  16718  pythagtriplem4  16747  pythagtriplem8  16751  pythagtriplem9  16752  pcgcd1  16805  sumhash  16824  fldivp1  16825  pockthlem  16833  setsfun  17099  setsfun0  17100  ssc2  17764  estrreslem1  18083  estrreslem1OLD  18084  tleile  18369  sgrppropd  18617  mndpropd  18645  grpidssd  18894  grpinvssd  18895  issubg2  19014  isnsg3  19033  eqgid  19053  gass  19158  symgextres  19285  gsmsymgreqlem2  19291  sylow1lem5  19462  sylow2alem2  19478  sylow3lem3  19489  efgredlemd  19604  efgredlem  19607  frgpnabllem1  19732  frgpnabllem2  19733  subgdmdprd  19895  ablfacrplem  19926  rglcom4d  20024  kerf1ghm  20270  issrngd  20456  lmodprop2d  20521  lsspropd  20615  pwssplit1  20657  lspvadd  20694  znidomb  21100  znrrg  21104  lindfind  21354  lindsind  21355  mplsubglem  21539  mplind  21612  mat1ghm  21966  mdetunilem1  22095  mdetunilem3  22097  mdetunilem4  22098  mdetunilem9  22103  cramerimplem2  22167  mat2pmatlin  22218  monmatcollpw  22262  cpmadugsumlemF  22359  mretopd  22577  neiptopnei  22617  neitr  22665  ufilen  23415  flimrest  23468  flimclslem  23469  fclsrest  23509  cnextcn  23552  haustsms2  23622  tsmsxplem2  23639  trust  23715  utoptop  23720  restutop  23723  ustuqtop4  23730  utopsnneiplem  23733  utop2nei  23736  utop3cls  23737  isucn2  23765  ucncn  23771  fmucnd  23778  trcfilu  23780  comet  24003  metustexhalf  24046  metustbl  24056  psmetutop  24057  nrmmetd  24064  reconnlem1  24323  reconnlem2  24324  fsumcn  24367  cmetcaulem  24786  iscmet3lem1  24789  iscmet3lem2  24790  bcthlem5  24826  cmslsschl  24875  rrxdstprj1  24907  minveclem4  24930  ovolfiniun  24999  itg1addlem4  25197  itg1addlem4OLD  25198  itg1addlem5  25199  itgsplitioo  25336  c1liplem1  25494  dvfsumlem1  25524  plyeq0lem  25705  quotcan  25803  psercnlem1  25918  cxplea  26185  birthdaylem3  26437  musumsum  26675  dvdsmulf1o  26677  dchrelbas4  26725  dchrhash  26753  gausslemma2dlem0d  26841  gausslemma2dlem1a  26847  2lgslem1a1  26871  2sqlem8a  26907  2sqlem8  26908  2sqcoprm  26917  2sqmod  26918  chto1ub  26958  vmadivsum  26964  dchrisumlem1  26971  dchrvmasumlem2  26980  dchrvmasumiflem1  26983  rpvmasum2  26994  mulog2sumlem2  27017  selberg2lem  27032  pntrmax  27046  pntpbnd1  27068  pntlemb  27079  pntlemj  27085  noextend  27148  cuteq0  27312  tgjustc1  27705  tgjustc2  27706  ercgrg  27747  motcgr  27766  tglineeltr  27861  colline  27879  miriso  27900  midexlem  27922  perpneq  27944  foot  27952  f1otrg  28101  axcontlem9  28209  uspgr1ewop  28484  nbupgrres  28600  structtocusgr  28682  wlkp1  28917  clwlkl1loop  29019  uspgrn2crct  29041  crctcshwlkn0lem5  29047  3trlond  29405  3pthond  29407  3spthond  29409  frgr3v  29507  vdgn1frgrv2  29528  numclwwlk3  29617  nmblolbii  30029  minvecolem3  30106  minvecolem4  30110  htthlem  30147  bcs2  30412  nmopub2tALT  31139  nmfnleub2  31156  eighmorth  31194  nmophmi  31261  nmopcoadji  31331  hstle  31460  atcvat3i  31626  opreu2reuALT  31694  iinabrex  31777  disjxpin  31796  fmptco1f1o  31834  off2  31843  xppreima2  31853  fgreu  31874  suppovss  31883  1stpreimas  31904  padct  31921  resf1o  31932  fpwrelmap  31935  xrofsup  31957  eliccelico  31965  elicoelioo  31966  iocinif  31969  difioo  31970  suppssnn0  31994  prmdvdsbc  31999  ccatf1  32092  pfxlsw2ccat  32093  wrdt2ind  32094  ressprs  32110  xrge0addgt0  32169  xrge0adddir  32170  gsumhashmul  32185  omndmul3  32208  gsumle  32219  symgcom  32221  pmtrcnel  32227  pmtrcnel2  32228  pmtrcnelor  32229  cycpmfv2  32250  trsp2cyc  32259  cycpmco2lem7  32268  cyc3genpm  32288  cycpmconjslem2  32291  cyc3conja  32293  archirng  32311  archirngz  32312  orngmul  32389  linds2eq  32461  nsgqusf1olem3  32488  ghmquskerlem1  32490  ghmqusker  32493  rhmpreimaidl  32498  elrspunidl  32503  drngidl  32508  isprmidlc  32523  qsidomlem1  32528  qsidomlem2  32529  qsnzr  32531  qsdrngi  32561  qsdrnglem2  32562  ressply1evl  32596  ply1degltdimlem  32651  ply1degltdim  32652  lindsunlem  32653  lbsdiflsp0  32655  fedgmullem1  32658  fedgmullem2  32659  ply1annprmidl  32709  1smat1  32721  madjusmdetlem2  32745  qtophaus  32753  locfinref  32758  zarclssn  32790  zar0ring  32795  zarmxt1  32797  rhmpreimacnlem  32801  rhmpreimacn  32802  metideq  32810  sqsscirc2  32826  tpr2rico  32829  fmcncfil  32848  lmxrge0  32869  lmdvg  32870  qqhval2lem  32898  qqhf  32903  qqhnm  32907  esumle  32993  gsumesum  32994  esumlef  32997  esumrnmpt2  33003  esumpcvgval  33013  esum2d  33028  ofcf  33038  ldsysgenld  33095  ldgenpisyslem1  33098  unelros  33106  difelros  33107  inelsros  33113  diffiunisros  33114  imambfm  33198  omssubadd  33236  inelcarsg  33247  carsgsigalem  33251  carsggect  33254  carsgclctunlem2  33255  oddpwdc  33290  eulerpartlems  33296  eulerpartlemb  33304  eulerpartlemt  33307  iwrdsplit  33323  sseqf  33328  sseqfres  33329  ballotlemfc0  33428  ballotlemfcc  33429  ballotlemfrcn0  33465  sgnsub  33480  plymulx0  33495  signsplypnf  33498  signsvtn0  33518  signstfvneq0  33520  signsvtp  33531  signsvtn  33532  fsum2dsub  33556  reprlt  33568  hashreprin  33569  reprgt  33570  reprpmtf1o  33575  chtvalz  33578  breprexplema  33579  breprexplemc  33581  breprexp  33582  circlemeth  33589  logdivsqrle  33599  hgt750lemb  33605  lpadlem3  33627  lpadleft  33632  bnj1536  33802  bnj1001  33907  bnj1280  33968  cvxsconn  34171  satffunlem1  34335  satffunlem2  34336  elmrsubrn  34448  neibastop3  35184  finxpsuclem  36215  poimirlem16  36441  poimirlem19  36444  poimirlem20  36445  poimirlem29  36454  mblfinlem3  36464  itg2addnclem3  36478  ftc1cnnclem  36496  lautlt  38899  lautcvr  38900  lauteq  38903  lautco  38905  ltrncl  38933  ltrncnvleN  38938  trljat2  38975  cdlemc6  39004  cdleme20c  39119  cdleme20j  39126  cdleme22e  39152  cdleme22eALTN  39153  cdlemg7aN  39433  cdlemg12e  39455  cdlemg17dALTN  39472  cdlemh  39625  cdlemkfid1N  39729  dibglbN  39974  diblss  39978  diclspsn  40002  dih1  40094  dihglbcpreN  40108  dihmeetlem4preN  40114  lcfrlem19  40369  aks4d1p8d1  40886  evlsvvval  41084  fsuppind  41111  mapfzcons  41386  mzpcl34  41401  mzpindd  41416  mzpsubst  41418  diophrw  41429  diophren  41483  irrapxlem1  41492  pellexlem5  41503  acongrep  41651  pwssplit4  41763  omlimcl2  41923  onexoegt  41925  oasubex  41968  omlim2  41981  nnoeomeqom  41994  nnawordexg  42009  succlg  42010  oacl2g  42012  onmcl  42013  omabs2  42014  omcl2  42015  tfsconcatrev  42030  ofoafg  42036  ofoaf  42037  ofoaass  42042  naddcnfass  42051  naddwordnexlem4  42084  omssrncard  42223  brtrclfv2  42410  rfovcnvf1od  42687  ntrk0kbimka  42722  isotone1  42731  isotone2  42732  4an4132  43192  mulltgt0  43638  fnchoice  43645  3adantlr3  43656  3adantll2  43657  3adantll3  43658  uzwo4  43672  disjf1o  43821  supxrgelem  43981  infleinflem2  44015  xrralrecnnle  44027  supxrunb3  44043  unb2ltle  44059  infrpgernmpt  44109  iooiinicc  44189  iooiinioc  44203  fmuldfeq  44233  mccl  44248  limccog  44270  limcrecl  44279  lptioo1  44282  islpcn  44289  limsupre  44291  neglimc  44297  0ellimcdiv  44299  limclner  44301  climleltrp  44326  climinf3  44366  liminflimsupclim  44457  xlimpnfxnegmnf  44464  icccncfext  44537  fprodcncf  44550  dvnmptdivc  44588  dvnmul  44593  dvmptfprod  44595  dvnprodlem3  44598  stoweidlem25  44675  stoweidlem34  44684  stoweidlem38  44688  stoweidlem44  44694  stoweidlem48  44698  stoweidlem49  44699  stoweidlem59  44709  stoweidlem60  44710  wallispilem4  44718  stirlinglem5  44728  dirkercncflem2  44754  fourierdlem39  44796  fourierdlem42  44799  fourierdlem46  44802  fourierdlem47  44803  fourierdlem48  44804  fourierdlem50  44806  fourierdlem51  44807  fourierdlem64  44820  fourierdlem73  44829  fourierdlem74  44830  fourierdlem77  44833  fourierdlem80  44836  fourierdlem87  44843  fourierdlem94  44850  fourierdlem103  44859  fourierdlem104  44860  etransclem32  44916  rrxsnicc  44950  sge0cl  45031  sge0f1o  45032  nnfoctbdjlem  45105  ismeannd  45117  omeiunltfirp  45169  hoicvr  45198  ovncvrrp  45214  hoidmvlelem2  45246  hoidmvlelem5  45249  hspdifhsp  45266  hoiqssbllem2  45273  hspmbllem2  45277  vonicclem2  45334  smflimsuplem7  45476  fundcmpsurbijinj  46012  sqrtpwpw2p  46140  isomgrref  46437  lincresunit2  47060  nnpw2pmod  47170  dignn0flhalflem1  47202  dignn0flhalf  47205  rrx2linest  47329  itsclc0yqsol  47351  itsclc0b  47359  functhinclem1  47562  functhinclem2  47563  fullthinc2  47568