Theorem syl21anc 851

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bibiad  853  syl1111anc  854  rspc2dv  3591  wereu2  5645  frpomin  6333  funtpg  6584  funcnvtp  6592  funcnvqp  6593  fnund  6643  fun2d  6735  fvun1  6965  iinpreima  7058  ftpg  7149  fsnunf  7179  f1prex  7281  soisores  7324  isotr  7333  off  7695  coof  7701  caofrss  7716  caonncan  7721  fvmpocurryd  8267  oaf1o  8550  omeulem1  8569  oeordi  8575  oelimcl  8588  oeeulem  8589  oeeui  8590  oaabs2  8637  omabs  8639  coflton  8659  pmresg  8877  ralxpmap  8903  domunsncan  9075  sucdom2  9197  unxpdom2  9230  sucxpdom  9231  unblem4  9265  fodomfi  9282  hartogslem1  9514  cantnflt  9651  cantnflem3  9670  cantnflem4  9671  cnfcomlem  9678  cnfcom  9679  ttrcltr  9695  infxpenlem  10049  infxpenc  10054  fseqenlem1  10060  pwsdompw  10238  cfeq0  10291  cofsmo  10304  cfsmolem  10305  ssfin4  10345  hsmexlem4  10464  hsmexlem5  10465  axdc3lem2  10486  fpwwe2  10685  wunpr  10751  mulclpi  10935  mulcanenq  11002  distrlem4pr  11068  prlem934  11075  prlem936  11089  divge0d  13159  elfzodif0  13859  elfznelfzob  13863  seqcaopr2  14135  facavg  14398  hashpss  14507  ccatf1  14689  swrdwrdsymb  14765  cats1un  14823  f1oun2prg  15021  sgnsub  15212  sqrtdiv  15385  sqrtdivd  15544  mulcn2  15716  o1of2  15733  fsumsplit  15860  sumsplit  15887  isumless  15967  demoivreALT  16322  rpnnen2lem11  16345  gcdnncl  16630  qredeu  16781  rpdvds  16783  isprm5  16831  rpexp  16846  prmdvdsbc  16850  divnumden  16872  divdenle  16873  phimullem  16903  phisum  16915  pythagtriplem4  16944  pythagtriplem8  16948  pythagtriplem9  16949  pcgcd1  17002  sumhash  17021  fldivp1  17022  pockthlem  17030  setsfun  17296  setsfun0  17297  ssc2  17944  estrreslem1  18258  tleile  18540  chnind  18742  sgrppropd  18867  mndpropd  18898  grpidssd  19173  grpinvssd  19174  issubg2  19299  isnsg3  19317  eqgid  19339  kerf1ghm  19408  ghmqusnsglem1  19441  ghmquskerlem1  19444  ghmqusker  19448  gass  19462  symgextres  19586  gsmsymgreqlem2  19592  sylow1lem5  19763  sylow2alem2  19779  sylow3lem3  19790  efgredlemd  19905  efgredlem  19908  frgpnabllem1  20034  frgpnabllem2  20035  subgdmdprd  20197  ablfacrplem  20228  omndmul3  20295  gsumle  20306  rglcom4d  20384  issrngd  21059  orngmul  21069  lmodprop2d  21146  lsspropd  21239  pwssplit1  21281  lspvadd  21318  drngidl  21486  rhmpreimaidl  21518  isprmidlc  21575  qsidomlem1  21583  qsidomlem2  21584  qsnzr  21586  znidomb  21814  znrrg  21818  lindfind  22069  lindsind  22070  mplsubglem  22253  mplind  22326  evlsvvval  22349  ressply1evl  22635  mat1ghm  22745  mdetunilem1  22874  mdetunilem3  22876  mdetunilem4  22877  mdetunilem9  22882  cramerimplem2  22949  mat2pmatlin  23000  monmatcollpw  23044  cpmadugsumlemF  23141  mretopd  23357  neiptopnei  23397  neitr  23445  ufilen  24196  flimrest  24249  flimclslem  24250  fclsrest  24290  cnextcn  24333  haustsms2  24403  tsmsxplem2  24420  trust  24495  utoptop  24500  restutop  24503  ustuqtop4  24510  utopsnneiplem  24513  utop2nei  24516  utop3cls  24517  isucn2  24544  ucncn  24550  fmucnd  24557  trcfilu  24559  comet  24779  metustexhalf  24822  metustbl  24832  psmetutop  24833  nrmmetd  24840  reconnlem1  25093  reconnlem2  25094  fsumcn  25138  cmetcaulem  25556  iscmet3lem1  25559  iscmet3lem2  25560  bcthlem5  25596  cmslsschl  25645  rrxdstprj1  25677  minveclem4  25700  ovolfiniun  25769  itg1addlem4  25967  itg1addlem5  25968  itgsplitioo  26105  c1liplem1  26263  dvfsumlem1  26293  plyeq0lem  26476  plyn0mulidp  26551  quotcan  26581  psercnlem1  26701  cxplea  26973  birthdaylem3  27230  musumsum  27468  mpodvdsmulf1o  27470  dvdsmulf1o  27472  dchrelbas4  27519  dchrhash  27547  gausslemma2dlem0d  27635  gausslemma2dlem1a  27641  2lgslem1a1  27665  2sqlem8a  27701  2sqlem8  27702  2sqcoprm  27711  2sqmod  27712  chto1ub  27752  vmadivsum  27758  dchrisumlem1  27765  dchrvmasumlem2  27774  dchrvmasumiflem1  27777  rpvmasum2  27788  mulog2sumlem2  27811  selberg2lem  27826  pntrmax  27840  pntpbnd1  27862  pntlemb  27873  pntlemj  27879  noextend  27942  cuteq0  28120  tgjustc1  28856  tgjustc2  28857  ercgrg  28899  motcgr  28918  tglineeltr  29018  colline  29037  miriso  29061  midexlem  29083  perpneq  29108  foot  29116  f1otrg  29367  axcontlem9  29469  uspgr1ewop  29748  nbupgrres  29864  structtocusgr  29946  wlkp1  30179  clwlkl1loop  30289  uspgrn2crct  30316  crctcshwlkn0lem5  30322  3trlond  30693  3pthond  30695  3spthond  30697  frgr3v  30795  vdgn1frgrv2  30816  numclwwlk3  30905  nmblolbii  31320  minvecolem3  31397  minvecolem4  31401  htthlem  31438  bcs2  31703  nmopub2tALT  32430  nmfnleub2  32447  eighmorth  32485  nmophmi  32552  nmopcoadji  32622  hstle  32751  atcvat3i  32917  opreu2reuALT  32992  prssad  33044  prssbd  33045  iinabrex  33082  disjxpin  33101  fmptco1f1o  33146  off2  33154  xppreima2  33164  fgreu  33184  suppovss  33193  1stpreimas  33218  padct  33229  resf1o  33241  fpwrelmap  33244  arginv  33258  argcj  33259  xrofsup  33278  eliccelico  33288  elicoelioo  33289  iocinif  33292  difioo  33293  suppssnn0  33316  elq2  33322  2exple2exp  33344  oexpled  33346  indsupp  33353  indfsid  33355  pfxlsw2ccat  33432  wrdt2ind  33435  ressprs  33446  xrge0addgt0  33497  xrge0adddir  33498  mndlactf1o  33510  mndractf1o  33511  gsumhashmul  33547  gsummulsubdishift1  33548  symgcom  33563  pmtrcnel  33569  pmtrcnel2  33570  pmtrcnelor  33571  cycpmfv2  33594  trsp2cyc  33603  cycpmco2lem7  33612  cyc3genpm  33632  cycpmconjslem2  33635  cyc3conja  33637  archirng  33668  archirngz  33669  rlocf1  33754  rlocisunit  33756  rrgsubm  33764  fracerl  33787  idomsubr  33790  linds2eq  33855  nsgqusf1olem3  33885  lidlunitel  33892  unitpidl1  33893  elrspunidl  33897  mxidlirredi  33915  mxidlirred  33916  qsdrngi  33938  qsdrnglem2  33939  dflring2  33944  rprmasso  33976  1arithidomlem2  33987  1arithufdlem4  33998  zringidom  34002  deg1le0eq0  34024  ply1unit  34026  ply1dg1rt  34031  ply1dg3rt0irred  34035  m1pmeq  34036  selvply1rhmlema  34069  selvply1rhmlem1  34071  evlextv  34093  mplvrpmrhm  34098  esplympl  34118  esplysply  34122  esplyind  34126  esplyindfv  34127  vietadeg1  34129  ply1degltdimlem  34173  ply1degltdim  34174  lindsunlem  34175  lbsdiflsp0  34177  fedgmullem1  34180  fedgmullem2  34181  assalactf1o  34186  ply1annprmidl  34258  minplyirredlem  34261  irngnminplynz  34263  minplyelirng  34266  algextdeglem4  34271  constrconj  34296  constrsqrtcl  34330  cos9thpiminplylem1  34333  cos9thpiminplylem2  34334  cos9thpinconstrlem1  34340  1smat1  34355  madjusmdetlem2  34379  qtophaus  34387  locfinref  34392  zarclssn  34424  zar0ring  34429  zarmxt1  34431  rhmpreimacnlem  34435  rhmpreimacn  34436  metideq  34444  sqsscirc2  34460  tpr2rico  34463  fmcncfil  34482  lmxrge0  34503  lmdvg  34504  qqhval2lem  34532  qqhf  34537  qqhnm  34541  esumle  34609  gsumesum  34610  esumlef  34613  esumrnmpt2  34619  esumpcvgval  34629  esum2d  34644  ofcf  34654  ldsysgenld  34712  ldgenpisyslem1  34715  unelros  34723  difelros  34724  inelsros  34730  diffiunisros  34731  imambfm  34814  omssubadd  34852  inelcarsg  34863  carsgsigalem  34867  carsggect  34870  carsgclctunlem2  34871  oddpwdc  34906  eulerpartlems  34912  eulerpartlemb  34920  eulerpartlemt  34923  iwrdsplit  34939  sseqf  34944  sseqfres  34945  ballotlemfc0  35045  ballotlemfcc  35046  ballotlemfrcn0  35082  signsplypnf  35099  signsvtn0  35119  signstfvneq0  35121  signsvtp  35132  signsvtn  35133  fsum2dsub  35156  reprlt  35168  hashreprin  35169  reprgt  35170  reprpmtf1o  35175  chtvalz  35178  breprexplema  35179  breprexplemc  35181  breprexp  35182  circlemeth  35189  logdivsqrle  35199  hgt750lemb  35205  lpadlem3  35230  lpadleft  35235  bnj1536  35404  bnj1001  35509  bnj1280  35570  fineqvnttrclselem2  35709  satffunlem1  36087  satffunlem2  36088  elmrsubrn  36200  neibastop3  37066  finxpsuclem  38234  poimirlem16  38468  poimirlem19  38471  poimirlem20  38472  poimirlem29  38481  mblfinlem3  38491  itg2addnclem3  38505  ftc1cnnclem  38523  lautlt  41062  lautcvr  41063  lauteq  41066  lautco  41068  ltrncl  41096  ltrncnvleN  41101  trljat2  41138  cdlemc6  41167  cdleme20c  41282  cdleme20j  41289  cdleme22e  41315  cdleme22eALTN  41316  cdlemg7aN  41596  cdlemg12e  41618  cdlemg17dALTN  41635  cdlemh  41788  cdlemkfid1N  41892  dibglbN  42137  diblss  42141  diclspsn  42165  dih1  42257  dihglbcpreN  42271  dihmeetlem4preN  42277  lcfrlem19  42532  aks4d1p8d1  43048  fsuppind  43534  mapfzcons  43659  mzpcl34  43674  mzpindd  43689  mzpsubst  43691  diophrw  43702  diophren  43752  irrapxlem1  43761  pellexlem5  43772  acongrep  43919  pwssplit4  44028  omlimcl2  44181  onexoegt  44183  oasubex  44225  omlim2  44238  nnoeomeqom  44251  nnawordexg  44266  succlg  44267  oacl2g  44269  onmcl  44270  omabs2  44271  omcl2  44272  tfsconcatrev  44287  ofoafg  44293  ofoaf  44294  ofoaass  44299  naddcnfass  44308  naddwordnexlem4  44340  omssrncard  44478  brtrclfv2  44665  rfovcnvf1od  44942  ntrk0kbimka  44977  isotone1  44986  isotone2  44987  4an4132  45420  modelaxrep  45902  mulltgt0  45954  fnchoice  45961  3adantlr3  45972  3adantll2  45973  3adantll3  45974  uzwo4  45985  disjf1o  46121  supxrgelem  46265  infleinflem2  46298  xrralrecnnle  46310  supxrunb3  46326  unb2ltle  46341  infrpgernmpt  46391  iooiinicc  46470  iooiinioc  46484  fmuldfeq  46511  mccl  46526  limccog  46548  limcrecl  46557  lptioo1  46560  islpcn  46565  limsupre  46567  neglimc  46573  0ellimcdiv  46575  limclner  46577  climleltrp  46602  climinf3  46642  liminflimsupclim  46733  xlimpnfxnegmnf  46740  icccncfext  46813  fprodcncf  46826  dvnmptdivc  46864  dvnmul  46869  dvmptfprod  46871  dvnprodlem3  46874  stoweidlem25  46951  stoweidlem34  46960  stoweidlem38  46964  stoweidlem44  46970  stoweidlem48  46974  stoweidlem49  46975  stoweidlem59  46985  stoweidlem60  46986  wallispilem4  46994  stirlinglem5  47004  dirkercncflem2  47030  fourierdlem39  47072  fourierdlem42  47075  fourierdlem46  47078  fourierdlem47  47079  fourierdlem48  47080  fourierdlem50  47082  fourierdlem51  47083  fourierdlem64  47096  fourierdlem73  47105  fourierdlem74  47106  fourierdlem77  47109  fourierdlem80  47112  fourierdlem87  47119  fourierdlem94  47126  fourierdlem103  47135  fourierdlem104  47136  etransclem32  47192  rrxsnicc  47226  sge0cl  47307  sge0f1o  47308  nnfoctbdjlem  47381  ismeannd  47393  omeiunltfirp  47445  ovncvrrp  47490  hoidmvlelem2  47522  hoidmvlelem5  47525  hspdifhsp  47542  hoiqssbllem2  47549  hspmbllem2  47553  vonicclem2  47610  smflimsuplem7  47752  tmachlem-agreeprod  47863  fundcmpsurbijinj  48408  sqrtpwpw2p  48539  lincresunit2  49506  nnpw2pmod  49611  dignn0flhalflem1  49643  dignn0flhalf  49646  rrx2linest  49770  itsclc0yqsol  49792  itsclc0b  49800  brab2dd  49854  oppcendc  50042  imaidfu  50134  imasubc  50175  oppcthinendcALT  50465  functhinclem1  50468  functhinclem2  50469  fullthinc2  50475