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  3603  wereu2  5635  frpomin  6313  funtpg  6571  funcnvtp  6579  funcnvqp  6580  fnund  6633  fun2d  6724  fvun1  6952  iinpreima  7041  ftpg  7128  fsnunf  7159  f1prex  7259  soisores  7302  isotr  7311  off  7671  coof  7677  caofrss  7692  caonncan  7697  fvmpocurryd  8250  oaf1o  8527  omeulem1  8546  oeordi  8551  oelimcl  8564  oeeulem  8565  oeeui  8566  oaabs2  8613  omabs  8615  coflton  8635  pmresg  8843  ralxpmap  8869  domunsncan  9041  sucdom2  9167  unxpdom2  9201  sucxpdom  9202  unblem4  9242  fodomfi  9261  fodomfiOLD  9281  hartogslem1  9495  cantnflt  9625  cantnflem3  9644  cantnflem4  9645  cnfcomlem  9652  cnfcom  9653  ttrcltr  9669  infxpenlem  9966  infxpenc  9971  fseqenlem1  9977  pwsdompw  10156  cfeq0  10209  cofsmo  10222  cfsmolem  10223  ssfin4  10263  hsmexlem4  10382  hsmexlem5  10383  axdc3lem2  10404  fpwwe2  10596  wunpr  10662  mulclpi  10846  mulcanenq  10913  distrlem4pr  10979  prlem934  10986  prlem936  11000  divge0d  13035  elfznelfzob  13734  seqcaopr2  14003  facavg  14266  swrdwrdsymb  14627  cats1un  14686  f1oun2prg  14883  sqrtdiv  15231  sqrtdivd  15390  mulcn2  15562  o1of2  15579  fsumsplit  15707  sumsplit  15734  isumless  15811  demoivreALT  16169  rpnnen2lem11  16192  gcdnncl  16477  qredeu  16628  rpdvds  16630  isprm5  16677  rpexp  16692  prmdvdsbc  16696  divnumden  16718  divdenle  16719  phimullem  16749  phisum  16761  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  pcgcd1  16848  sumhash  16867  fldivp1  16868  pockthlem  16876  setsfun  17141  setsfun0  17142  ssc2  17784  estrreslem1  18098  tleile  18380  sgrppropd  18658  mndpropd  18686  grpidssd  18948  grpinvssd  18949  issubg2  19073  isnsg3  19092  eqgid  19112  kerf1ghm  19179  ghmqusnsglem1  19212  ghmquskerlem1  19215  ghmqusker  19219  gass  19233  symgextres  19355  gsmsymgreqlem2  19361  sylow1lem5  19532  sylow2alem2  19548  sylow3lem3  19559  efgredlemd  19674  efgredlem  19677  frgpnabllem1  19803  frgpnabllem2  19804  subgdmdprd  19966  ablfacrplem  19997  rglcom4d  20120  issrngd  20764  lmodprop2d  20830  lsspropd  20924  pwssplit1  20966  lspvadd  21003  rhmpreimaidl  21187  znidomb  21471  znrrg  21475  lindfind  21725  lindsind  21726  mplsubglem  21908  mplind  21977  ressply1evl  22257  mat1ghm  22370  mdetunilem1  22499  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  cramerimplem2  22571  mat2pmatlin  22622  monmatcollpw  22666  cpmadugsumlemF  22763  mretopd  22979  neiptopnei  23019  neitr  23067  ufilen  23817  flimrest  23870  flimclslem  23871  fclsrest  23911  cnextcn  23954  haustsms2  24024  tsmsxplem2  24041  trust  24117  utoptop  24122  restutop  24125  ustuqtop4  24132  utopsnneiplem  24135  utop2nei  24138  utop3cls  24139  isucn2  24166  ucncn  24172  fmucnd  24179  trcfilu  24181  comet  24401  metustexhalf  24444  metustbl  24454  psmetutop  24455  nrmmetd  24462  reconnlem1  24715  reconnlem2  24716  fsumcn  24761  cmetcaulem  25188  iscmet3lem1  25191  iscmet3lem2  25192  bcthlem5  25228  cmslsschl  25277  rrxdstprj1  25309  minveclem4  25332  ovolfiniun  25402  itg1addlem4  25600  itg1addlem5  25601  itgsplitioo  25739  c1liplem1  25901  dvfsumlem1  25932  plyeq0lem  26115  quotcan  26217  psercnlem1  26335  cxplea  26605  birthdaylem3  26863  musumsum  27102  mpodvdsmulf1o  27104  dvdsmulf1o  27106  dchrelbas4  27154  dchrhash  27182  gausslemma2dlem0d  27270  gausslemma2dlem1a  27276  2lgslem1a1  27300  2sqlem8a  27336  2sqlem8  27337  2sqcoprm  27346  2sqmod  27347  chto1ub  27387  vmadivsum  27393  dchrisumlem1  27400  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  rpvmasum2  27423  mulog2sumlem2  27446  selberg2lem  27461  pntrmax  27475  pntpbnd1  27497  pntlemb  27508  pntlemj  27514  noextend  27578  cuteq0  27744  tgjustc1  28402  tgjustc2  28403  ercgrg  28444  motcgr  28463  tglineeltr  28558  colline  28576  miriso  28597  midexlem  28619  perpneq  28641  foot  28649  f1otrg  28798  axcontlem9  28899  uspgr1ewop  29175  nbupgrres  29291  structtocusgr  29373  wlkp1  29609  clwlkl1loop  29713  uspgrn2crct  29738  crctcshwlkn0lem5  29744  3trlond  30102  3pthond  30104  3spthond  30106  frgr3v  30204  vdgn1frgrv2  30225  numclwwlk3  30314  nmblolbii  30728  minvecolem3  30805  minvecolem4  30809  htthlem  30846  bcs2  31111  nmopub2tALT  31838  nmfnleub2  31855  eighmorth  31893  nmophmi  31960  nmopcoadji  32030  hstle  32159  atcvat3i  32325  opreu2reuALT  32406  prssad  32458  prssbd  32459  iinabrex  32498  disjxpin  32517  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  33142  archirngz  33143  rlocf1  33224  rrgsubm  33234  fracerl  33256  idomsubr  33259  orngmul  33281  linds2eq  33352  nsgqusf1olem3  33386  lidlunitel  33394  unitpidl1  33395  elrspunidl  33399  drngidl  33404  isprmidlc  33418  qsidomlem1  33423  qsidomlem2  33424  qsnzr  33426  mxidlirredi  33442  mxidlirred  33443  qsdrngi  33466  qsdrnglem2  33467  rprmasso  33496  1arithidomlem2  33507  1arithufdlem4  33518  zringidom  33522  deg1le0eq0  33542  ply1unit  33544  ply1dg1rt  33548  ply1dg3rt0irred  33551  m1pmeq  33552  ply1degltdimlem  33618  ply1degltdim  33619  lindsunlem  33620  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  assalactf1o  33631  ply1annprmidl  33697  minplyirredlem  33700  irngnminplynz  33702  minplyelirng  33705  algextdeglem4  33710  constrconj  33735  constrsqrtcl  33769  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpinconstrlem1  33779  1smat1  33794  madjusmdetlem2  33818  qtophaus  33826  locfinref  33831  zarclssn  33863  zar0ring  33868  zarmxt1  33870  rhmpreimacnlem  33874  rhmpreimacn  33875  metideq  33883  sqsscirc2  33899  tpr2rico  33902  fmcncfil  33921  lmxrge0  33942  lmdvg  33943  qqhval2lem  33971  qqhf  33976  qqhnm  33980  esumle  34048  gsumesum  34049  esumlef  34052  esumrnmpt2  34058  esumpcvgval  34068  esum2d  34083  ofcf  34093  ldsysgenld  34150  ldgenpisyslem1  34153  unelros  34161  difelros  34162  inelsros  34168  diffiunisros  34169  imambfm  34253  omssubadd  34291  inelcarsg  34302  carsgsigalem  34306  carsggect  34309  carsgclctunlem2  34310  oddpwdc  34345  eulerpartlems  34351  eulerpartlemb  34359  eulerpartlemt  34362  iwrdsplit  34378  sseqf  34383  sseqfres  34384  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemfrcn0  34521  plymulx0  34538  signsplypnf  34541  signsvtn0  34561  signstfvneq0  34563  signsvtp  34574  signsvtn  34575  fsum2dsub  34598  reprlt  34610  hashreprin  34611  reprgt  34612  reprpmtf1o  34617  chtvalz  34620  breprexplema  34621  breprexplemc  34623  breprexp  34624  circlemeth  34631  logdivsqrle  34641  hgt750lemb  34647  lpadlem3  34669  lpadleft  34674  bnj1536  34844  bnj1001  34949  bnj1280  35010  satffunlem1  35394  satffunlem2  35395  elmrsubrn  35507  neibastop3  36350  finxpsuclem  37385  poimirlem16  37630  poimirlem19  37633  poimirlem20  37634  poimirlem29  37643  mblfinlem3  37653  itg2addnclem3  37667  ftc1cnnclem  37685  lautlt  40085  lautcvr  40086  lauteq  40089  lautco  40091  ltrncl  40119  ltrncnvleN  40124  trljat2  40161  cdlemc6  40190  cdleme20c  40305  cdleme20j  40312  cdleme22e  40338  cdleme22eALTN  40339  cdlemg7aN  40619  cdlemg12e  40641  cdlemg17dALTN  40658  cdlemh  40811  cdlemkfid1N  40915  dibglbN  41160  diblss  41164  diclspsn  41188  dih1  41280  dihglbcpreN  41294  dihmeetlem4preN  41300  lcfrlem19  41555  aks4d1p8d1  42072  evlsvvval  42551  fsuppind  42578  mapfzcons  42704  mzpcl34  42719  mzpindd  42734  mzpsubst  42736  diophrw  42747  diophren  42801  irrapxlem1  42810  pellexlem5  42821  acongrep  42969  pwssplit4  43078  omlimcl2  43231  onexoegt  43233  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  44489  modelaxrep  44971  mulltgt0  45016  fnchoice  45023  3adantlr3  45034  3adantll2  45035  3adantll3  45036  uzwo4  45047  disjf1o  45185  supxrgelem  45333  infleinflem2  45367  xrralrecnnle  45379  supxrunb3  45395  unb2ltle  45411  infrpgernmpt  45461  iooiinicc  45540  iooiinioc  45554  fmuldfeq  45581  mccl  45596  limccog  45618  limcrecl  45627  lptioo1  45630  islpcn  45637  limsupre  45639  neglimc  45645  0ellimcdiv  45647  limclner  45649  climleltrp  45674  climinf3  45714  liminflimsupclim  45805  xlimpnfxnegmnf  45812  icccncfext  45885  fprodcncf  45898  dvnmptdivc  45936  dvnmul  45941  dvmptfprod  45943  dvnprodlem3  45946  stoweidlem25  46023  stoweidlem34  46032  stoweidlem38  46036  stoweidlem44  46042  stoweidlem48  46046  stoweidlem49  46047  stoweidlem59  46057  stoweidlem60  46058  wallispilem4  46066  stirlinglem5  46076  dirkercncflem2  46102  fourierdlem39  46144  fourierdlem42  46147  fourierdlem46  46150  fourierdlem47  46151  fourierdlem48  46152  fourierdlem50  46154  fourierdlem51  46155  fourierdlem64  46168  fourierdlem73  46177  fourierdlem74  46178  fourierdlem77  46181  fourierdlem80  46184  fourierdlem87  46191  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  etransclem32  46264  rrxsnicc  46298  sge0cl  46379  sge0f1o  46380  nnfoctbdjlem  46453  ismeannd  46465  omeiunltfirp  46517  hoicvr  46546  ovncvrrp  46562  hoidmvlelem2  46594  hoidmvlelem5  46597  hspdifhsp  46614  hoiqssbllem2  46621  hspmbllem2  46625  vonicclem2  46682  smflimsuplem7  46824  fundcmpsurbijinj  47411  sqrtpwpw2p  47539  lincresunit2  48467  nnpw2pmod  48572  dignn0flhalflem1  48604  dignn0flhalf  48607  rrx2linest  48731  itsclc0yqsol  48753  itsclc0b  48761  brab2dd  48816  oppcendc  49007  imaidfu  49099  imasubc  49140  oppcthinendcALT  49430  functhinclem1  49433  functhinclem2  49434  fullthinc2  49440