Theorem syl21anc 838

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:  syl1111anc  840  rspc2dv  3636  wereu2  5685  frpomin  6362  funtpg  6622  funcnvtp  6630  funcnvqp  6631  fnund  6683  fun2d  6772  fvun1  6999  iinpreima  7088  ftpg  7175  fsnunf  7204  f1prex  7303  soisores  7346  isotr  7355  off  7714  coof  7720  caofrss  7734  caonncan  7739  fvmpocurryd  8294  oaf1o  8599  omeulem1  8618  oeordi  8623  oelimcl  8636  oeeulem  8637  oeeui  8638  oaabs2  8685  omabs  8687  coflton  8707  pmresg  8908  ralxpmap  8934  domunsncan  9110  sucdom2OLD  9120  sucdom2  9240  unxpdom2  9287  sucxpdom  9288  unblem4  9328  fodomfi  9347  fodomfiOLD  9367  hartogslem1  9579  cantnflt  9709  cantnflem3  9728  cantnflem4  9729  cnfcomlem  9736  cnfcom  9737  ttrcltr  9753  infxpenlem  10050  infxpenc  10055  fseqenlem1  10061  pwsdompw  10240  cfeq0  10293  cofsmo  10306  cfsmolem  10307  ssfin4  10347  hsmexlem4  10466  hsmexlem5  10467  axdc3lem2  10488  fpwwe2  10680  wunpr  10746  mulclpi  10930  mulcanenq  10997  distrlem4pr  11063  prlem934  11070  prlem936  11084  divge0d  13114  elfznelfzob  13808  seqcaopr2  14075  facavg  14336  swrdwrdsymb  14696  cats1un  14755  f1oun2prg  14952  sqrtdiv  15300  sqrtdivd  15458  mulcn2  15628  o1of2  15645  fsumsplit  15773  sumsplit  15800  isumless  15877  demoivreALT  16233  rpnnen2lem11  16256  gcdnncl  16540  qredeu  16691  rpdvds  16693  isprm5  16740  rpexp  16755  prmdvdsbc  16759  divnumden  16781  divdenle  16782  phimullem  16812  phisum  16823  pythagtriplem4  16852  pythagtriplem8  16856  pythagtriplem9  16857  pcgcd1  16910  sumhash  16929  fldivp1  16930  pockthlem  16938  setsfun  17204  setsfun0  17205  ssc2  17869  estrreslem1  18191  estrreslem1OLD  18192  tleile  18478  sgrppropd  18756  mndpropd  18784  grpidssd  19046  grpinvssd  19047  issubg2  19171  isnsg3  19190  eqgid  19210  kerf1ghm  19277  ghmqusnsglem1  19310  ghmquskerlem1  19313  ghmqusker  19317  gass  19331  symgextres  19457  gsmsymgreqlem2  19463  sylow1lem5  19634  sylow2alem2  19650  sylow3lem3  19661  efgredlemd  19776  efgredlem  19779  frgpnabllem1  19905  frgpnabllem2  19906  subgdmdprd  20068  ablfacrplem  20099  rglcom4d  20228  issrngd  20872  lmodprop2d  20938  lsspropd  21033  pwssplit1  21075  lspvadd  21112  rhmpreimaidl  21304  znidomb  21597  znrrg  21601  lindfind  21853  lindsind  21854  mplsubglem  22036  mplind  22111  ressply1evl  22389  mat1ghm  22504  mdetunilem1  22633  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  cramerimplem2  22705  mat2pmatlin  22756  monmatcollpw  22800  cpmadugsumlemF  22897  mretopd  23115  neiptopnei  23155  neitr  23203  ufilen  23953  flimrest  24006  flimclslem  24007  fclsrest  24047  cnextcn  24090  haustsms2  24160  tsmsxplem2  24177  trust  24253  utoptop  24258  restutop  24261  ustuqtop4  24268  utopsnneiplem  24271  utop2nei  24274  utop3cls  24275  isucn2  24303  ucncn  24309  fmucnd  24316  trcfilu  24318  comet  24541  metustexhalf  24584  metustbl  24594  psmetutop  24595  nrmmetd  24602  reconnlem1  24861  reconnlem2  24862  fsumcn  24907  cmetcaulem  25335  iscmet3lem1  25338  iscmet3lem2  25339  bcthlem5  25375  cmslsschl  25424  rrxdstprj1  25456  minveclem4  25479  ovolfiniun  25549  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  itgsplitioo  25887  c1liplem1  26049  dvfsumlem1  26080  plyeq0lem  26263  quotcan  26365  psercnlem1  26483  cxplea  26752  birthdaylem3  27010  musumsum  27249  mpodvdsmulf1o  27251  dvdsmulf1o  27253  dchrelbas4  27301  dchrhash  27329  gausslemma2dlem0d  27417  gausslemma2dlem1a  27423  2lgslem1a1  27447  2sqlem8a  27483  2sqlem8  27484  2sqcoprm  27493  2sqmod  27494  chto1ub  27534  vmadivsum  27540  dchrisumlem1  27547  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  rpvmasum2  27570  mulog2sumlem2  27593  selberg2lem  27608  pntrmax  27622  pntpbnd1  27644  pntlemb  27655  pntlemj  27661  noextend  27725  cuteq0  27891  tgjustc1  28497  tgjustc2  28498  ercgrg  28539  motcgr  28558  tglineeltr  28653  colline  28671  miriso  28692  midexlem  28714  perpneq  28736  foot  28744  f1otrg  28893  axcontlem9  29001  uspgr1ewop  29279  nbupgrres  29395  structtocusgr  29477  wlkp1  29713  clwlkl1loop  29815  uspgrn2crct  29837  crctcshwlkn0lem5  29843  3trlond  30201  3pthond  30203  3spthond  30205  frgr3v  30303  vdgn1frgrv2  30324  numclwwlk3  30413  nmblolbii  30827  minvecolem3  30904  minvecolem4  30908  htthlem  30945  bcs2  31210  nmopub2tALT  31937  nmfnleub2  31954  eighmorth  31992  nmophmi  32059  nmopcoadji  32129  hstle  32258  atcvat3i  32424  bibiad  32485  opreu2reuALT  32504  iinabrex  32588  disjxpin  32607  fmptco1f1o  32649  off2  32657  xppreima2  32667  fgreu  32688  suppovss  32695  1stpreimas  32720  padct  32736  resf1o  32747  fpwrelmap  32750  xrofsup  32777  eliccelico  32785  elicoelioo  32786  iocinif  32789  difioo  32790  suppssnn0  32814  ccatf1  32917  pfxlsw2ccat  32919  wrdt2ind  32922  ressprs  32938  chnind  32984  xrge0addgt0  33004  xrge0adddir  33005  mndlactf1o  33017  mndractf1o  33018  gsumhashmul  33046  omndmul3  33072  gsumle  33083  symgcom  33085  pmtrcnel  33091  pmtrcnel2  33092  pmtrcnelor  33093  cycpmfv2  33116  trsp2cyc  33125  cycpmco2lem7  33134  cyc3genpm  33154  cycpmconjslem2  33157  cyc3conja  33159  archirng  33177  archirngz  33178  rlocf1  33259  rrgsubm  33267  fracerl  33287  idomsubr  33290  orngmul  33312  linds2eq  33388  nsgqusf1olem3  33422  lidlunitel  33430  unitpidl1  33431  elrspunidl  33435  drngidl  33440  isprmidlc  33454  qsidomlem1  33459  qsidomlem2  33460  qsnzr  33462  mxidlirredi  33478  mxidlirred  33479  qsdrngi  33502  qsdrnglem2  33503  rprmasso  33532  1arithidomlem2  33543  1arithufdlem4  33554  zringidom  33558  deg1le0eq0  33577  ply1unit  33579  ply1dg1rt  33583  ply1dg3rt0irred  33586  m1pmeq  33587  ply1degltdimlem  33649  ply1degltdim  33650  lindsunlem  33651  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  assalactf1o  33662  ply1annprmidl  33714  minplyirredlem  33717  irngnminplynz  33719  algextdeglem4  33725  constrconj  33749  1smat1  33764  madjusmdetlem2  33788  qtophaus  33796  locfinref  33801  zarclssn  33833  zar0ring  33838  zarmxt1  33840  rhmpreimacnlem  33844  rhmpreimacn  33845  metideq  33853  sqsscirc2  33869  tpr2rico  33872  fmcncfil  33891  lmxrge0  33912  lmdvg  33913  qqhval2lem  33943  qqhf  33948  qqhnm  33952  esumle  34038  gsumesum  34039  esumlef  34042  esumrnmpt2  34048  esumpcvgval  34058  esum2d  34073  ofcf  34083  ldsysgenld  34140  ldgenpisyslem1  34143  unelros  34151  difelros  34152  inelsros  34158  diffiunisros  34159  imambfm  34243  omssubadd  34281  inelcarsg  34292  carsgsigalem  34296  carsggect  34299  carsgclctunlem2  34300  oddpwdc  34335  eulerpartlems  34341  eulerpartlemb  34349  eulerpartlemt  34352  iwrdsplit  34368  sseqf  34373  sseqfres  34374  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemfrcn0  34510  sgnsub  34525  plymulx0  34540  signsplypnf  34543  signsvtn0  34563  signstfvneq0  34565  signsvtp  34576  signsvtn  34577  fsum2dsub  34600  reprlt  34612  hashreprin  34613  reprgt  34614  reprpmtf1o  34619  chtvalz  34622  breprexplema  34623  breprexplemc  34625  breprexp  34626  circlemeth  34633  logdivsqrle  34643  hgt750lemb  34649  lpadlem3  34671  lpadleft  34676  bnj1536  34846  bnj1001  34951  bnj1280  35012  satffunlem1  35391  satffunlem2  35392  elmrsubrn  35504  neibastop3  36344  finxpsuclem  37379  poimirlem16  37622  poimirlem19  37625  poimirlem20  37626  poimirlem29  37635  mblfinlem3  37645  itg2addnclem3  37659  ftc1cnnclem  37677  lautlt  40073  lautcvr  40074  lauteq  40077  lautco  40079  ltrncl  40107  ltrncnvleN  40112  trljat2  40149  cdlemc6  40178  cdleme20c  40293  cdleme20j  40300  cdleme22e  40326  cdleme22eALTN  40327  cdlemg7aN  40607  cdlemg12e  40629  cdlemg17dALTN  40646  cdlemh  40799  cdlemkfid1N  40903  dibglbN  41148  diblss  41152  diclspsn  41176  dih1  41268  dihglbcpreN  41282  dihmeetlem4preN  41288  lcfrlem19  41543  aks4d1p8d1  42065  evlsvvval  42549  fsuppind  42576  mapfzcons  42703  mzpcl34  42718  mzpindd  42733  mzpsubst  42735  diophrw  42746  diophren  42800  irrapxlem1  42809  pellexlem5  42820  acongrep  42968  pwssplit4  43077  omlimcl2  43230  onexoegt  43232  oasubex  43275  omlim2  43288  nnoeomeqom  43301  nnawordexg  43316  succlg  43317  oacl2g  43319  onmcl  43320  omabs2  43321  omcl2  43322  tfsconcatrev  43337  ofoafg  43343  ofoaf  43344  ofoaass  43349  naddcnfass  43358  naddwordnexlem4  43390  omssrncard  43529  brtrclfv2  43716  rfovcnvf1od  43993  ntrk0kbimka  44028  isotone1  44037  isotone2  44038  4an4132  44496  modelaxrep  44945  mulltgt0  44959  fnchoice  44966  3adantlr3  44977  3adantll2  44978  3adantll3  44979  uzwo4  44992  disjf1o  45133  supxrgelem  45286  infleinflem2  45320  xrralrecnnle  45332  supxrunb3  45348  unb2ltle  45364  infrpgernmpt  45414  iooiinicc  45494  iooiinioc  45508  fmuldfeq  45538  mccl  45553  limccog  45575  limcrecl  45584  lptioo1  45587  islpcn  45594  limsupre  45596  neglimc  45602  0ellimcdiv  45604  limclner  45606  climleltrp  45631  climinf3  45671  liminflimsupclim  45762  xlimpnfxnegmnf  45769  icccncfext  45842  fprodcncf  45855  dvnmptdivc  45893  dvnmul  45898  dvmptfprod  45900  dvnprodlem3  45903  stoweidlem25  45980  stoweidlem34  45989  stoweidlem38  45993  stoweidlem44  45999  stoweidlem48  46003  stoweidlem49  46004  stoweidlem59  46014  stoweidlem60  46015  wallispilem4  46023  stirlinglem5  46033  dirkercncflem2  46059  fourierdlem39  46101  fourierdlem42  46104  fourierdlem46  46107  fourierdlem47  46108  fourierdlem48  46109  fourierdlem50  46111  fourierdlem51  46112  fourierdlem64  46125  fourierdlem73  46134  fourierdlem74  46135  fourierdlem77  46138  fourierdlem80  46141  fourierdlem87  46148  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  etransclem32  46221  rrxsnicc  46255  sge0cl  46336  sge0f1o  46337  nnfoctbdjlem  46410  ismeannd  46422  omeiunltfirp  46474  hoicvr  46503  ovncvrrp  46519  hoidmvlelem2  46551  hoidmvlelem5  46554  hspdifhsp  46571  hoiqssbllem2  46578  hspmbllem2  46582  vonicclem2  46639  smflimsuplem7  46781  fundcmpsurbijinj  47334  sqrtpwpw2p  47462  lincresunit2  48323  nnpw2pmod  48432  dignn0flhalflem1  48464  dignn0flhalf  48467  rrx2linest  48591  itsclc0yqsol  48613  itsclc0b  48621  functhinclem1  48840  functhinclem2  48841  fullthinc2  48846