Theorem syl21anc 851

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bibiad  853  syl1111anc  854  rspc2dv  3594  wereu2  5656  frpomin  6342  funtpg  6592  funcnvtp  6600  funcnvqp  6601  fnund  6651  fun2d  6743  fvun1  6973  iinpreima  7065  ftpg  7156  fsnunf  7186  f1prex  7288  soisores  7331  isotr  7340  off  7699  coof  7705  caofrss  7720  caonncan  7725  fvmpocurryd  8272  oaf1o  8553  omeulem1  8572  oeordi  8578  oelimcl  8591  oeeulem  8592  oeeui  8593  oaabs2  8640  omabs  8642  coflton  8662  pmresg  8880  ralxpmap  8906  domunsncan  9078  sucdom2  9200  unxpdom2  9233  sucxpdom  9234  unblem4  9268  fodomfi  9285  hartogslem1  9517  cantnflt  9654  cantnflem3  9673  cantnflem4  9674  cnfcomlem  9681  cnfcom  9682  ttrcltr  9698  infxpenlem  10019  infxpenc  10024  fseqenlem1  10030  pwsdompw  10208  cfeq0  10261  cofsmo  10274  cfsmolem  10275  ssfin4  10315  hsmexlem4  10434  hsmexlem5  10435  axdc3lem2  10456  fpwwe2  10655  wunpr  10721  mulclpi  10905  mulcanenq  10972  distrlem4pr  11038  prlem934  11045  prlem936  11059  divge0d  13128  elfzodif0  13828  elfznelfzob  13832  seqcaopr2  14104  facavg  14367  hashpss  14476  ccatf1  14658  swrdwrdsymb  14734  cats1un  14792  f1oun2prg  14990  sgnsub  15181  sqrtdiv  15354  sqrtdivd  15513  mulcn2  15685  o1of2  15702  fsumsplit  15829  sumsplit  15856  isumless  15936  demoivreALT  16293  rpnnen2lem11  16316  gcdnncl  16601  qredeu  16752  rpdvds  16754  isprm5  16802  rpexp  16817  prmdvdsbc  16821  divnumden  16843  divdenle  16844  phimullem  16874  phisum  16886  pythagtriplem4  16915  pythagtriplem8  16919  pythagtriplem9  16920  pcgcd1  16973  sumhash  16992  fldivp1  16993  pockthlem  17001  setsfun  17267  setsfun0  17268  ssc2  17915  estrreslem1  18229  tleile  18511  chnind  18713  sgrppropd  18835  mndpropd  18866  grpidssd  19140  grpinvssd  19141  issubg2  19266  isnsg3  19284  eqgid  19306  kerf1ghm  19375  ghmqusnsglem1  19408  ghmquskerlem1  19411  ghmqusker  19415  gass  19429  symgextres  19553  gsmsymgreqlem2  19559  sylow1lem5  19730  sylow2alem2  19746  sylow3lem3  19757  efgredlemd  19872  efgredlem  19875  frgpnabllem1  20001  frgpnabllem2  20002  subgdmdprd  20164  ablfacrplem  20195  omndmul3  20262  gsumle  20273  rglcom4d  20351  issrngd  21022  orngmul  21032  lmodprop2d  21109  lsspropd  21202  pwssplit1  21244  lspvadd  21281  drngidl  21449  rhmpreimaidl  21480  isprmidlc  21536  qsidomlem1  21544  qsidomlem2  21545  qsnzr  21547  znidomb  21775  znrrg  21779  lindfind  22030  lindsind  22031  mplsubglem  22214  mplind  22287  evlsvvval  22310  ressply1evl  22596  mat1ghm  22706  mdetunilem1  22835  mdetunilem3  22837  mdetunilem4  22838  mdetunilem9  22843  cramerimplem2  22910  mat2pmatlin  22961  monmatcollpw  23005  cpmadugsumlemF  23102  mretopd  23318  neiptopnei  23358  neitr  23406  ufilen  24157  flimrest  24210  flimclslem  24211  fclsrest  24251  cnextcn  24294  haustsms2  24364  tsmsxplem2  24381  trust  24456  utoptop  24461  restutop  24464  ustuqtop4  24471  utopsnneiplem  24474  utop2nei  24477  utop3cls  24478  isucn2  24505  ucncn  24511  fmucnd  24518  trcfilu  24520  comet  24740  metustexhalf  24783  metustbl  24793  psmetutop  24794  nrmmetd  24801  reconnlem1  25054  reconnlem2  25055  fsumcn  25099  cmetcaulem  25517  iscmet3lem1  25520  iscmet3lem2  25521  bcthlem5  25557  cmslsschl  25606  rrxdstprj1  25638  minveclem4  25661  ovolfiniun  25730  itg1addlem4  25928  itg1addlem5  25929  itgsplitioo  26067  c1liplem1  26225  dvfsumlem1  26255  plyeq0lem  26437  plyn0mulidp  26512  quotcan  26540  psercnlem1  26658  cxplea  26931  birthdaylem3  27188  musumsum  27426  mpodvdsmulf1o  27428  dvdsmulf1o  27430  dchrelbas4  27477  dchrhash  27505  gausslemma2dlem0d  27593  gausslemma2dlem1a  27599  2lgslem1a1  27623  2sqlem8a  27659  2sqlem8  27660  2sqcoprm  27669  2sqmod  27670  chto1ub  27710  vmadivsum  27716  dchrisumlem1  27723  dchrvmasumlem2  27732  dchrvmasumiflem1  27735  rpvmasum2  27746  mulog2sumlem2  27769  selberg2lem  27784  pntrmax  27798  pntpbnd1  27820  pntlemb  27831  pntlemj  27837  noextend  27900  cuteq0  28078  tgjustc1  28814  tgjustc2  28815  ercgrg  28857  motcgr  28876  tglineeltr  28976  colline  28995  miriso  29019  midexlem  29041  perpneq  29066  foot  29074  f1otrg  29313  axcontlem9  29415  uspgr1ewop  29694  nbupgrres  29810  structtocusgr  29892  wlkp1  30125  clwlkl1loop  30235  uspgrn2crct  30262  crctcshwlkn0lem5  30268  3trlond  30639  3pthond  30641  3spthond  30643  frgr3v  30741  vdgn1frgrv2  30762  numclwwlk3  30851  nmblolbii  31266  minvecolem3  31343  minvecolem4  31347  htthlem  31384  bcs2  31649  nmopub2tALT  32376  nmfnleub2  32393  eighmorth  32431  nmophmi  32498  nmopcoadji  32568  hstle  32697  atcvat3i  32863  opreu2reuALT  32938  prssad  32990  prssbd  32991  iinabrex  33029  disjxpin  33048  fmptco1f1o  33093  off2  33101  xppreima2  33111  fgreu  33131  suppovss  33140  1stpreimas  33165  padct  33176  resf1o  33188  fpwrelmap  33191  arginv  33205  argcj  33206  xrofsup  33225  eliccelico  33235  elicoelioo  33236  iocinif  33239  difioo  33240  suppssnn0  33263  elq2  33269  2exple2exp  33291  oexpled  33293  indsupp  33300  indfsid  33302  pfxlsw2ccat  33379  wrdt2ind  33382  ressprs  33393  xrge0addgt0  33444  xrge0adddir  33445  mndlactf1o  33457  mndractf1o  33458  gsumhashmul  33494  gsummulsubdishift1  33495  symgcom  33510  pmtrcnel  33516  pmtrcnel2  33517  pmtrcnelor  33518  cycpmfv2  33541  trsp2cyc  33550  cycpmco2lem7  33559  cyc3genpm  33579  cycpmconjslem2  33582  cyc3conja  33584  archirng  33615  archirngz  33616  rlocf1  33701  rlocisunit  33703  rrgsubm  33711  fracerl  33734  idomsubr  33737  linds2eq  33801  nsgqusf1olem3  33831  lidlunitel  33838  unitpidl1  33839  elrspunidl  33843  mxidlirredi  33861  mxidlirred  33862  qsdrngi  33884  qsdrnglem2  33885  dflring2  33890  rprmasso  33922  1arithidomlem2  33933  1arithufdlem4  33944  zringidom  33948  deg1le0eq0  33970  ply1unit  33972  ply1dg1rt  33977  ply1dg3rt0irred  33981  m1pmeq  33982  selvply1rhmlema  34015  selvply1rhmlem1  34017  evlextv  34039  mplvrpmrhm  34044  esplympl  34064  esplysply  34068  esplyind  34072  esplyindfv  34073  vietadeg1  34075  ply1degltdimlem  34119  ply1degltdim  34120  lindsunlem  34121  lbsdiflsp0  34123  fedgmullem1  34126  fedgmullem2  34127  assalactf1o  34132  ply1annprmidl  34204  minplyirredlem  34207  irngnminplynz  34209  minplyelirng  34212  algextdeglem4  34217  constrconj  34242  constrsqrtcl  34276  cos9thpiminplylem1  34279  cos9thpiminplylem2  34280  cos9thpinconstrlem1  34286  1smat1  34301  madjusmdetlem2  34325  qtophaus  34333  locfinref  34338  zarclssn  34370  zar0ring  34375  zarmxt1  34377  rhmpreimacnlem  34381  rhmpreimacn  34382  metideq  34390  sqsscirc2  34406  tpr2rico  34409  fmcncfil  34428  lmxrge0  34449  lmdvg  34450  qqhval2lem  34478  qqhf  34483  qqhnm  34487  esumle  34555  gsumesum  34556  esumlef  34559  esumrnmpt2  34565  esumpcvgval  34575  esum2d  34590  ofcf  34600  ldsysgenld  34658  ldgenpisyslem1  34661  unelros  34669  difelros  34670  inelsros  34676  diffiunisros  34677  imambfm  34760  omssubadd  34798  inelcarsg  34809  carsgsigalem  34813  carsggect  34816  carsgclctunlem2  34817  oddpwdc  34852  eulerpartlems  34858  eulerpartlemb  34866  eulerpartlemt  34869  iwrdsplit  34885  sseqf  34890  sseqfres  34891  ballotlemfc0  34991  ballotlemfcc  34992  ballotlemfrcn0  35028  signsplypnf  35045  signsvtn0  35065  signstfvneq0  35067  signsvtp  35078  signsvtn  35079  fsum2dsub  35102  reprlt  35114  hashreprin  35115  reprgt  35116  reprpmtf1o  35121  chtvalz  35124  breprexplema  35125  breprexplemc  35127  breprexp  35128  circlemeth  35135  logdivsqrle  35145  hgt750lemb  35151  lpadlem3  35176  lpadleft  35181  bnj1536  35350  bnj1001  35455  bnj1280  35516  fineqvnttrclselem2  35635  satffunlem1  35973  satffunlem2  35974  elmrsubrn  36086  neibastop3  36968  finxpsuclem  38138  poimirlem16  38372  poimirlem19  38375  poimirlem20  38376  poimirlem29  38385  mblfinlem3  38395  itg2addnclem3  38409  ftc1cnnclem  38427  lautlt  40951  lautcvr  40952  lauteq  40955  lautco  40957  ltrncl  40985  ltrncnvleN  40990  trljat2  41027  cdlemc6  41056  cdleme20c  41171  cdleme20j  41178  cdleme22e  41204  cdleme22eALTN  41205  cdlemg7aN  41485  cdlemg12e  41507  cdlemg17dALTN  41524  cdlemh  41677  cdlemkfid1N  41781  dibglbN  42026  diblss  42030  diclspsn  42054  dih1  42146  dihglbcpreN  42160  dihmeetlem4preN  42166  lcfrlem19  42421  aks4d1p8d1  42937  fsuppind  43423  mapfzcons  43548  mzpcl34  43563  mzpindd  43578  mzpsubst  43580  diophrw  43591  diophren  43641  irrapxlem1  43650  pellexlem5  43661  acongrep  43808  pwssplit4  43917  omlimcl2  44070  onexoegt  44072  oasubex  44114  omlim2  44127  nnoeomeqom  44140  nnawordexg  44155  succlg  44156  oacl2g  44158  onmcl  44159  omabs2  44160  omcl2  44161  tfsconcatrev  44176  ofoafg  44182  ofoaf  44183  ofoaass  44188  naddcnfass  44197  naddwordnexlem4  44229  omssrncard  44367  brtrclfv2  44554  rfovcnvf1od  44831  ntrk0kbimka  44866  isotone1  44875  isotone2  44876  4an4132  45309  modelaxrep  45791  mulltgt0  45843  fnchoice  45850  3adantlr3  45861  3adantll2  45862  3adantll3  45863  uzwo4  45874  disjf1o  46010  supxrgelem  46154  infleinflem2  46187  xrralrecnnle  46199  supxrunb3  46215  unb2ltle  46230  infrpgernmpt  46280  iooiinicc  46359  iooiinioc  46373  fmuldfeq  46400  mccl  46415  limccog  46437  limcrecl  46446  lptioo1  46449  islpcn  46454  limsupre  46456  neglimc  46462  0ellimcdiv  46464  limclner  46466  climleltrp  46491  climinf3  46531  liminflimsupclim  46622  xlimpnfxnegmnf  46629  icccncfext  46702  fprodcncf  46715  dvnmptdivc  46753  dvnmul  46758  dvmptfprod  46760  dvnprodlem3  46763  stoweidlem25  46840  stoweidlem34  46849  stoweidlem38  46853  stoweidlem44  46859  stoweidlem48  46863  stoweidlem49  46864  stoweidlem59  46874  stoweidlem60  46875  wallispilem4  46883  stirlinglem5  46893  dirkercncflem2  46919  fourierdlem39  46961  fourierdlem42  46964  fourierdlem46  46967  fourierdlem47  46968  fourierdlem48  46969  fourierdlem50  46971  fourierdlem51  46972  fourierdlem64  46985  fourierdlem73  46994  fourierdlem74  46995  fourierdlem77  46998  fourierdlem80  47001  fourierdlem87  47008  fourierdlem94  47015  fourierdlem103  47024  fourierdlem104  47025  etransclem32  47081  rrxsnicc  47115  sge0cl  47196  sge0f1o  47197  nnfoctbdjlem  47270  ismeannd  47282  omeiunltfirp  47334  ovncvrrp  47379  hoidmvlelem2  47411  hoidmvlelem5  47414  hspdifhsp  47431  hoiqssbllem2  47438  hspmbllem2  47442  vonicclem2  47499  smflimsuplem7  47641  tmachlem-agreeprod  47752  fundcmpsurbijinj  48297  sqrtpwpw2p  48428  lincresunit2  49395  nnpw2pmod  49500  dignn0flhalflem1  49532  dignn0flhalf  49535  rrx2linest  49659  itsclc0yqsol  49681  itsclc0b  49689  brab2dd  49743  oppcendc  49931  imaidfu  50023  imasubc  50064  oppcthinendcALT  50354  functhinclem1  50357  functhinclem2  50358  fullthinc2  50364