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 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  839  syl1111anc  840  rspc2dv  3616  wereu2  5651  frpomin  6329  funtpg  6590  funcnvtp  6598  funcnvqp  6599  fnund  6652  fun2d  6741  fvun1  6969  iinpreima  7058  ftpg  7145  fsnunf  7176  f1prex  7276  soisores  7319  isotr  7328  off  7687  coof  7693  caofrss  7708  caonncan  7713  fvmpocurryd  8268  oaf1o  8573  omeulem1  8592  oeordi  8597  oelimcl  8610  oeeulem  8611  oeeui  8612  oaabs2  8659  omabs  8661  coflton  8681  pmresg  8882  ralxpmap  8908  domunsncan  9084  sucdom2OLD  9094  sucdom2  9215  unxpdom2  9260  sucxpdom  9261  unblem4  9301  fodomfi  9320  fodomfiOLD  9340  hartogslem1  9554  cantnflt  9684  cantnflem3  9703  cantnflem4  9704  cnfcomlem  9711  cnfcom  9712  ttrcltr  9728  infxpenlem  10025  infxpenc  10030  fseqenlem1  10036  pwsdompw  10215  cfeq0  10268  cofsmo  10281  cfsmolem  10282  ssfin4  10322  hsmexlem4  10441  hsmexlem5  10442  axdc3lem2  10463  fpwwe2  10655  wunpr  10721  mulclpi  10905  mulcanenq  10972  distrlem4pr  11038  prlem934  11045  prlem936  11059  divge0d  13089  elfznelfzob  13787  seqcaopr2  14054  facavg  14317  swrdwrdsymb  14678  cats1un  14737  f1oun2prg  14934  sqrtdiv  15282  sqrtdivd  15440  mulcn2  15610  o1of2  15627  fsumsplit  15755  sumsplit  15782  isumless  15859  demoivreALT  16217  rpnnen2lem11  16240  gcdnncl  16524  qredeu  16675  rpdvds  16677  isprm5  16724  rpexp  16739  prmdvdsbc  16743  divnumden  16765  divdenle  16766  phimullem  16796  phisum  16808  pythagtriplem4  16837  pythagtriplem8  16841  pythagtriplem9  16842  pcgcd1  16895  sumhash  16914  fldivp1  16915  pockthlem  16923  setsfun  17188  setsfun0  17189  ssc2  17833  estrreslem1  18147  tleile  18429  sgrppropd  18707  mndpropd  18735  grpidssd  18997  grpinvssd  18998  issubg2  19122  isnsg3  19141  eqgid  19161  kerf1ghm  19228  ghmqusnsglem1  19261  ghmquskerlem1  19264  ghmqusker  19268  gass  19282  symgextres  19404  gsmsymgreqlem2  19410  sylow1lem5  19581  sylow2alem2  19597  sylow3lem3  19608  efgredlemd  19723  efgredlem  19726  frgpnabllem1  19852  frgpnabllem2  19853  subgdmdprd  20015  ablfacrplem  20046  rglcom4d  20169  issrngd  20813  lmodprop2d  20879  lsspropd  20973  pwssplit1  21015  lspvadd  21052  rhmpreimaidl  21236  znidomb  21520  znrrg  21524  lindfind  21774  lindsind  21775  mplsubglem  21957  mplind  22026  ressply1evl  22306  mat1ghm  22419  mdetunilem1  22548  mdetunilem3  22550  mdetunilem4  22551  mdetunilem9  22556  cramerimplem2  22620  mat2pmatlin  22671  monmatcollpw  22715  cpmadugsumlemF  22812  mretopd  23028  neiptopnei  23068  neitr  23116  ufilen  23866  flimrest  23919  flimclslem  23920  fclsrest  23960  cnextcn  24003  haustsms2  24073  tsmsxplem2  24090  trust  24166  utoptop  24171  restutop  24174  ustuqtop4  24181  utopsnneiplem  24184  utop2nei  24187  utop3cls  24188  isucn2  24215  ucncn  24221  fmucnd  24228  trcfilu  24230  comet  24450  metustexhalf  24493  metustbl  24503  psmetutop  24504  nrmmetd  24511  reconnlem1  24764  reconnlem2  24765  fsumcn  24810  cmetcaulem  25238  iscmet3lem1  25241  iscmet3lem2  25242  bcthlem5  25278  cmslsschl  25327  rrxdstprj1  25359  minveclem4  25382  ovolfiniun  25452  itg1addlem4  25650  itg1addlem5  25651  itgsplitioo  25789  c1liplem1  25951  dvfsumlem1  25982  plyeq0lem  26165  quotcan  26267  psercnlem1  26385  cxplea  26655  birthdaylem3  26913  musumsum  27152  mpodvdsmulf1o  27154  dvdsmulf1o  27156  dchrelbas4  27204  dchrhash  27232  gausslemma2dlem0d  27320  gausslemma2dlem1a  27326  2lgslem1a1  27350  2sqlem8a  27386  2sqlem8  27387  2sqcoprm  27396  2sqmod  27397  chto1ub  27437  vmadivsum  27443  dchrisumlem1  27450  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  rpvmasum2  27473  mulog2sumlem2  27496  selberg2lem  27511  pntrmax  27525  pntpbnd1  27547  pntlemb  27558  pntlemj  27564  noextend  27628  cuteq0  27794  tgjustc1  28400  tgjustc2  28401  ercgrg  28442  motcgr  28461  tglineeltr  28556  colline  28574  miriso  28595  midexlem  28617  perpneq  28639  foot  28647  f1otrg  28796  axcontlem9  28897  uspgr1ewop  29173  nbupgrres  29289  structtocusgr  29371  wlkp1  29607  clwlkl1loop  29711  uspgrn2crct  29736  crctcshwlkn0lem5  29742  3trlond  30100  3pthond  30102  3spthond  30104  frgr3v  30202  vdgn1frgrv2  30223  numclwwlk3  30312  nmblolbii  30726  minvecolem3  30803  minvecolem4  30807  htthlem  30844  bcs2  31109  nmopub2tALT  31836  nmfnleub2  31853  eighmorth  31891  nmophmi  31958  nmopcoadji  32028  hstle  32157  atcvat3i  32323  opreu2reuALT  32404  prssad  32456  prssbd  32457  iinabrex  32496  disjxpin  32515  fmptco1f1o  32557  off2  32565  xppreima2  32575  fgreu  32596  suppovss  32604  1stpreimas  32629  padct  32643  resf1o  32653  fpwrelmap  32656  arginv  32671  argcj  32672  xrofsup  32690  eliccelico  32700  elicoelioo  32701  iocinif  32704  difioo  32705  elfzodif0  32717  suppssnn0  32730  hashpss  32734  elq2  32736  sgnsub  32762  2exple2exp  32770  oexpled  32772  indsupp  32790  ccatf1  32870  pfxlsw2ccat  32872  wrdt2ind  32875  ressprs  32890  chnind  32937  xrge0addgt0  32958  xrge0adddir  32959  mndlactf1o  32971  mndractf1o  32972  gsumhashmul  33001  omndmul3  33027  gsumle  33038  symgcom  33040  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  cycpmfv2  33071  trsp2cyc  33080  cycpmco2lem7  33089  cyc3genpm  33109  cycpmconjslem2  33112  cyc3conja  33114  archirng  33132  archirngz  33133  rlocf1  33214  rrgsubm  33224  fracerl  33246  idomsubr  33249  orngmul  33271  linds2eq  33342  nsgqusf1olem3  33376  lidlunitel  33384  unitpidl1  33385  elrspunidl  33389  drngidl  33394  isprmidlc  33408  qsidomlem1  33413  qsidomlem2  33414  qsnzr  33416  mxidlirredi  33432  mxidlirred  33433  qsdrngi  33456  qsdrnglem2  33457  rprmasso  33486  1arithidomlem2  33497  1arithufdlem4  33508  zringidom  33512  deg1le0eq0  33532  ply1unit  33534  ply1dg1rt  33538  ply1dg3rt0irred  33541  m1pmeq  33542  ply1degltdimlem  33608  ply1degltdim  33609  lindsunlem  33610  lbsdiflsp0  33612  fedgmullem1  33615  fedgmullem2  33616  assalactf1o  33621  ply1annprmidl  33687  minplyirredlem  33690  irngnminplynz  33692  minplyelirng  33695  algextdeglem4  33700  constrconj  33725  constrsqrtcl  33759  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpinconstrlem1  33769  1smat1  33781  madjusmdetlem2  33805  qtophaus  33813  locfinref  33818  zarclssn  33850  zar0ring  33855  zarmxt1  33857  rhmpreimacnlem  33861  rhmpreimacn  33862  metideq  33870  sqsscirc2  33886  tpr2rico  33889  fmcncfil  33908  lmxrge0  33929  lmdvg  33930  qqhval2lem  33958  qqhf  33963  qqhnm  33967  esumle  34035  gsumesum  34036  esumlef  34039  esumrnmpt2  34045  esumpcvgval  34055  esum2d  34070  ofcf  34080  ldsysgenld  34137  ldgenpisyslem1  34140  unelros  34148  difelros  34149  inelsros  34155  diffiunisros  34156  imambfm  34240  omssubadd  34278  inelcarsg  34289  carsgsigalem  34293  carsggect  34296  carsgclctunlem2  34297  oddpwdc  34332  eulerpartlems  34338  eulerpartlemb  34346  eulerpartlemt  34349  iwrdsplit  34365  sseqf  34370  sseqfres  34371  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemfrcn0  34508  plymulx0  34525  signsplypnf  34528  signsvtn0  34548  signstfvneq0  34550  signsvtp  34561  signsvtn  34562  fsum2dsub  34585  reprlt  34597  hashreprin  34598  reprgt  34599  reprpmtf1o  34604  chtvalz  34607  breprexplema  34608  breprexplemc  34610  breprexp  34611  circlemeth  34618  logdivsqrle  34628  hgt750lemb  34634  lpadlem3  34656  lpadleft  34661  bnj1536  34831  bnj1001  34936  bnj1280  34997  satffunlem1  35375  satffunlem2  35376  elmrsubrn  35488  neibastop3  36326  finxpsuclem  37361  poimirlem16  37606  poimirlem19  37609  poimirlem20  37610  poimirlem29  37619  mblfinlem3  37629  itg2addnclem3  37643  ftc1cnnclem  37661  lautlt  40056  lautcvr  40057  lauteq  40060  lautco  40062  ltrncl  40090  ltrncnvleN  40095  trljat2  40132  cdlemc6  40161  cdleme20c  40276  cdleme20j  40283  cdleme22e  40309  cdleme22eALTN  40310  cdlemg7aN  40590  cdlemg12e  40612  cdlemg17dALTN  40629  cdlemh  40782  cdlemkfid1N  40886  dibglbN  41131  diblss  41135  diclspsn  41159  dih1  41251  dihglbcpreN  41265  dihmeetlem4preN  41271  lcfrlem19  41526  aks4d1p8d1  42043  evlsvvval  42533  fsuppind  42560  mapfzcons  42686  mzpcl34  42701  mzpindd  42716  mzpsubst  42718  diophrw  42729  diophren  42783  irrapxlem1  42792  pellexlem5  42803  acongrep  42951  pwssplit4  43060  omlimcl2  43213  onexoegt  43215  oasubex  43257  omlim2  43270  nnoeomeqom  43283  nnawordexg  43298  succlg  43299  oacl2g  43301  onmcl  43302  omabs2  43303  omcl2  43304  tfsconcatrev  43319  ofoafg  43325  ofoaf  43326  ofoaass  43331  naddcnfass  43340  naddwordnexlem4  43372  omssrncard  43511  brtrclfv2  43698  rfovcnvf1od  43975  ntrk0kbimka  44010  isotone1  44019  isotone2  44020  4an4132  44472  modelaxrep  44954  mulltgt0  44994  fnchoice  45001  3adantlr3  45012  3adantll2  45013  3adantll3  45014  uzwo4  45025  disjf1o  45163  supxrgelem  45312  infleinflem2  45346  xrralrecnnle  45358  supxrunb3  45374  unb2ltle  45390  infrpgernmpt  45440  iooiinicc  45519  iooiinioc  45533  fmuldfeq  45560  mccl  45575  limccog  45597  limcrecl  45606  lptioo1  45609  islpcn  45616  limsupre  45618  neglimc  45624  0ellimcdiv  45626  limclner  45628  climleltrp  45653  climinf3  45693  liminflimsupclim  45784  xlimpnfxnegmnf  45791  icccncfext  45864  fprodcncf  45877  dvnmptdivc  45915  dvnmul  45920  dvmptfprod  45922  dvnprodlem3  45925  stoweidlem25  46002  stoweidlem34  46011  stoweidlem38  46015  stoweidlem44  46021  stoweidlem48  46025  stoweidlem49  46026  stoweidlem59  46036  stoweidlem60  46037  wallispilem4  46045  stirlinglem5  46055  dirkercncflem2  46081  fourierdlem39  46123  fourierdlem42  46126  fourierdlem46  46129  fourierdlem47  46130  fourierdlem48  46131  fourierdlem50  46133  fourierdlem51  46134  fourierdlem64  46147  fourierdlem73  46156  fourierdlem74  46157  fourierdlem77  46160  fourierdlem80  46163  fourierdlem87  46170  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  etransclem32  46243  rrxsnicc  46277  sge0cl  46358  sge0f1o  46359  nnfoctbdjlem  46432  ismeannd  46444  omeiunltfirp  46496  hoicvr  46525  ovncvrrp  46541  hoidmvlelem2  46573  hoidmvlelem5  46576  hspdifhsp  46593  hoiqssbllem2  46600  hspmbllem2  46604  vonicclem2  46661  smflimsuplem7  46803  fundcmpsurbijinj  47372  sqrtpwpw2p  47500  lincresunit2  48402  nnpw2pmod  48511  dignn0flhalflem1  48543  dignn0flhalf  48546  rrx2linest  48670  itsclc0yqsol  48692  itsclc0b  48700  brab2dd  48754  oppcendc  48941  imaidfu  49017  imasubc  49039  oppcthinendcALT  49275  functhinclem1  49278  functhinclem2  49279  fullthinc2  49285