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  3580  wereu2  5621  frpomin  6298  funtpg  6547  funcnvtp  6555  funcnvqp  6556  fnund  6607  fun2d  6698  fvun1  6925  iinpreima  7015  ftpg  7103  fsnunf  7133  f1prex  7232  soisores  7275  isotr  7284  off  7642  coof  7648  caofrss  7663  caonncan  7668  fvmpocurryd  8214  oaf1o  8491  omeulem1  8510  oeordi  8516  oelimcl  8529  oeeulem  8530  oeeui  8531  oaabs2  8578  omabs  8580  coflton  8600  pmresg  8811  ralxpmap  8837  domunsncan  9008  sucdom2  9130  unxpdom2  9163  sucxpdom  9164  unblem4  9198  fodomfi  9215  fodomfiOLD  9233  hartogslem1  9450  cantnflt  9584  cantnflem3  9603  cantnflem4  9604  cnfcomlem  9611  cnfcom  9612  ttrcltr  9628  infxpenlem  9926  infxpenc  9931  fseqenlem1  9937  pwsdompw  10116  cfeq0  10169  cofsmo  10182  cfsmolem  10183  ssfin4  10223  hsmexlem4  10342  hsmexlem5  10343  axdc3lem2  10364  fpwwe2  10557  wunpr  10623  mulclpi  10807  mulcanenq  10874  distrlem4pr  10940  prlem934  10947  prlem936  10961  divge0d  13017  elfzodif0  13716  elfznelfzob  13720  seqcaopr2  13991  facavg  14254  swrdwrdsymb  14616  cats1un  14674  f1oun2prg  14870  sqrtdiv  15218  sqrtdivd  15377  mulcn2  15549  o1of2  15566  fsumsplit  15694  sumsplit  15721  isumless  15801  demoivreALT  16159  rpnnen2lem11  16182  gcdnncl  16467  qredeu  16618  rpdvds  16620  isprm5  16668  rpexp  16683  prmdvdsbc  16687  divnumden  16709  divdenle  16710  phimullem  16740  phisum  16752  pythagtriplem4  16781  pythagtriplem8  16785  pythagtriplem9  16786  pcgcd1  16839  sumhash  16858  fldivp1  16859  pockthlem  16867  setsfun  17132  setsfun0  17133  ssc2  17780  estrreslem1  18094  tleile  18376  chnind  18578  sgrppropd  18690  mndpropd  18718  grpidssd  18983  grpinvssd  18984  issubg2  19108  isnsg3  19126  eqgid  19146  kerf1ghm  19213  ghmqusnsglem1  19246  ghmquskerlem1  19249  ghmqusker  19253  gass  19267  symgextres  19391  gsmsymgreqlem2  19397  sylow1lem5  19568  sylow2alem2  19584  sylow3lem3  19595  efgredlemd  19710  efgredlem  19713  frgpnabllem1  19839  frgpnabllem2  19840  subgdmdprd  20002  ablfacrplem  20033  omndmul3  20100  gsumle  20111  rglcom4d  20183  issrngd  20823  orngmul  20833  lmodprop2d  20910  lsspropd  21004  pwssplit1  21046  lspvadd  21083  rhmpreimaidl  21267  znidomb  21551  znrrg  21555  lindfind  21806  lindsind  21807  mplsubglem  21987  mplind  22058  evlsvvval  22081  ressply1evl  22345  mat1ghm  22458  mdetunilem1  22587  mdetunilem3  22589  mdetunilem4  22590  mdetunilem9  22595  cramerimplem2  22659  mat2pmatlin  22710  monmatcollpw  22754  cpmadugsumlemF  22851  mretopd  23067  neiptopnei  23107  neitr  23155  ufilen  23905  flimrest  23958  flimclslem  23959  fclsrest  23999  cnextcn  24042  haustsms2  24112  tsmsxplem2  24129  trust  24204  utoptop  24209  restutop  24212  ustuqtop4  24219  utopsnneiplem  24222  utop2nei  24225  utop3cls  24226  isucn2  24253  ucncn  24259  fmucnd  24266  trcfilu  24268  comet  24488  metustexhalf  24531  metustbl  24541  psmetutop  24542  nrmmetd  24549  reconnlem1  24802  reconnlem2  24803  fsumcn  24847  cmetcaulem  25265  iscmet3lem1  25268  iscmet3lem2  25269  bcthlem5  25305  cmslsschl  25354  rrxdstprj1  25386  minveclem4  25409  ovolfiniun  25478  itg1addlem4  25676  itg1addlem5  25677  itgsplitioo  25815  c1liplem1  25973  dvfsumlem1  26003  plyeq0lem  26185  quotcan  26286  psercnlem1  26403  cxplea  26673  birthdaylem3  26930  musumsum  27169  mpodvdsmulf1o  27171  dvdsmulf1o  27173  dchrelbas4  27220  dchrhash  27248  gausslemma2dlem0d  27336  gausslemma2dlem1a  27342  2lgslem1a1  27366  2sqlem8a  27402  2sqlem8  27403  2sqcoprm  27412  2sqmod  27413  chto1ub  27453  vmadivsum  27459  dchrisumlem1  27466  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  rpvmasum2  27489  mulog2sumlem2  27512  selberg2lem  27527  pntrmax  27541  pntpbnd1  27563  pntlemb  27574  pntlemj  27580  noextend  27644  cuteq0  27821  tgjustc1  28557  tgjustc2  28558  ercgrg  28599  motcgr  28618  tglineeltr  28713  colline  28731  miriso  28752  midexlem  28774  perpneq  28796  foot  28804  f1otrg  28953  axcontlem9  29055  uspgr1ewop  29331  nbupgrres  29447  structtocusgr  29529  wlkp1  29763  clwlkl1loop  29866  uspgrn2crct  29891  crctcshwlkn0lem5  29897  3trlond  30258  3pthond  30260  3spthond  30262  frgr3v  30360  vdgn1frgrv2  30381  numclwwlk3  30470  nmblolbii  30885  minvecolem3  30962  minvecolem4  30966  htthlem  31003  bcs2  31268  nmopub2tALT  31995  nmfnleub2  32012  eighmorth  32050  nmophmi  32117  nmopcoadji  32187  hstle  32316  atcvat3i  32482  opreu2reuALT  32561  prssad  32614  prssbd  32615  iinabrex  32654  disjxpin  32673  fmptco1f1o  32721  off2  32729  xppreima2  32739  fgreu  32759  suppovss  32769  1stpreimas  32794  padct  32806  resf1o  32818  fpwrelmap  32821  arginv  32835  argcj  32836  xrofsup  32855  eliccelico  32865  elicoelioo  32866  iocinif  32869  difioo  32870  suppssnn0  32893  hashpss  32897  elq2  32900  sgnsub  32925  2exple2exp  32933  oexpled  32935  indsupp  32942  indfsid  32944  ccatf1  33024  pfxlsw2ccat  33025  wrdt2ind  33028  ressprs  33041  xrge0addgt0  33092  xrge0adddir  33093  mndlactf1o  33105  mndractf1o  33106  gsumhashmul  33143  gsummulsubdishift1  33144  symgcom  33159  pmtrcnel  33165  pmtrcnel2  33166  pmtrcnelor  33167  cycpmfv2  33190  trsp2cyc  33199  cycpmco2lem7  33208  cyc3genpm  33228  cycpmconjslem2  33231  cyc3conja  33233  archirng  33264  archirngz  33265  rlocf1  33349  rrgsubm  33360  fracerl  33382  idomsubr  33385  linds2eq  33456  nsgqusf1olem3  33490  lidlunitel  33498  unitpidl1  33499  elrspunidl  33503  drngidl  33508  isprmidlc  33522  qsidomlem1  33527  qsidomlem2  33528  qsnzr  33530  mxidlirredi  33546  mxidlirred  33547  qsdrngi  33570  qsdrnglem2  33571  rprmasso  33600  1arithidomlem2  33611  1arithufdlem4  33622  zringidom  33626  deg1le0eq0  33648  ply1unit  33650  ply1dg1rt  33655  ply1dg3rt0irred  33659  m1pmeq  33660  evlextv  33701  mplvrpmrhm  33706  esplympl  33726  esplysply  33730  esplyind  33734  esplyindfv  33735  vietadeg1  33737  ply1degltdimlem  33782  ply1degltdim  33783  lindsunlem  33784  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  assalactf1o  33795  ply1annprmidl  33867  minplyirredlem  33870  irngnminplynz  33872  minplyelirng  33875  algextdeglem4  33880  constrconj  33905  constrsqrtcl  33939  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpinconstrlem1  33949  1smat1  33964  madjusmdetlem2  33988  qtophaus  33996  locfinref  34001  zarclssn  34033  zar0ring  34038  zarmxt1  34040  rhmpreimacnlem  34044  rhmpreimacn  34045  metideq  34053  sqsscirc2  34069  tpr2rico  34072  fmcncfil  34091  lmxrge0  34112  lmdvg  34113  qqhval2lem  34141  qqhf  34146  qqhnm  34150  esumle  34218  gsumesum  34219  esumlef  34222  esumrnmpt2  34228  esumpcvgval  34238  esum2d  34253  ofcf  34263  ldsysgenld  34320  ldgenpisyslem1  34323  unelros  34331  difelros  34332  inelsros  34338  diffiunisros  34339  imambfm  34422  omssubadd  34460  inelcarsg  34471  carsgsigalem  34475  carsggect  34478  carsgclctunlem2  34479  oddpwdc  34514  eulerpartlems  34520  eulerpartlemb  34528  eulerpartlemt  34531  iwrdsplit  34547  sseqf  34552  sseqfres  34553  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemfrcn0  34690  plymulx0  34707  signsplypnf  34710  signsvtn0  34730  signstfvneq0  34732  signsvtp  34743  signsvtn  34744  fsum2dsub  34767  reprlt  34779  hashreprin  34780  reprgt  34781  reprpmtf1o  34786  chtvalz  34789  breprexplema  34790  breprexplemc  34792  breprexp  34793  circlemeth  34800  logdivsqrle  34810  hgt750lemb  34816  lpadlem3  34838  lpadleft  34843  bnj1536  35012  bnj1001  35117  bnj1280  35178  fineqvnttrclselem2  35282  satffunlem1  35605  satffunlem2  35606  elmrsubrn  35718  neibastop3  36560  finxpsuclem  37727  poimirlem16  37971  poimirlem19  37974  poimirlem20  37975  poimirlem29  37984  mblfinlem3  37994  itg2addnclem3  38008  ftc1cnnclem  38026  lautlt  40551  lautcvr  40552  lauteq  40555  lautco  40557  ltrncl  40585  ltrncnvleN  40590  trljat2  40627  cdlemc6  40656  cdleme20c  40771  cdleme20j  40778  cdleme22e  40804  cdleme22eALTN  40805  cdlemg7aN  41085  cdlemg12e  41107  cdlemg17dALTN  41124  cdlemh  41277  cdlemkfid1N  41381  dibglbN  41626  diblss  41630  diclspsn  41654  dih1  41746  dihglbcpreN  41760  dihmeetlem4preN  41766  lcfrlem19  42021  aks4d1p8d1  42537  fsuppind  43037  mapfzcons  43162  mzpcl34  43177  mzpindd  43192  mzpsubst  43194  diophrw  43205  diophren  43259  irrapxlem1  43268  pellexlem5  43279  acongrep  43426  pwssplit4  43535  omlimcl2  43688  onexoegt  43690  oasubex  43732  omlim2  43745  nnoeomeqom  43758  nnawordexg  43773  succlg  43774  oacl2g  43776  onmcl  43777  omabs2  43778  omcl2  43779  tfsconcatrev  43794  ofoafg  43800  ofoaf  43801  ofoaass  43806  naddcnfass  43815  naddwordnexlem4  43847  omssrncard  43985  brtrclfv2  44172  rfovcnvf1od  44449  ntrk0kbimka  44484  isotone1  44493  isotone2  44494  4an4132  44944  modelaxrep  45426  mulltgt0  45471  fnchoice  45478  3adantlr3  45489  3adantll2  45490  3adantll3  45491  uzwo4  45502  disjf1o  45639  supxrgelem  45785  infleinflem2  45818  xrralrecnnle  45830  supxrunb3  45846  unb2ltle  45861  infrpgernmpt  45911  iooiinicc  45990  iooiinioc  46004  fmuldfeq  46031  mccl  46046  limccog  46068  limcrecl  46077  lptioo1  46080  islpcn  46085  limsupre  46087  neglimc  46093  0ellimcdiv  46095  limclner  46097  climleltrp  46122  climinf3  46162  liminflimsupclim  46253  xlimpnfxnegmnf  46260  icccncfext  46333  fprodcncf  46346  dvnmptdivc  46384  dvnmul  46389  dvmptfprod  46391  dvnprodlem3  46394  stoweidlem25  46471  stoweidlem34  46480  stoweidlem38  46484  stoweidlem44  46490  stoweidlem48  46494  stoweidlem49  46495  stoweidlem59  46505  stoweidlem60  46506  wallispilem4  46514  stirlinglem5  46524  dirkercncflem2  46550  fourierdlem39  46592  fourierdlem42  46595  fourierdlem46  46598  fourierdlem47  46599  fourierdlem48  46600  fourierdlem50  46602  fourierdlem51  46603  fourierdlem64  46616  fourierdlem73  46625  fourierdlem74  46626  fourierdlem77  46629  fourierdlem80  46632  fourierdlem87  46639  fourierdlem94  46646  fourierdlem103  46655  fourierdlem104  46656  etransclem32  46712  rrxsnicc  46746  sge0cl  46827  sge0f1o  46828  nnfoctbdjlem  46901  ismeannd  46913  omeiunltfirp  46965  ovncvrrp  47010  hoidmvlelem2  47042  hoidmvlelem5  47045  hspdifhsp  47062  hoiqssbllem2  47069  hspmbllem2  47073  vonicclem2  47130  smflimsuplem7  47272  fundcmpsurbijinj  47882  sqrtpwpw2p  48013  lincresunit2  48966  nnpw2pmod  49071  dignn0flhalflem1  49103  dignn0flhalf  49106  rrx2linest  49230  itsclc0yqsol  49252  itsclc0b  49260  brab2dd  49315  oppcendc  49505  imaidfu  49597  imasubc  49638  oppcthinendcALT  49928  functhinclem1  49931  functhinclem2  49932  fullthinc2  49938