Theorem syl21anc 844

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

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  bibiad  846  syl1111anc  847  rspc2dv  3576  wereu2  5617  frpomin  6294  funtpg  6543  funcnvtp  6551  funcnvqp  6552  fnund  6603  fun2d  6694  fvun1  6921  iinpreima  7013  ftpg  7102  fsnunf  7132  f1prex  7231  soisores  7274  isotr  7283  off  7641  coof  7647  caofrss  7662  caonncan  7667  fvmpocurryd  8213  oaf1o  8492  omeulem1  8511  oeordi  8517  oelimcl  8530  oeeulem  8531  oeeui  8532  oaabs2  8579  omabs  8581  coflton  8601  pmresg  8812  ralxpmap  8838  domunsncan  9009  sucdom2  9131  unxpdom2  9164  sucxpdom  9165  unblem4  9199  fodomfi  9216  fodomfiOLD  9234  hartogslem1  9451  cantnflt  9588  cantnflem3  9607  cantnflem4  9608  cnfcomlem  9615  cnfcom  9616  ttrcltr  9632  infxpenlem  9930  infxpenc  9935  fseqenlem1  9941  pwsdompw  10120  cfeq0  10174  cofsmo  10187  cfsmolem  10188  ssfin4  10228  hsmexlem4  10347  hsmexlem5  10348  axdc3lem2  10369  fpwwe2  10562  wunpr  10628  mulclpi  10812  mulcanenq  10879  distrlem4pr  10945  prlem934  10952  prlem936  10966  divge0d  13021  elfzodif0  13720  elfznelfzob  13724  seqcaopr2  13995  facavg  14258  swrdwrdsymb  14620  cats1un  14678  f1oun2prg  14874  sqrtdiv  15222  sqrtdivd  15381  mulcn2  15553  o1of2  15570  fsumsplit  15698  sumsplit  15725  isumless  15805  demoivreALT  16163  rpnnen2lem11  16186  gcdnncl  16471  qredeu  16622  rpdvds  16624  isprm5  16672  rpexp  16687  prmdvdsbc  16691  divnumden  16713  divdenle  16714  phimullem  16744  phisum  16756  pythagtriplem4  16785  pythagtriplem8  16789  pythagtriplem9  16790  pcgcd1  16843  sumhash  16862  fldivp1  16863  pockthlem  16871  setsfun  17136  setsfun0  17137  ssc2  17784  estrreslem1  18098  tleile  18380  chnind  18582  sgrppropd  18694  mndpropd  18722  grpidssd  18987  grpinvssd  18988  issubg2  19112  isnsg3  19130  eqgid  19150  kerf1ghm  19216  ghmqusnsglem1  19249  ghmquskerlem1  19252  ghmqusker  19256  gass  19270  symgextres  19394  gsmsymgreqlem2  19400  sylow1lem5  19571  sylow2alem2  19587  sylow3lem3  19598  efgredlemd  19713  efgredlem  19716  frgpnabllem1  19842  frgpnabllem2  19843  subgdmdprd  20005  ablfacrplem  20036  omndmul3  20103  gsumle  20114  rglcom4d  20186  issrngd  20830  orngmul  20840  lmodprop2d  20917  lsspropd  21010  pwssplit1  21052  lspvadd  21089  rhmpreimaidl  21273  znidomb  21539  znrrg  21543  lindfind  21794  lindsind  21795  mplsubglem  21976  mplind  22049  evlsvvval  22072  ressply1evl  22359  mat1ghm  22469  mdetunilem1  22598  mdetunilem3  22600  mdetunilem4  22601  mdetunilem9  22606  cramerimplem2  22670  mat2pmatlin  22721  monmatcollpw  22765  cpmadugsumlemF  22862  mretopd  23078  neiptopnei  23118  neitr  23166  ufilen  23916  flimrest  23969  flimclslem  23970  fclsrest  24010  cnextcn  24053  haustsms2  24123  tsmsxplem2  24140  trust  24215  utoptop  24220  restutop  24223  ustuqtop4  24230  utopsnneiplem  24233  utop2nei  24236  utop3cls  24237  isucn2  24264  ucncn  24270  fmucnd  24277  trcfilu  24279  comet  24499  metustexhalf  24542  metustbl  24552  psmetutop  24553  nrmmetd  24560  reconnlem1  24813  reconnlem2  24814  fsumcn  24858  cmetcaulem  25276  iscmet3lem1  25279  iscmet3lem2  25280  bcthlem5  25316  cmslsschl  25365  rrxdstprj1  25397  minveclem4  25420  ovolfiniun  25489  itg1addlem4  25687  itg1addlem5  25688  itgsplitioo  25826  c1liplem1  25984  dvfsumlem1  26014  plyeq0lem  26196  quotcan  26296  psercnlem1  26411  cxplea  26681  birthdaylem3  26938  musumsum  27176  mpodvdsmulf1o  27178  dvdsmulf1o  27180  dchrelbas4  27227  dchrhash  27255  gausslemma2dlem0d  27343  gausslemma2dlem1a  27349  2lgslem1a1  27373  2sqlem8a  27409  2sqlem8  27410  2sqcoprm  27419  2sqmod  27420  chto1ub  27460  vmadivsum  27466  dchrisumlem1  27473  dchrvmasumlem2  27482  dchrvmasumiflem1  27485  rpvmasum2  27496  mulog2sumlem2  27519  selberg2lem  27534  pntrmax  27548  pntpbnd1  27570  pntlemb  27581  pntlemj  27587  noextend  27650  cuteq0  27827  tgjustc1  28563  tgjustc2  28564  ercgrg  28605  motcgr  28624  tglineeltr  28719  colline  28737  miriso  28758  midexlem  28780  perpneq  28802  foot  28810  f1otrg  28959  axcontlem9  29061  uspgr1ewop  29337  nbupgrres  29453  structtocusgr  29535  wlkp1  29768  clwlkl1loop  29871  uspgrn2crct  29896  crctcshwlkn0lem5  29902  3trlond  30263  3pthond  30265  3spthond  30267  frgr3v  30365  vdgn1frgrv2  30386  numclwwlk3  30475  nmblolbii  30890  minvecolem3  30967  minvecolem4  30971  htthlem  31008  bcs2  31273  nmopub2tALT  32000  nmfnleub2  32017  eighmorth  32055  nmophmi  32122  nmopcoadji  32192  hstle  32321  atcvat3i  32487  opreu2reuALT  32566  prssad  32619  prssbd  32620  iinabrex  32660  disjxpin  32679  fmptco1f1o  32727  off2  32735  xppreima2  32745  fgreu  32765  suppovss  32775  1stpreimas  32800  padct  32812  resf1o  32824  fpwrelmap  32827  arginv  32841  argcj  32842  xrofsup  32861  eliccelico  32871  elicoelioo  32872  iocinif  32875  difioo  32876  suppssnn0  32899  hashpss  32903  elq2  32906  sgnsub  32931  2exple2exp  32939  oexpled  32941  indsupp  32948  indfsid  32950  ccatf1  33030  pfxlsw2ccat  33031  wrdt2ind  33034  ressprs  33047  xrge0addgt0  33098  xrge0adddir  33099  mndlactf1o  33111  mndractf1o  33112  gsumhashmul  33150  gsummulsubdishift1  33151  symgcom  33166  pmtrcnel  33172  pmtrcnel2  33173  pmtrcnelor  33174  cycpmfv2  33197  trsp2cyc  33206  cycpmco2lem7  33215  cyc3genpm  33235  cycpmconjslem2  33238  cyc3conja  33240  archirng  33271  archirngz  33272  rlocf1  33356  rrgsubm  33367  fracerl  33392  idomsubr  33395  linds2eq  33466  nsgqusf1olem3  33500  lidlunitel  33508  unitpidl1  33509  elrspunidl  33513  drngidl  33518  isprmidlc  33532  qsidomlem1  33537  qsidomlem2  33538  qsnzr  33540  mxidlirredi  33556  mxidlirred  33557  qsdrngi  33580  qsdrnglem2  33581  dflring2  33586  rprmasso  33618  1arithidomlem2  33629  1arithufdlem4  33640  zringidom  33644  deg1le0eq0  33666  ply1unit  33668  ply1dg1rt  33673  ply1dg3rt0irred  33677  m1pmeq  33678  selvply1rhmlema  33712  selvply1rhmlem1  33714  evlextv  33736  mplvrpmrhm  33741  esplympl  33761  esplysply  33765  esplyind  33769  esplyindfv  33770  vietadeg1  33772  ply1degltdimlem  33816  ply1degltdim  33817  lindsunlem  33818  lbsdiflsp0  33820  fedgmullem1  33823  fedgmullem2  33824  assalactf1o  33829  ply1annprmidl  33901  minplyirredlem  33904  irngnminplynz  33906  minplyelirng  33909  algextdeglem4  33914  constrconj  33939  constrsqrtcl  33973  cos9thpiminplylem1  33976  cos9thpiminplylem2  33977  cos9thpinconstrlem1  33983  1smat1  33998  madjusmdetlem2  34022  qtophaus  34030  locfinref  34035  zarclssn  34067  zar0ring  34072  zarmxt1  34074  rhmpreimacnlem  34078  rhmpreimacn  34079  metideq  34087  sqsscirc2  34103  tpr2rico  34106  fmcncfil  34125  lmxrge0  34146  lmdvg  34147  qqhval2lem  34175  qqhf  34180  qqhnm  34184  esumle  34252  gsumesum  34253  esumlef  34256  esumrnmpt2  34262  esumpcvgval  34272  esum2d  34287  ofcf  34297  ldsysgenld  34354  ldgenpisyslem1  34357  unelros  34365  difelros  34366  inelsros  34372  diffiunisros  34373  imambfm  34456  omssubadd  34494  inelcarsg  34505  carsgsigalem  34509  carsggect  34512  carsgclctunlem2  34513  oddpwdc  34548  eulerpartlems  34554  eulerpartlemb  34562  eulerpartlemt  34565  iwrdsplit  34581  sseqf  34586  sseqfres  34587  ballotlemfc0  34687  ballotlemfcc  34688  ballotlemfrcn0  34724  plymulx0  34741  signsplypnf  34744  signsvtn0  34764  signstfvneq0  34766  signsvtp  34777  signsvtn  34778  fsum2dsub  34801  reprlt  34813  hashreprin  34814  reprgt  34815  reprpmtf1o  34820  chtvalz  34823  breprexplema  34824  breprexplemc  34826  breprexp  34827  circlemeth  34834  logdivsqrle  34844  hgt750lemb  34850  lpadlem3  34875  lpadleft  34880  bnj1536  35049  bnj1001  35154  bnj1280  35215  fineqvnttrclselem2  35316  satffunlem1  35648  satffunlem2  35649  elmrsubrn  35761  neibastop3  36603  finxpsuclem  37772  poimirlem16  38016  poimirlem19  38019  poimirlem20  38020  poimirlem29  38029  mblfinlem3  38039  itg2addnclem3  38053  ftc1cnnclem  38071  lautlt  40596  lautcvr  40597  lauteq  40600  lautco  40602  ltrncl  40630  ltrncnvleN  40635  trljat2  40672  cdlemc6  40701  cdleme20c  40816  cdleme20j  40823  cdleme22e  40849  cdleme22eALTN  40850  cdlemg7aN  41130  cdlemg12e  41152  cdlemg17dALTN  41169  cdlemh  41322  cdlemkfid1N  41426  dibglbN  41671  diblss  41675  diclspsn  41699  dih1  41791  dihglbcpreN  41805  dihmeetlem4preN  41811  lcfrlem19  42066  aks4d1p8d1  42582  fsuppind  43053  mapfzcons  43178  mzpcl34  43193  mzpindd  43208  mzpsubst  43210  diophrw  43221  diophren  43271  irrapxlem1  43280  pellexlem5  43291  acongrep  43438  pwssplit4  43547  omlimcl2  43700  onexoegt  43702  oasubex  43744  omlim2  43757  nnoeomeqom  43770  nnawordexg  43785  succlg  43786  oacl2g  43788  onmcl  43789  omabs2  43790  omcl2  43791  tfsconcatrev  43806  ofoafg  43812  ofoaf  43813  ofoaass  43818  naddcnfass  43827  naddwordnexlem4  43859  omssrncard  43997  brtrclfv2  44184  rfovcnvf1od  44461  ntrk0kbimka  44496  isotone1  44505  isotone2  44506  4an4132  44956  modelaxrep  45438  mulltgt0  45483  fnchoice  45490  3adantlr3  45501  3adantll2  45502  3adantll3  45503  uzwo4  45514  disjf1o  45650  supxrgelem  45794  infleinflem2  45827  xrralrecnnle  45839  supxrunb3  45855  unb2ltle  45870  infrpgernmpt  45920  iooiinicc  45999  iooiinioc  46013  fmuldfeq  46040  mccl  46055  limccog  46077  limcrecl  46086  lptioo1  46089  islpcn  46094  limsupre  46096  neglimc  46102  0ellimcdiv  46104  limclner  46106  climleltrp  46131  climinf3  46171  liminflimsupclim  46262  xlimpnfxnegmnf  46269  icccncfext  46342  fprodcncf  46355  dvnmptdivc  46393  dvnmul  46398  dvmptfprod  46400  dvnprodlem3  46403  stoweidlem25  46480  stoweidlem34  46489  stoweidlem38  46493  stoweidlem44  46499  stoweidlem48  46503  stoweidlem49  46504  stoweidlem59  46514  stoweidlem60  46515  wallispilem4  46523  stirlinglem5  46533  dirkercncflem2  46559  fourierdlem39  46601  fourierdlem42  46604  fourierdlem46  46607  fourierdlem47  46608  fourierdlem48  46609  fourierdlem50  46611  fourierdlem51  46612  fourierdlem64  46625  fourierdlem73  46634  fourierdlem74  46635  fourierdlem77  46638  fourierdlem80  46641  fourierdlem87  46648  fourierdlem94  46655  fourierdlem103  46664  fourierdlem104  46665  etransclem32  46721  rrxsnicc  46755  sge0cl  46836  sge0f1o  46837  nnfoctbdjlem  46910  ismeannd  46922  omeiunltfirp  46974  ovncvrrp  47019  hoidmvlelem2  47051  hoidmvlelem5  47054  hspdifhsp  47071  hoiqssbllem2  47078  hspmbllem2  47082  vonicclem2  47139  smflimsuplem7  47281  fundcmpsurbijinj  47897  sqrtpwpw2p  48028  lincresunit2  48981  nnpw2pmod  49086  dignn0flhalflem1  49118  dignn0flhalf  49121  rrx2linest  49245  itsclc0yqsol  49267  itsclc0b  49275  brab2dd  49330  oppcendc  49520  imaidfu  49612  imasubc  49653  oppcthinendcALT  49943  functhinclem1  49946  functhinclem2  49947  fullthinc2  49953