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  3591  wereu2  5621  frpomin  6298  funtpg  6547  funcnvtp  6555  funcnvqp  6556  fnund  6607  fun2d  6698  fvun1  6925  iinpreima  7014  ftpg  7101  fsnunf  7131  f1prex  7230  soisores  7273  isotr  7282  off  7640  coof  7646  caofrss  7661  caonncan  7666  fvmpocurryd  8213  oaf1o  8490  omeulem1  8509  oeordi  8515  oelimcl  8528  oeeulem  8529  oeeui  8530  oaabs2  8577  omabs  8579  coflton  8599  pmresg  8808  ralxpmap  8834  domunsncan  9005  sucdom2  9127  unxpdom2  9160  sucxpdom  9161  unblem4  9195  fodomfi  9212  fodomfiOLD  9230  hartogslem1  9447  cantnflt  9581  cantnflem3  9600  cantnflem4  9601  cnfcomlem  9608  cnfcom  9609  ttrcltr  9625  infxpenlem  9923  infxpenc  9928  fseqenlem1  9934  pwsdompw  10113  cfeq0  10166  cofsmo  10179  cfsmolem  10180  ssfin4  10220  hsmexlem4  10339  hsmexlem5  10340  axdc3lem2  10361  fpwwe2  10554  wunpr  10620  mulclpi  10804  mulcanenq  10871  distrlem4pr  10937  prlem934  10944  prlem936  10958  divge0d  12989  elfzodif0  13686  elfznelfzob  13690  seqcaopr2  13961  facavg  14224  swrdwrdsymb  14586  cats1un  14644  f1oun2prg  14840  sqrtdiv  15188  sqrtdivd  15347  mulcn2  15519  o1of2  15536  fsumsplit  15664  sumsplit  15691  isumless  15768  demoivreALT  16126  rpnnen2lem11  16149  gcdnncl  16434  qredeu  16585  rpdvds  16587  isprm5  16634  rpexp  16649  prmdvdsbc  16653  divnumden  16675  divdenle  16676  phimullem  16706  phisum  16718  pythagtriplem4  16747  pythagtriplem8  16751  pythagtriplem9  16752  pcgcd1  16805  sumhash  16824  fldivp1  16825  pockthlem  16833  setsfun  17098  setsfun0  17099  ssc2  17746  estrreslem1  18060  tleile  18342  chnind  18544  sgrppropd  18656  mndpropd  18684  grpidssd  18946  grpinvssd  18947  issubg2  19071  isnsg3  19089  eqgid  19109  kerf1ghm  19176  ghmqusnsglem1  19209  ghmquskerlem1  19212  ghmqusker  19216  gass  19230  symgextres  19354  gsmsymgreqlem2  19360  sylow1lem5  19531  sylow2alem2  19547  sylow3lem3  19558  efgredlemd  19673  efgredlem  19676  frgpnabllem1  19802  frgpnabllem2  19803  subgdmdprd  19965  ablfacrplem  19996  omndmul3  20063  gsumle  20074  rglcom4d  20146  issrngd  20788  orngmul  20798  lmodprop2d  20875  lsspropd  20969  pwssplit1  21011  lspvadd  21048  rhmpreimaidl  21232  znidomb  21516  znrrg  21520  lindfind  21771  lindsind  21772  mplsubglem  21954  mplind  22025  evlsvvval  22048  ressply1evl  22314  mat1ghm  22427  mdetunilem1  22556  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  cramerimplem2  22628  mat2pmatlin  22679  monmatcollpw  22723  cpmadugsumlemF  22820  mretopd  23036  neiptopnei  23076  neitr  23124  ufilen  23874  flimrest  23927  flimclslem  23928  fclsrest  23968  cnextcn  24011  haustsms2  24081  tsmsxplem2  24098  trust  24173  utoptop  24178  restutop  24181  ustuqtop4  24188  utopsnneiplem  24191  utop2nei  24194  utop3cls  24195  isucn2  24222  ucncn  24228  fmucnd  24235  trcfilu  24237  comet  24457  metustexhalf  24500  metustbl  24510  psmetutop  24511  nrmmetd  24518  reconnlem1  24771  reconnlem2  24772  fsumcn  24817  cmetcaulem  25244  iscmet3lem1  25247  iscmet3lem2  25248  bcthlem5  25284  cmslsschl  25333  rrxdstprj1  25365  minveclem4  25388  ovolfiniun  25458  itg1addlem4  25656  itg1addlem5  25657  itgsplitioo  25795  c1liplem1  25957  dvfsumlem1  25988  plyeq0lem  26171  quotcan  26273  psercnlem1  26391  cxplea  26661  birthdaylem3  26919  musumsum  27158  mpodvdsmulf1o  27160  dvdsmulf1o  27162  dchrelbas4  27210  dchrhash  27238  gausslemma2dlem0d  27326  gausslemma2dlem1a  27332  2lgslem1a1  27356  2sqlem8a  27392  2sqlem8  27393  2sqcoprm  27402  2sqmod  27403  chto1ub  27443  vmadivsum  27449  dchrisumlem1  27456  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  rpvmasum2  27479  mulog2sumlem2  27502  selberg2lem  27517  pntrmax  27531  pntpbnd1  27553  pntlemb  27564  pntlemj  27570  noextend  27634  cuteq0  27811  tgjustc1  28547  tgjustc2  28548  ercgrg  28589  motcgr  28608  tglineeltr  28703  colline  28721  miriso  28742  midexlem  28764  perpneq  28786  foot  28794  f1otrg  28943  axcontlem9  29045  uspgr1ewop  29321  nbupgrres  29437  structtocusgr  29519  wlkp1  29753  clwlkl1loop  29856  uspgrn2crct  29881  crctcshwlkn0lem5  29887  3trlond  30248  3pthond  30250  3spthond  30252  frgr3v  30350  vdgn1frgrv2  30371  numclwwlk3  30460  nmblolbii  30874  minvecolem3  30951  minvecolem4  30955  htthlem  30992  bcs2  31257  nmopub2tALT  31984  nmfnleub2  32001  eighmorth  32039  nmophmi  32106  nmopcoadji  32176  hstle  32305  atcvat3i  32471  opreu2reuALT  32551  prssad  32604  prssbd  32605  iinabrex  32644  disjxpin  32663  fmptco1f1o  32711  off2  32719  xppreima2  32729  fgreu  32750  suppovss  32760  1stpreimas  32785  padct  32797  resf1o  32809  fpwrelmap  32812  arginv  32827  argcj  32828  xrofsup  32847  eliccelico  32857  elicoelioo  32858  iocinif  32861  difioo  32862  suppssnn0  32885  hashpss  32889  elq2  32892  sgnsub  32918  2exple2exp  32926  oexpled  32928  indsupp  32949  indfsid  32951  ccatf1  33031  pfxlsw2ccat  33032  wrdt2ind  33035  ressprs  33048  xrge0addgt0  33099  xrge0adddir  33100  mndlactf1o  33112  mndractf1o  33113  gsumhashmul  33150  gsummulsubdishift1  33151  symgcom  33165  pmtrcnel  33171  pmtrcnel2  33172  pmtrcnelor  33173  cycpmfv2  33196  trsp2cyc  33205  cycpmco2lem7  33214  cyc3genpm  33234  cycpmconjslem2  33237  cyc3conja  33239  archirng  33270  archirngz  33271  rlocf1  33355  rrgsubm  33366  fracerl  33388  idomsubr  33391  linds2eq  33462  nsgqusf1olem3  33496  lidlunitel  33504  unitpidl1  33505  elrspunidl  33509  drngidl  33514  isprmidlc  33528  qsidomlem1  33533  qsidomlem2  33534  qsnzr  33536  mxidlirredi  33552  mxidlirred  33553  qsdrngi  33576  qsdrnglem2  33577  rprmasso  33606  1arithidomlem2  33617  1arithufdlem4  33628  zringidom  33632  deg1le0eq0  33654  ply1unit  33656  ply1dg1rt  33661  ply1dg3rt0irred  33665  m1pmeq  33666  evlextv  33707  mplvrpmrhm  33712  esplympl  33725  esplysply  33729  esplyind  33731  esplyindfv  33732  vietadeg1  33734  ply1degltdimlem  33779  ply1degltdim  33780  lindsunlem  33781  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  assalactf1o  33792  ply1annprmidl  33864  minplyirredlem  33867  irngnminplynz  33869  minplyelirng  33872  algextdeglem4  33877  constrconj  33902  constrsqrtcl  33936  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpinconstrlem1  33946  1smat1  33961  madjusmdetlem2  33985  qtophaus  33993  locfinref  33998  zarclssn  34030  zar0ring  34035  zarmxt1  34037  rhmpreimacnlem  34041  rhmpreimacn  34042  metideq  34050  sqsscirc2  34066  tpr2rico  34069  fmcncfil  34088  lmxrge0  34109  lmdvg  34110  qqhval2lem  34138  qqhf  34143  qqhnm  34147  esumle  34215  gsumesum  34216  esumlef  34219  esumrnmpt2  34225  esumpcvgval  34235  esum2d  34250  ofcf  34260  ldsysgenld  34317  ldgenpisyslem1  34320  unelros  34328  difelros  34329  inelsros  34335  diffiunisros  34336  imambfm  34419  omssubadd  34457  inelcarsg  34468  carsgsigalem  34472  carsggect  34475  carsgclctunlem2  34476  oddpwdc  34511  eulerpartlems  34517  eulerpartlemb  34525  eulerpartlemt  34528  iwrdsplit  34544  sseqf  34549  sseqfres  34550  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemfrcn0  34687  plymulx0  34704  signsplypnf  34707  signsvtn0  34727  signstfvneq0  34729  signsvtp  34740  signsvtn  34741  fsum2dsub  34764  reprlt  34776  hashreprin  34777  reprgt  34778  reprpmtf1o  34783  chtvalz  34786  breprexplema  34787  breprexplemc  34789  breprexp  34790  circlemeth  34797  logdivsqrle  34807  hgt750lemb  34813  lpadlem3  34835  lpadleft  34840  bnj1536  35010  bnj1001  35115  bnj1280  35176  fineqvnttrclselem2  35278  satffunlem1  35601  satffunlem2  35602  elmrsubrn  35714  neibastop3  36556  finxpsuclem  37598  poimirlem16  37833  poimirlem19  37836  poimirlem20  37837  poimirlem29  37846  mblfinlem3  37856  itg2addnclem3  37870  ftc1cnnclem  37888  lautlt  40347  lautcvr  40348  lauteq  40351  lautco  40353  ltrncl  40381  ltrncnvleN  40386  trljat2  40423  cdlemc6  40452  cdleme20c  40567  cdleme20j  40574  cdleme22e  40600  cdleme22eALTN  40601  cdlemg7aN  40881  cdlemg12e  40903  cdlemg17dALTN  40920  cdlemh  41073  cdlemkfid1N  41177  dibglbN  41422  diblss  41426  diclspsn  41450  dih1  41542  dihglbcpreN  41556  dihmeetlem4preN  41562  lcfrlem19  41817  aks4d1p8d1  42334  fsuppind  42829  mapfzcons  42954  mzpcl34  42969  mzpindd  42984  mzpsubst  42986  diophrw  42997  diophren  43051  irrapxlem1  43060  pellexlem5  43071  acongrep  43218  pwssplit4  43327  omlimcl2  43480  onexoegt  43482  oasubex  43524  omlim2  43537  nnoeomeqom  43550  nnawordexg  43565  succlg  43566  oacl2g  43568  onmcl  43569  omabs2  43570  omcl2  43571  tfsconcatrev  43586  ofoafg  43592  ofoaf  43593  ofoaass  43598  naddcnfass  43607  naddwordnexlem4  43639  omssrncard  43777  brtrclfv2  43964  rfovcnvf1od  44241  ntrk0kbimka  44276  isotone1  44285  isotone2  44286  4an4132  44736  modelaxrep  45218  mulltgt0  45263  fnchoice  45270  3adantlr3  45281  3adantll2  45282  3adantll3  45283  uzwo4  45294  disjf1o  45431  supxrgelem  45578  infleinflem2  45611  xrralrecnnle  45623  supxrunb3  45639  unb2ltle  45655  infrpgernmpt  45705  iooiinicc  45784  iooiinioc  45798  fmuldfeq  45825  mccl  45840  limccog  45862  limcrecl  45871  lptioo1  45874  islpcn  45879  limsupre  45881  neglimc  45887  0ellimcdiv  45889  limclner  45891  climleltrp  45916  climinf3  45956  liminflimsupclim  46047  xlimpnfxnegmnf  46054  icccncfext  46127  fprodcncf  46140  dvnmptdivc  46178  dvnmul  46183  dvmptfprod  46185  dvnprodlem3  46188  stoweidlem25  46265  stoweidlem34  46274  stoweidlem38  46278  stoweidlem44  46284  stoweidlem48  46288  stoweidlem49  46289  stoweidlem59  46299  stoweidlem60  46300  wallispilem4  46308  stirlinglem5  46318  dirkercncflem2  46344  fourierdlem39  46386  fourierdlem42  46389  fourierdlem46  46392  fourierdlem47  46393  fourierdlem48  46394  fourierdlem50  46396  fourierdlem51  46397  fourierdlem64  46410  fourierdlem73  46419  fourierdlem74  46420  fourierdlem77  46423  fourierdlem80  46426  fourierdlem87  46433  fourierdlem94  46440  fourierdlem103  46449  fourierdlem104  46450  etransclem32  46506  rrxsnicc  46540  sge0cl  46621  sge0f1o  46622  nnfoctbdjlem  46695  ismeannd  46707  omeiunltfirp  46759  hoicvr  46788  ovncvrrp  46804  hoidmvlelem2  46836  hoidmvlelem5  46839  hspdifhsp  46856  hoiqssbllem2  46863  hspmbllem2  46867  vonicclem2  46924  smflimsuplem7  47066  fundcmpsurbijinj  47652  sqrtpwpw2p  47780  lincresunit2  48720  nnpw2pmod  48825  dignn0flhalflem1  48857  dignn0flhalf  48860  rrx2linest  48984  itsclc0yqsol  49006  itsclc0b  49014  brab2dd  49069  oppcendc  49259  imaidfu  49351  imasubc  49392  oppcthinendcALT  49682  functhinclem1  49685  functhinclem2  49686  fullthinc2  49692