Theorem syl21anc 836

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syl1111anc  838  wereu2  5516  funtpg  6379  funcnvtp  6387  funcnvqp  6388  fnund  6435  fun2d  6516  fvun1  6729  iinpreima  6814  ftpg  6895  fsnunf  6924  f1prex  7018  soisores  7059  isotr  7068  off  7404  caofrss  7422  caonncan  7427  fvmpocurryd  7920  oaf1o  8172  omeulem1  8191  oeordi  8196  oelimcl  8209  oeeulem  8210  oeeui  8211  oaabs2  8255  omabs  8257  pmresg  8417  ralxpmap  8443  domunsncan  8600  sucdom2  8610  unxpdom2  8710  sucxpdom  8711  unblem4  8757  fodomfi  8781  hartogslem1  8990  cantnflt  9119  cantnflem3  9138  cantnflem4  9139  cnfcomlem  9146  cnfcom  9147  infxpenlem  9424  infxpenc  9429  fseqenlem1  9435  pwsdompw  9615  cfeq0  9667  cofsmo  9680  cfsmolem  9681  ssfin4  9721  hsmexlem4  9840  hsmexlem5  9841  axdc3lem2  9862  fpwwe2  10054  wunpr  10120  mulclpi  10304  mulcanenq  10371  distrlem4pr  10437  prlem934  10444  prlem936  10458  divge0d  12459  elfznelfzob  13138  seqcaopr2  13402  facavg  13657  swrdwrdsymb  14015  cats1un  14074  f1oun2prg  14270  sqrtdiv  14617  sqrtdivd  14775  mulcn2  14944  o1of2  14961  fsumsplit  15089  sumsplit  15115  isumless  15192  demoivreALT  15546  rpnnen2lem11  15569  gcdnncl  15846  qredeu  15992  rpdvds  15994  isprm5  16041  rpexp  16054  divnumden  16078  divdenle  16079  phimullem  16106  phisum  16117  pythagtriplem4  16146  pythagtriplem8  16150  pythagtriplem9  16151  pcgcd1  16203  sumhash  16222  fldivp1  16223  pockthlem  16231  setsfun  16510  setsfun0  16511  ssc2  17084  estrreslem1  17379  mndpropd  17928  grpidssd  18167  grpinvssd  18168  issubg2  18286  isnsg3  18304  eqgid  18324  gass  18423  symgextres  18545  gsmsymgreqlem2  18551  sylow1lem5  18719  sylow2alem2  18735  sylow3lem3  18746  efgredlemd  18862  efgredlem  18865  frgpnabllem1  18986  frgpnabllem2  18987  subgdmdprd  19149  ablfacrplem  19180  kerf1ghm  19491  issrngd  19625  lmodprop2d  19689  lsspropd  19782  pwssplit1  19824  lspvadd  19861  znidomb  20253  znrrg  20257  lindfind  20505  lindsind  20506  mplsubglem  20672  mplind  20741  mat1ghm  21088  mdetunilem1  21217  mdetunilem3  21219  mdetunilem4  21220  mdetunilem9  21225  cramerimplem2  21289  mat2pmatlin  21340  monmatcollpw  21384  cpmadugsumlemF  21481  mretopd  21697  neiptopnei  21737  neitr  21785  ufilen  22535  flimrest  22588  flimclslem  22589  fclsrest  22629  cnextcn  22672  haustsms2  22742  tsmsxplem2  22759  trust  22835  utoptop  22840  restutop  22843  ustuqtop4  22850  utopsnneiplem  22853  utop2nei  22856  utop3cls  22857  isucn2  22885  ucncn  22891  fmucnd  22898  trcfilu  22900  comet  23120  metustexhalf  23163  metustbl  23173  psmetutop  23174  nrmmetd  23181  reconnlem1  23431  reconnlem2  23432  fsumcn  23475  cmetcaulem  23892  iscmet3lem1  23895  iscmet3lem2  23896  bcthlem5  23932  cmslsschl  23981  rrxdstprj1  24013  minveclem4  24036  ovolfiniun  24105  itg1addlem4  24303  itg1addlem5  24304  itgsplitioo  24441  c1liplem1  24599  dvfsumlem1  24629  plyeq0lem  24807  quotcan  24905  psercnlem1  25020  cxplea  25287  birthdaylem3  25539  musumsum  25777  dvdsmulf1o  25779  dchrelbas4  25827  dchrhash  25855  gausslemma2dlem0d  25943  gausslemma2dlem1a  25949  2lgslem1a1  25973  2sqlem8a  26009  2sqlem8  26010  2sqcoprm  26019  2sqmod  26020  chto1ub  26060  vmadivsum  26066  dchrisumlem1  26073  dchrvmasumlem2  26082  dchrvmasumiflem1  26085  rpvmasum2  26096  mulog2sumlem2  26119  selberg2lem  26134  pntrmax  26148  pntpbnd1  26170  pntlemb  26181  pntlemj  26187  tgjustc1  26269  tgjustc2  26270  ercgrg  26311  motcgr  26330  tglineeltr  26425  colline  26443  miriso  26464  midexlem  26486  perpneq  26508  foot  26516  f1otrg  26665  axcontlem9  26766  uspgr1ewop  27038  nbupgrres  27154  structtocusgr  27236  wlkp1  27471  clwlkl1loop  27572  uspgrn2crct  27594  crctcshwlkn0lem5  27600  3trlond  27958  3pthond  27960  3spthond  27962  frgr3v  28060  vdgn1frgrv2  28081  numclwwlk3  28170  nmblolbii  28582  minvecolem3  28659  minvecolem4  28663  htthlem  28700  bcs2  28965  nmopub2tALT  29692  nmfnleub2  29709  eighmorth  29747  nmophmi  29814  nmopcoadji  29884  hstle  30013  atcvat3i  30179  opreu2reuALT  30247  iinabrex  30332  disjxpin  30351  fmptco1f1o  30392  off2  30402  xppreima2  30413  fgreu  30435  suppovss  30443  1stpreimas  30465  padct  30481  resf1o  30492  fpwrelmap  30495  xrofsup  30518  eliccelico  30526  elicoelioo  30527  iocinif  30530  difioo  30531  prmdvdsbc  30558  ccatf1  30651  pfxlsw2ccat  30652  wrdt2ind  30653  ressprs  30668  tleile  30674  xrge0addgt0  30725  xrge0adddir  30726  gsumhashmul  30741  omndmul3  30764  gsumle  30775  symgcom  30777  pmtrcnel  30783  pmtrcnel2  30784  pmtrcnelor  30785  cycpmfv2  30806  trsp2cyc  30815  cycpmco2lem7  30824  cyc3genpm  30844  cycpmconjslem2  30847  cyc3conja  30849  archirng  30867  archirngz  30868  orngmul  30927  linds2eq  30995  rhmpreimaidl  31011  elrspunidl  31014  isprmidlc  31031  qsidomlem1  31036  qsidomlem2  31037  lindsunlem  31108  lbsdiflsp0  31110  fedgmullem1  31113  fedgmullem2  31114  1smat1  31157  madjusmdetlem2  31181  qtophaus  31189  locfinref  31194  zarclssn  31226  zar0ring  31231  zarmxt1  31233  rhmpreimacnlem  31237  rhmpreimacn  31238  metideq  31246  sqsscirc2  31262  tpr2rico  31265  fmcncfil  31284  lmxrge0  31305  lmdvg  31306  qqhval2lem  31332  qqhf  31337  qqhnm  31341  esumle  31427  gsumesum  31428  esumlef  31431  esumrnmpt2  31437  esumpcvgval  31447  esum2d  31462  ofcf  31472  ldsysgenld  31529  ldgenpisyslem1  31532  unelros  31540  difelros  31541  inelsros  31547  diffiunisros  31548  imambfm  31630  omssubadd  31668  inelcarsg  31679  carsgsigalem  31683  carsggect  31686  carsgclctunlem2  31687  oddpwdc  31722  eulerpartlems  31728  eulerpartlemb  31736  eulerpartlemt  31739  iwrdsplit  31755  sseqf  31760  sseqfres  31761  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemfrcn0  31897  sgnsub  31912  plymulx0  31927  signsplypnf  31930  signsvtn0  31950  signstfvneq0  31952  signsvtp  31963  signsvtn  31964  fsum2dsub  31988  reprlt  32000  hashreprin  32001  reprgt  32002  reprpmtf1o  32007  chtvalz  32010  breprexplema  32011  breprexplemc  32013  breprexp  32014  circlemeth  32021  logdivsqrle  32031  hgt750lemb  32037  lpadlem3  32059  lpadleft  32064  bnj1536  32236  bnj1001  32341  bnj1280  32402  cvxsconn  32603  satffunlem1  32767  satffunlem2  32768  elmrsubrn  32880  frpomin  33191  noextend  33286  neibastop3  33823  finxpsuclem  34814  poimirlem16  35073  poimirlem19  35076  poimirlem20  35077  poimirlem29  35086  mblfinlem3  35096  itg2addnclem3  35110  ftc1cnnclem  35128  lautlt  37387  lautcvr  37388  lauteq  37391  lautco  37393  ltrncl  37421  ltrncnvleN  37426  trljat2  37463  cdlemc6  37492  cdleme20c  37607  cdleme20j  37614  cdleme22e  37640  cdleme22eALTN  37641  cdlemg7aN  37921  cdlemg12e  37943  cdlemg17dALTN  37960  cdlemh  38113  cdlemkfid1N  38217  dibglbN  38462  diblss  38466  diclspsn  38490  dih1  38582  dihglbcpreN  38596  dihmeetlem4preN  38602  lcfrlem19  38857  fsuppind  39456  mapfzcons  39657  mzpcl34  39672  mzpindd  39687  mzpsubst  39689  diophrw  39700  diophren  39754  irrapxlem1  39763  pellexlem5  39774  acongrep  39921  pwssplit4  40033  brtrclfv2  40428  rfovcnvf1od  40705  ntrk0kbimka  40742  isotone1  40751  isotone2  40752  4an4132  41205  mulltgt0  41651  fnchoice  41658  3adantlr3  41670  3adantll2  41672  3adantll3  41673  uzwo4  41687  disjf1o  41818  supxrgelem  41969  infleinflem2  42003  xrralrecnnle  42017  supxrunb3  42036  unb2ltle  42052  infrpgernmpt  42104  iooiinicc  42179  iooiinioc  42193  fmuldfeq  42225  mccl  42240  limccog  42262  limcrecl  42271  lptioo1  42274  islpcn  42281  limsupre  42283  neglimc  42289  0ellimcdiv  42291  limclner  42293  climleltrp  42318  climinf3  42358  liminflimsupclim  42449  xlimpnfxnegmnf  42456  icccncfext  42529  fprodcncf  42542  dvnmptdivc  42580  dvnmul  42585  dvmptfprod  42587  dvnprodlem3  42590  stoweidlem25  42667  stoweidlem34  42676  stoweidlem38  42680  stoweidlem44  42686  stoweidlem48  42690  stoweidlem49  42691  stoweidlem59  42701  stoweidlem60  42702  wallispilem4  42710  stirlinglem5  42720  dirkercncflem2  42746  fourierdlem39  42788  fourierdlem42  42791  fourierdlem46  42794  fourierdlem47  42795  fourierdlem48  42796  fourierdlem50  42798  fourierdlem51  42799  fourierdlem64  42812  fourierdlem73  42821  fourierdlem74  42822  fourierdlem77  42825  fourierdlem80  42828  fourierdlem87  42835  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  etransclem32  42908  rrxsnicc  42942  sge0cl  43020  sge0f1o  43021  nnfoctbdjlem  43094  ismeannd  43106  omeiunltfirp  43158  hoicvr  43187  ovncvrrp  43203  hoidmvlelem2  43235  hoidmvlelem5  43238  hspdifhsp  43255  hoiqssbllem2  43262  hspmbllem2  43266  vonicclem2  43323  smflimsuplem7  43457  fundcmpsurbijinj  43927  sqrtpwpw2p  44055  isomgrref  44353  lincresunit2  44887  nnpw2pmod  44997  dignn0flhalflem1  45029  dignn0flhalf  45032  rrx2linest  45156  itsclc0yqsol  45178  itsclc0b  45186