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 585	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  840  syl1111anc  841  rspc2dv  3593  wereu2  5629  frpomin  6306  funtpg  6555  funcnvtp  6563  funcnvqp  6564  fnund  6615  fun2d  6706  fvun1  6933  iinpreima  7023  ftpg  7111  fsnunf  7141  f1prex  7240  soisores  7283  isotr  7292  off  7650  coof  7656  caofrss  7671  caonncan  7676  fvmpocurryd  8223  oaf1o  8500  omeulem1  8519  oeordi  8525  oelimcl  8538  oeeulem  8539  oeeui  8540  oaabs2  8587  omabs  8589  coflton  8609  pmresg  8820  ralxpmap  8846  domunsncan  9017  sucdom2  9139  unxpdom2  9172  sucxpdom  9173  unblem4  9207  fodomfi  9224  fodomfiOLD  9242  hartogslem1  9459  cantnflt  9593  cantnflem3  9612  cantnflem4  9613  cnfcomlem  9620  cnfcom  9621  ttrcltr  9637  infxpenlem  9935  infxpenc  9940  fseqenlem1  9946  pwsdompw  10125  cfeq0  10178  cofsmo  10191  cfsmolem  10192  ssfin4  10232  hsmexlem4  10351  hsmexlem5  10352  axdc3lem2  10373  fpwwe2  10566  wunpr  10632  mulclpi  10816  mulcanenq  10883  distrlem4pr  10949  prlem934  10956  prlem936  10970  divge0d  13001  elfzodif0  13698  elfznelfzob  13702  seqcaopr2  13973  facavg  14236  swrdwrdsymb  14598  cats1un  14656  f1oun2prg  14852  sqrtdiv  15200  sqrtdivd  15359  mulcn2  15531  o1of2  15548  fsumsplit  15676  sumsplit  15703  isumless  15780  demoivreALT  16138  rpnnen2lem11  16161  gcdnncl  16446  qredeu  16597  rpdvds  16599  isprm5  16646  rpexp  16661  prmdvdsbc  16665  divnumden  16687  divdenle  16688  phimullem  16718  phisum  16730  pythagtriplem4  16759  pythagtriplem8  16763  pythagtriplem9  16764  pcgcd1  16817  sumhash  16836  fldivp1  16837  pockthlem  16845  setsfun  17110  setsfun0  17111  ssc2  17758  estrreslem1  18072  tleile  18354  chnind  18556  sgrppropd  18668  mndpropd  18696  grpidssd  18958  grpinvssd  18959  issubg2  19083  isnsg3  19101  eqgid  19121  kerf1ghm  19188  ghmqusnsglem1  19221  ghmquskerlem1  19224  ghmqusker  19228  gass  19242  symgextres  19366  gsmsymgreqlem2  19372  sylow1lem5  19543  sylow2alem2  19559  sylow3lem3  19570  efgredlemd  19685  efgredlem  19688  frgpnabllem1  19814  frgpnabllem2  19815  subgdmdprd  19977  ablfacrplem  20008  omndmul3  20075  gsumle  20086  rglcom4d  20158  issrngd  20800  orngmul  20810  lmodprop2d  20887  lsspropd  20981  pwssplit1  21023  lspvadd  21060  rhmpreimaidl  21244  znidomb  21528  znrrg  21532  lindfind  21783  lindsind  21784  mplsubglem  21966  mplind  22037  evlsvvval  22060  ressply1evl  22326  mat1ghm  22439  mdetunilem1  22568  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  cramerimplem2  22640  mat2pmatlin  22691  monmatcollpw  22735  cpmadugsumlemF  22832  mretopd  23048  neiptopnei  23088  neitr  23136  ufilen  23886  flimrest  23939  flimclslem  23940  fclsrest  23980  cnextcn  24023  haustsms2  24093  tsmsxplem2  24110  trust  24185  utoptop  24190  restutop  24193  ustuqtop4  24200  utopsnneiplem  24203  utop2nei  24206  utop3cls  24207  isucn2  24234  ucncn  24240  fmucnd  24247  trcfilu  24249  comet  24469  metustexhalf  24512  metustbl  24522  psmetutop  24523  nrmmetd  24530  reconnlem1  24783  reconnlem2  24784  fsumcn  24829  cmetcaulem  25256  iscmet3lem1  25259  iscmet3lem2  25260  bcthlem5  25296  cmslsschl  25345  rrxdstprj1  25377  minveclem4  25400  ovolfiniun  25470  itg1addlem4  25668  itg1addlem5  25669  itgsplitioo  25807  c1liplem1  25969  dvfsumlem1  26000  plyeq0lem  26183  quotcan  26285  psercnlem1  26403  cxplea  26673  birthdaylem3  26931  musumsum  27170  mpodvdsmulf1o  27172  dvdsmulf1o  27174  dchrelbas4  27222  dchrhash  27250  gausslemma2dlem0d  27338  gausslemma2dlem1a  27344  2lgslem1a1  27368  2sqlem8a  27404  2sqlem8  27405  2sqcoprm  27414  2sqmod  27415  chto1ub  27455  vmadivsum  27461  dchrisumlem1  27468  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  rpvmasum2  27491  mulog2sumlem2  27514  selberg2lem  27529  pntrmax  27543  pntpbnd1  27565  pntlemb  27576  pntlemj  27582  noextend  27646  cuteq0  27823  tgjustc1  28559  tgjustc2  28560  ercgrg  28601  motcgr  28620  tglineeltr  28715  colline  28733  miriso  28754  midexlem  28776  perpneq  28798  foot  28806  f1otrg  28955  axcontlem9  29057  uspgr1ewop  29333  nbupgrres  29449  structtocusgr  29531  wlkp1  29765  clwlkl1loop  29868  uspgrn2crct  29893  crctcshwlkn0lem5  29899  3trlond  30260  3pthond  30262  3spthond  30264  frgr3v  30362  vdgn1frgrv2  30383  numclwwlk3  30472  nmblolbii  30886  minvecolem3  30963  minvecolem4  30967  htthlem  31004  bcs2  31269  nmopub2tALT  31996  nmfnleub2  32013  eighmorth  32051  nmophmi  32118  nmopcoadji  32188  hstle  32317  atcvat3i  32483  opreu2reuALT  32562  prssad  32615  prssbd  32616  iinabrex  32655  disjxpin  32674  fmptco1f1o  32722  off2  32730  xppreima2  32740  fgreu  32760  suppovss  32770  1stpreimas  32795  padct  32807  resf1o  32819  fpwrelmap  32822  arginv  32837  argcj  32838  xrofsup  32857  eliccelico  32867  elicoelioo  32868  iocinif  32871  difioo  32872  suppssnn0  32895  hashpss  32899  elq2  32902  sgnsub  32928  2exple2exp  32936  oexpled  32938  indsupp  32959  indfsid  32961  ccatf1  33041  pfxlsw2ccat  33042  wrdt2ind  33045  ressprs  33058  xrge0addgt0  33109  xrge0adddir  33110  mndlactf1o  33122  mndractf1o  33123  gsumhashmul  33160  gsummulsubdishift1  33161  symgcom  33176  pmtrcnel  33182  pmtrcnel2  33183  pmtrcnelor  33184  cycpmfv2  33207  trsp2cyc  33216  cycpmco2lem7  33225  cyc3genpm  33245  cycpmconjslem2  33248  cyc3conja  33250  archirng  33281  archirngz  33282  rlocf1  33366  rrgsubm  33377  fracerl  33399  idomsubr  33402  linds2eq  33473  nsgqusf1olem3  33507  lidlunitel  33515  unitpidl1  33516  elrspunidl  33520  drngidl  33525  isprmidlc  33539  qsidomlem1  33544  qsidomlem2  33545  qsnzr  33547  mxidlirredi  33563  mxidlirred  33564  qsdrngi  33587  qsdrnglem2  33588  rprmasso  33617  1arithidomlem2  33628  1arithufdlem4  33639  zringidom  33643  deg1le0eq0  33665  ply1unit  33667  ply1dg1rt  33672  ply1dg3rt0irred  33676  m1pmeq  33677  evlextv  33718  mplvrpmrhm  33723  esplympl  33743  esplysply  33747  esplyind  33751  esplyindfv  33752  vietadeg1  33754  ply1degltdimlem  33799  ply1degltdim  33800  lindsunlem  33801  lbsdiflsp0  33803  fedgmullem1  33806  fedgmullem2  33807  assalactf1o  33812  ply1annprmidl  33884  minplyirredlem  33887  irngnminplynz  33889  minplyelirng  33892  algextdeglem4  33897  constrconj  33922  constrsqrtcl  33956  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  cos9thpinconstrlem1  33966  1smat1  33981  madjusmdetlem2  34005  qtophaus  34013  locfinref  34018  zarclssn  34050  zar0ring  34055  zarmxt1  34057  rhmpreimacnlem  34061  rhmpreimacn  34062  metideq  34070  sqsscirc2  34086  tpr2rico  34089  fmcncfil  34108  lmxrge0  34129  lmdvg  34130  qqhval2lem  34158  qqhf  34163  qqhnm  34167  esumle  34235  gsumesum  34236  esumlef  34239  esumrnmpt2  34245  esumpcvgval  34255  esum2d  34270  ofcf  34280  ldsysgenld  34337  ldgenpisyslem1  34340  unelros  34348  difelros  34349  inelsros  34355  diffiunisros  34356  imambfm  34439  omssubadd  34477  inelcarsg  34488  carsgsigalem  34492  carsggect  34495  carsgclctunlem2  34496  oddpwdc  34531  eulerpartlems  34537  eulerpartlemb  34545  eulerpartlemt  34548  iwrdsplit  34564  sseqf  34569  sseqfres  34570  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemfrcn0  34707  plymulx0  34724  signsplypnf  34727  signsvtn0  34747  signstfvneq0  34749  signsvtp  34760  signsvtn  34761  fsum2dsub  34784  reprlt  34796  hashreprin  34797  reprgt  34798  reprpmtf1o  34803  chtvalz  34806  breprexplema  34807  breprexplemc  34809  breprexp  34810  circlemeth  34817  logdivsqrle  34827  hgt750lemb  34833  lpadlem3  34855  lpadleft  34860  bnj1536  35029  bnj1001  35134  bnj1280  35195  fineqvnttrclselem2  35297  satffunlem1  35620  satffunlem2  35621  elmrsubrn  35733  neibastop3  36575  finxpsuclem  37646  poimirlem16  37881  poimirlem19  37884  poimirlem20  37885  poimirlem29  37894  mblfinlem3  37904  itg2addnclem3  37918  ftc1cnnclem  37936  lautlt  40461  lautcvr  40462  lauteq  40465  lautco  40467  ltrncl  40495  ltrncnvleN  40500  trljat2  40537  cdlemc6  40566  cdleme20c  40681  cdleme20j  40688  cdleme22e  40714  cdleme22eALTN  40715  cdlemg7aN  40995  cdlemg12e  41017  cdlemg17dALTN  41034  cdlemh  41187  cdlemkfid1N  41291  dibglbN  41536  diblss  41540  diclspsn  41564  dih1  41656  dihglbcpreN  41670  dihmeetlem4preN  41676  lcfrlem19  41931  aks4d1p8d1  42448  fsuppind  42942  mapfzcons  43067  mzpcl34  43082  mzpindd  43097  mzpsubst  43099  diophrw  43110  diophren  43164  irrapxlem1  43173  pellexlem5  43184  acongrep  43331  pwssplit4  43440  omlimcl2  43593  onexoegt  43595  oasubex  43637  omlim2  43650  nnoeomeqom  43663  nnawordexg  43678  succlg  43679  oacl2g  43681  onmcl  43682  omabs2  43683  omcl2  43684  tfsconcatrev  43699  ofoafg  43705  ofoaf  43706  ofoaass  43711  naddcnfass  43720  naddwordnexlem4  43752  omssrncard  43890  brtrclfv2  44077  rfovcnvf1od  44354  ntrk0kbimka  44389  isotone1  44398  isotone2  44399  4an4132  44849  modelaxrep  45331  mulltgt0  45376  fnchoice  45383  3adantlr3  45394  3adantll2  45395  3adantll3  45396  uzwo4  45407  disjf1o  45544  supxrgelem  45690  infleinflem2  45723  xrralrecnnle  45735  supxrunb3  45751  unb2ltle  45767  infrpgernmpt  45817  iooiinicc  45896  iooiinioc  45910  fmuldfeq  45937  mccl  45952  limccog  45974  limcrecl  45983  lptioo1  45986  islpcn  45991  limsupre  45993  neglimc  45999  0ellimcdiv  46001  limclner  46003  climleltrp  46028  climinf3  46068  liminflimsupclim  46159  xlimpnfxnegmnf  46166  icccncfext  46239  fprodcncf  46252  dvnmptdivc  46290  dvnmul  46295  dvmptfprod  46297  dvnprodlem3  46300  stoweidlem25  46377  stoweidlem34  46386  stoweidlem38  46390  stoweidlem44  46396  stoweidlem48  46400  stoweidlem49  46401  stoweidlem59  46411  stoweidlem60  46412  wallispilem4  46420  stirlinglem5  46430  dirkercncflem2  46456  fourierdlem39  46498  fourierdlem42  46501  fourierdlem46  46504  fourierdlem47  46505  fourierdlem48  46506  fourierdlem50  46508  fourierdlem51  46509  fourierdlem64  46522  fourierdlem73  46531  fourierdlem74  46532  fourierdlem77  46535  fourierdlem80  46538  fourierdlem87  46545  fourierdlem94  46552  fourierdlem103  46561  fourierdlem104  46562  etransclem32  46618  rrxsnicc  46652  sge0cl  46733  sge0f1o  46734  nnfoctbdjlem  46807  ismeannd  46819  omeiunltfirp  46871  hoicvr  46900  ovncvrrp  46916  hoidmvlelem2  46948  hoidmvlelem5  46951  hspdifhsp  46968  hoiqssbllem2  46975  hspmbllem2  46979  vonicclem2  47036  smflimsuplem7  47178  fundcmpsurbijinj  47764  sqrtpwpw2p  47892  lincresunit2  48832  nnpw2pmod  48937  dignn0flhalflem1  48969  dignn0flhalf  48972  rrx2linest  49096  itsclc0yqsol  49118  itsclc0b  49126  brab2dd  49181  oppcendc  49371  imaidfu  49463  imasubc  49504  oppcthinendcALT  49794  functhinclem1  49797  functhinclem2  49798  fullthinc2  49804