Theorem syl22anc 835

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl22anc.5	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl22anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 510	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 833	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  preqsnd  4858  fr2nr  5653  soltmin  6136  f1oprg  6877  f1prex  7284  fveqf1o  7303  weniso  7353  fr3nr  7761  suppofssd  8190  smogt  8369  smocdmdom  8370  oacomf1o  8567  en2prd  9050  enpr2dOLD  9052  difsnen  9055  undomOLD  9062  enfixsn  9083  domss2  9138  ssenen  9153  marypha1lem  9430  fisupcl  9466  ordtypelem3  9517  ordtypelem8  9522  oieu  9536  oismo  9537  wofib  9542  wemaplem2  9544  wemapso  9548  wemapso2lem  9549  unxpwdom2  9585  infdifsn  9654  oemapvali  9681  cantnflem1c  9684  cantnflem1  9686  cantnf  9690  cnfcom3  9701  r1ordg  9775  dif1card  10007  infxpenlem  10010  dfac8clem  10029  infxp  10212  infmap2  10215  cflim2  10260  coftr  10270  fin2i2  10315  enfin2i  10318  fin23lem26  10322  fin23lem27  10325  fin23lem40  10348  isf32lem2  10351  isf32lem3  10352  isf32lem4  10353  isf32lem7  10356  isf32lem9  10358  fin1a2lem13  10409  fin12  10410  alephexp1  10576  gchdomtri  10626  fpwwe2lem11  10638  fpwwe2lem12  10639  gchpwdom  10667  gchhar  10676  adderpqlem  10951  mulerpqlem  10952  addassnq  10955  mulassnq  10956  distrnq  10958  mulidnq  10960  recmulnq  10961  ltexnq  10972  distrlem1pr  11022  distrlem4pr  11023  prlem936  11044  reclem3pr  11046  mulcmpblnr  11068  mulgt0d  11373  mul4d  11430  add4d  11446  add42d  11447  subcan  11519  addsub4d  11622  subadd4d  11623  sub4d  11624  2addsubd  11625  addsubeq4d  11626  muladdd  11676  mulsubd  11677  addgegt0d  11791  addgtge0d  11792  addge0d  11794  mulge0d  11795  le2addd  11837  le2subd  11838  ltleaddd  11839  leltaddd  11840  lt2subd  11842  divdivdiv  11919  divcan5  11920  divne0d  12010  recdivd  12011  recdiv2d  12012  divcan6d  12013  ddcand  12014  rec11d  12015  divmuldivd  12035  divmul13d  12036  divmul24d  12037  divadddivd  12038  divsubdivd  12039  divmuleqd  12040  divdivdivd  12041  subrecd  12049  mulge0b  12088  recreclt  12117  divgt0d  12153  mulgt1d  12154  lemulge11d  12155  lemulge12d  12156  ltmul12ad  12159  lemul12ad  12160  lemul12bd  12161  supmul1  12187  nndivtr  12263  qreccl  12957  ledivdivd  13045  lediv12ad  13079  lt2mul2divd  13089  xlt2add  13243  supxrun  13299  supxrre  13310  infxrre  13319  elicore  13380  iccss2  13399  iccssico2  13402  lincmb01cmp  13476  iccf1o  13477  fzrev2i  13570  2tnp1ge0ge0  13798  m1modnnsub1  13886  modaddmodup  13903  modaddmodlo  13904  modsubdir  13909  fzennn  13937  sermono  14004  mulexpz  14072  expaddz  14076  sqdiv  14090  expsubd  14126  ltexp2a  14135  expmordi  14136  leexp2a  14141  expmulnbnd  14202  digit1  14204  lt2sqd  14223  le2sqd  14224  sq11d  14225  bcm1k  14279  bcp1n  14280  bcp1nk  14281  hashf1lem1  14419  hashf1lem1OLD  14420  cshw1  14776  2swrd2eqwrdeq  14908  ofccat  14920  absrele  15259  sqreulem  15310  sqrtmuld  15375  sqrtsq2d  15376  sqrtled  15377  sqrtltd  15378  sqr11d  15379  abs3lemd  15412  rlimuni  15498  climuni  15500  lo1resb  15512  o1resb  15514  2clim  15520  addcn2  15542  mulcn2  15544  o1of2  15561  o1rlimmul  15567  lo1add  15575  lo1mul  15576  isercolllem1  15615  caucvgrlem  15623  iseraltlem2  15633  iseraltlem3  15634  mptfzshft  15728  fsumrev  15729  fsum0diag2  15733  binomlem  15779  climcndslem1  15799  climcndslem2  15800  harmonic  15809  mertenslem1  15834  fprodser  15897  fprodrev  15925  efcllem  16025  moddvds  16212  dvds1  16266  dvdsext  16268  evennn2n  16298  bitsinv1  16387  sadaddlem  16411  sadasslem  16415  sadeq  16417  mulgcd  16494  dvdssqlem  16507  lcmftp  16577  rpmulgcd2  16597  coprmproddvdslem  16603  isprm5  16648  isprm6  16655  crth  16715  eulerthlem2  16719  prmdiveq  16723  pythagtriplem11  16762  pythagtriplem13  16764  pcgcd1  16814  pcprmpw2  16819  pcaddlem  16825  fldivp1  16834  4sqlem12  16893  4sqlem14  16895  4sqlem15  16896  4sqlem16  16897  vdwapun  16911  mreexexlem4d  17595  acsfn1  17609  acsfn2  17611  sscpwex  17766  rescabs  17786  rescabsOLD  17787  yonedainv  18238  subm0  18732  pmtrfb  19374  psgnunilem1  19402  odmodnn0  19449  odeq  19459  dfod2  19473  sylow1lem1  19507  lsmsubg  19563  lsmmod  19584  lsmdisj2  19591  ghmplusg  19755  odadd  19759  gexexlem  19761  lt6abl  19804  cyggex2  19806  dprdfinv  19930  dmdprdsplitlem  19948  dpjidcl  19969  ablfacrp  19977  ablfacrp2  19978  ablfac1c  19982  ablfac1eu  19984  acsfn1p  20558  lcomfsupp  20656  lssvancl1  20699  lssvnegcl  20711  lspprvacl  20754  lspsneli  20756  lspsn  20757  lmhmplusg  20799  lmhmima  20802  lmhmpreima  20803  reslmhm  20807  lbsind2  20836  lsmcl  20838  lsmelval2  20840  lsppreli  20845  lspprabs  20850  pj1lmhm  20855  lssvs0or  20868  lspabs3  20879  lspfixed  20886  lspexch  20887  lsmcv  20899  lspsolv  20901  drngnidl  21003  rngqiprngimfo  21060  rngqiprngfulem4  21073  gzrngunit  21211  zringlpirlem3  21235  prmirredlem  21243  znf1o  21326  znunithash  21339  frlmsubgval  21539  frlmvplusgvalc  21541  frlmvscaval  21542  frlmphllem  21554  frlmphl  21555  frlmssuvc1  21568  frlmsslsp  21570  frlmup1  21572  frlmup2  21573  lindfind2  21592  lindfrn  21595  f1lindf  21596  islindf4  21612  mplbas2  21816  evlslem3  21862  evlslem1  21864  coe1addfv  22007  lply1binom  22050  evl1addd  22080  evl1subd  22081  evl1muld  22082  mamudi  22123  mamudir  22124  1marepvmarrepid  22297  mdetrlin  22324  smadiadetglem1  22393  smadiadetg  22395  cramerimplem1  22405  mat2pmatscmxcl  22462  m2pmfzgsumcl  22470  pmatcollpw  22503  pmatcollpwfi  22504  pmatcollpw3fi1lem1  22508  cpmidpmatlem2  22593  cpmadugsumlemF  22598  chcoeffeqlem  22607  ntrin  22785  topssnei  22848  restbas  22882  restntr  22906  cnntri  22995  fiuncmp  23128  nllyrest  23210  nllyidm  23213  hausllycmp  23218  cldllycmp  23219  hauspwdom  23225  txcld  23327  txcn  23350  txlly  23360  txnlly  23361  txhaus  23371  txlm  23372  txkgen  23376  xkococnlem  23383  cnmpt2res  23401  xkoinjcn  23411  basqtop  23435  qtopeu  23440  trfbas2  23567  neifil  23604  hausflim  23705  alexsubALTlem2  23772  cnextfval  23786  cnextfvval  23789  cnextf  23790  cnextfres  23793  clssubg  23833  utop2nei  23975  utop3cls  23976  utopreg  23977  psmetlecl  24041  xmetlecl  24072  prdsxmetlem  24094  bldisj  24124  imasf1obl  24217  prdsbl  24220  stdbdmet  24245  stdbdmopn  24247  met2ndci  24251  metcnp  24270  metustto  24282  metustexhalf  24285  cfilucfil  24288  metucn  24300  lssnlm  24438  nmotri  24476  nmoid  24479  tgioo  24532  blcvx  24534  xrsmopn  24548  reperflem  24554  reconnlem2  24563  opnreen  24567  metdsge  24585  metdsre  24589  metdscnlem  24591  metnrmlem1a  24594  metnrmlem1  24595  metnrmlem3  24597  cncfmet  24649  cnmpopc  24669  icopnfcnv  24687  icopnfhmeo  24688  cnllycmp  24702  evth  24705  lebnumii  24712  nmoleub2lem3  24862  iscfil2  25014  cfil3i  25017  iscfil3  25021  cfilfcls  25022  iscau3  25026  iscmet3lem2  25040  caubl  25056  lmcau  25061  cssbn  25123  rrxcph  25140  minveclem2  25174  pjthlem1  25185  pjthlem2  25186  ivthicc  25207  ovollecl  25232  ovolunlem1a  25245  ovolunnul  25249  ovoliunlem1  25251  ismbl2  25276  nulmbl2  25285  unmbl  25286  volun  25294  voliunlem2  25300  ioombl1lem2  25308  uniioombllem2a  25331  uniioombllem3  25334  uniioombllem4  25335  dyaddisjlem  25344  dyadmaxlem  25346  opnmbllem  25350  volsup2  25354  volcn  25355  ismbfd  25388  mbfi1fseqlem1  25465  mbfi1fseqlem5  25469  itg2lecl  25488  itg2monolem2  25501  itg2gt0  25510  itgspliticc  25586  ellimc3  25628  limcres  25635  dvfval  25646  dvres3  25662  dvres3a  25663  dvmptresicc  25665  dvnff  25673  dvnadd  25679  dvn2bss  25680  dvnres  25681  dvcmul  25695  dvcmulf  25696  dvmptres3  25708  dvmptres2  25714  dvmptntr  25723  dvexp3  25730  dvferm1lem  25736  dvlip  25745  dvlipcn  25746  dvlip2  25747  c1liplem1  25748  dvgt0lem1  25754  dvgt0lem2  25755  dvne0  25763  lhop1lem  25765  lhop2  25767  lhop  25768  dvcnvrelem1  25769  dvcnvrelem2  25770  dvcvx  25772  dvfsumle  25773  dvfsumabs  25775  dvfsumlem2  25779  ftc1lem6  25793  ftc1  25794  ftc2ditglem  25797  itgsubstlem  25800  itgpowd  25802  tdeglem4  25812  tdeglem4OLD  25813  mdegaddle  25827  mdegmullem  25831  ply1rem  25916  fta1glem2  25919  fta1blem  25921  ig1peu  25924  ig1pdvds  25929  dgrmulc  26021  dgrcolem1  26023  plydivlem4  26045  plydiveu  26047  fta1lem  26056  vieta1lem1  26059  vieta1lem2  26060  plyexmo  26062  taylfvallem1  26105  taylfval  26107  tayl0  26110  taylplem1  26111  taylply2  26116  taylply  26117  dvtaylp  26118  dvntaylp  26119  dvntaylp0  26120  taylthlem1  26121  taylthlem2  26122  ulmcaulem  26142  ulmcau  26143  ulmcn  26147  ulmdvlem1  26148  radcnvlem1  26161  radcnvle  26168  psercn  26174  pserdvlem2  26176  pserdv  26177  abelth  26189  tanregt0  26284  dvlog2lem  26396  efopn  26402  logtayllem  26403  logccv  26407  cxplt3  26444  cxpmul2zd  26460  cxpltd  26463  cxpled  26464  cxplt3d  26479  cxple3d  26480  dvsqrt  26486  cxpcn3  26492  cxpaddle  26496  cxpeq  26501  angcan  26543  angvald  26545  ang180lem2  26551  ang180  26555  isosctrlem3  26561  dquartlem1  26592  atantayl2  26679  leibpi  26683  log2tlbnd  26686  birthdaylem3  26694  xrlimcnp  26709  efrlim  26710  o1cxp  26715  jensenlem2  26728  jensen  26729  fsumharmonic  26752  lgamucov  26778  lgamcvg2  26795  wilthlem1  26808  basellem3  26823  basellem6  26826  basellem8  26828  ppisval  26844  chtwordi  26896  ppiwordi  26902  mumullem2  26920  dvdsmulf1o  26934  fsumvma  26952  fsumvma2  26953  chpchtsum  26958  chpub  26959  logfacubnd  26960  dchrmulcl  26988  dchrinv  27000  dchrptlem1  27003  dchrptlem2  27004  sumdchr2  27009  dchr2sum  27012  bposlem7  27029  lgslem1  27036  lgslem3  27038  lgsdirprm  27070  lgsqrlem2  27086  lgseisenlem1  27114  lgseisenlem2  27115  lgseisenlem4  27117  lgseisen  27118  lgsquadlem1  27119  lgsquad2lem1  27123  lgsquad3  27126  m1lgs  27127  2sqlem7  27163  2sq2  27172  2sqmod  27175  chebbnd1lem2  27209  chebbnd1lem3  27210  rplogsumlem1  27223  rpvmasumlem  27226  dchrvmasumlem1  27234  dchrvmasum2lem  27235  dchrvmasumlema  27239  dchrisum0flblem2  27248  dchrisum0fno1  27250  dchrisum0re  27252  logdivsum  27272  pntrsumbnd2  27306  pntpbnd1a  27324  pntpbnd1  27325  pntibndlem2  27330  pntlemr  27341  pntlemj  27342  pntlemf  27344  pnt2  27352  padicabv  27369  ostth2lem2  27373  sltrec  27558  madebday  27631  sltn0  27636  addsproplem6  27696  sleadd1  27711  negsproplem6  27746  mulsproplem13  27823  mulsproplem14  27824  sltmuld  27832  mulsgt0d  27840  f1otrg  28389  brbtwn2  28430  colinearalglem2  28432  axcgrtr  28440  axcgrid  28441  axsegconlem7  28448  axsegcon  28452  ax5seglem3  28456  ax5seglem6  28459  ax5seg  28463  axpaschlem  28465  axlowdimlem17  28483  axcontlem2  28490  axcontlem4  28492  axcontlem7  28495  axcontlem8  28496  ecgrtg  28508  usgredg2v  28751  vtxdgoddnumeven  29077  2trlond  29460  eupthp1  29736  nmobndi  30295  ubthlem2  30391  ubthlem3  30392  minvecolem2  30395  shuni  30820  pjhthlem1  30911  chscllem2  31158  pjcompi  31192  mayete3i  31248  unoplin  31440  hmoplin  31462  nmophmi  31551  mdslmd4i  31853  isoun  32190  xrge0addcld  32242  xrofsup  32247  eliccelico  32255  elicoelioo  32256  difioo  32260  rexdiv  32359  mgcmnt1d  32434  mgcmnt2d  32435  xrge0addgt0  32459  omndadd2d  32496  omndadd2rd  32497  omndmul2  32500  cycpmcl  32545  cycpm2tr  32548  cyc3evpm  32579  cycpmconjslem2  32584  freshmansdream  32651  fldgensdrg  32674  ofldchr  32702  qusker  32734  eqgvscpbl  32735  ringlsmss1  32780  ringlsmss2  32781  intlidl  32810  rhmpreimaidl  32811  lidlunitel  32815  elrspunidl  32820  idlinsubrg  32823  isprmidlc  32840  rhmpreimaprmidl  32844  qsidomlem1  32845  mxidlmaxv  32858  mxidlprm  32860  ssmxidllem  32863  opprmxidlabs  32875  qsdrnglem2  32884  resssra  32962  ply1degltdimlem  32995  lindsunlem  32997  finexttrb  33029  algextdeglem4  33065  algextdeglem8  33069  mdetpmtr2  33102  mdetpmtr12  33103  madjusmdetlem1  33105  madjusmdetlem4  33108  rhmpreimacn  33163  unitdivcld  33179  xrge0mulc1cn  33219  qqhnm  33268  esumcst  33359  esumfsup  33366  esumpmono  33375  esumcvg  33382  difelsiga  33429  sigapisys  33451  sigapildsys  33458  ldgenpisyslem1  33459  1stmbfm  33557  2ndmbfm  33558  dya2icoseg  33574  sibfinima  33636  probmeasb  33727  orvcgteel  33764  orvclteel  33769  ballotlemsima  33812  ballotlemfrceq  33825  sgnmul  33839  ccatmulgnn0dir  33851  fct2relem  33907  ftc2re  33908  chtvalz  33939  subfacp1lem2a  34469  subfaclim  34477  erdsze2lem2  34493  cvmliftlem2  34575  cvmliftlem10  34583  cvmliftlem13  34585  cvmliftiota  34590  cvmlift2lem9  34600  cvmlift2lem11  34602  cvmlift2lem12  34603  cvmliftphtlem  34606  cvmlift3lem6  34613  cvmlift3lem7  34614  cvmlift3lem9  34616  snmlff  34618  mrsubfval  34797  wzel  35100  wsuclem  35101  brsegle  35384  gg-dvfsumle  35468  gg-dvfsumlem2  35469  opnregcld  35518  fin2so  36778  poimirlem17  36808  poimirlem23  36814  opnmbllem0  36827  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem  36842  itg2addnc  36845  itg2gt0cn  36846  ftc1cnnclem  36862  ftc1cnnc  36863  areacirclem5  36883  indexdom  36905  sstotbnd2  36945  isbnd3  36955  isbnd3b  36956  cntotbnd  36967  ismtyima  36974  heibor1lem  36980  heiborlem8  36989  rrncmslem  37003  reheibor  37010  lkrlsp  38275  lshpkrlem5  38287  ldualssvscl  38331  ldualssvsubcl  38332  llnmlplnN  38713  llncvrlpln  38732  pmapjat1  39027  pclfinN  39074  lautlt  39265  lauteq  39269  lautco  39271  ltrn11  39300  ltrnle  39303  ltrneq2  39322  cdlemednuN  39474  cdleme20k  39493  cdleme20l2  39495  cdleme20l  39496  cdleme20m  39497  cdleme21c  39501  cdleme22e  39518  cdleme22eALTN  39519  cdlemefrs32fva  39574  cdlemg4g  39790  cdlemg18b  39853  cdlemg18c  39854  cdlemj3  39997  dia2dimlem5  40242  dvhopN  40290  cdlemm10N  40292  dihjatcclem4  40595  dochexmidlem2  40635  lclkrlem2o  40695  lcfrlem5  40720  lcfrlem6  40721  lcdlssvscl  40780  mapdpglem6  40852  mapdpglem9  40854  mapdpglem12  40857  mapdpglem14  40859  mapdindp0  40893  hdmaprnlem7N  41029  hdmaprnlem8N  41030  hdmaprnlem3eN  41032  hgmapvvlem3  41099  evlsaddval  41442  evlsmulval  41443  evladdval  41449  evlmulval  41450  addinvcom  41606  mzpsubst  41788  eldioph2lem1  41800  eldioph2lem2  41801  eldioph2b  41803  diophin  41812  irrapxlem2  41863  irrapxlem4  41865  irrapxlem5  41866  pellexlem1  41869  pellexlem2  41870  pellexlem6  41874  elpell1qr2  41912  pell1qrgaplem  41913  pell1qrgap  41914  pellqrex  41919  pellfundex  41926  pellfund14  41938  rmspecsqrtnq  41946  rmxyadd  41962  congsub  42011  mzpcong  42013  congrep  42014  acongtr  42019  acongrep  42021  jm2.19lem1  42030  jm2.22  42036  jm2.23  42037  jm2.26lem3  42042  jm2.26  42043  jm2.27a  42046  fnwe2lem2  42095  aomclem6  42103  hbtlem2  42168  hbtlem4  42170  hbtlem5  42172  dgraa0p  42193  rngunsnply  42217  proot1hash  42244  nnoeomeqom  42364  cantnf2  42377  omabs2  42384  naddcnff  42414  naddcnffo  42416  naddcnfcom  42418  naddcnfid1  42419  expgrowth  43396  fpmd  44266  abslt2sqd  44368  ioondisj2  44504  ioondisj1  44505  eliocre  44520  ioossioobi  44528  iooiinicc  44553  iooiinioc  44567  icossico2  44575  lptioo2  44645  limcresiooub  44656  limsupequzlem  44736  xlimmnfvlem2  44847  xlimpnfvlem2  44851  cncfuni  44900  cncfiooicclem1  44907  cxpcncf2  44913  dvcnre  44930  dvresntr  44932  dvresioo  44935  dvbdfbdioolem1  44942  dvnmptdivc  44952  dvnxpaek  44956  itgsinexplem1  44968  itgcoscmulx  44983  itgiccshift  44994  itgperiod  44995  ovolsplit  45002  stoweidlem11  45025  stoweidlem26  45040  stoweidlem34  45048  stoweidlem36  45050  stoweidlem38  45052  stirlinglem5  45092  dirkercncflem2  45118  dirkercncflem4  45120  fourierdlem20  45141  fourierdlem58  45178  fourierdlem72  45192  fourierdlem73  45193  fourierdlem74  45194  fourierdlem75  45195  fourierdlem76  45196  fourierdlem79  45199  fourierdlem80  45200  fourierdlem87  45207  fourierdlem94  45214  fourierdlem103  45223  fourierdlem104  45224  fourierdlem107  45227  fourierdlem113  45233  sqwvfoura  45242  sqwvfourb  45243  fourierswlem  45244  fouriersw  45245  etransclem46  45294  etransclem47  45295  rrndistlt  45304  rrnprjdstle  45315  ioorrnopnxrlem  45320  sge0ssre  45411  sge0seq  45460  hsphoidmvle2  45599  hsphoidmvle  45600  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmv1lelem3  45607  hoidmvlelem1  45609  hoidifhspdmvle  45634  hoiqssbllem2  45637  ovolval5lem2  45667  iinhoiicc  45688  iunhoiioo  45690  vonioolem2  45695  vonicclem2  45698  issmflem  45741  iccpartdisj  46403  m1expevenALTV  46613  fpprel2  46707  tgoldbach  46783  strisomgrop  46806  nn0eo  47301  fdivpm  47316  refdivpm  47317  elbigolo1  47330  logbpw2m1  47340  fllog2  47341  dignn0flhalflem1  47388  dignn0flhalflem2  47389  itsclinecirc0in  47548  2itscplem2  47552  itscnhlinecirc02plem1  47555  iccdisj2  47617