Theorem syl22anc 837

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 512	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 835	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  preqsnd  4821  fr2nr  5616  soltmin  6095  f1oprg  6834  f1prex  7235  fveqf1o  7254  weniso  7304  fr3nr  7711  suppofssd  8139  smogt  8318  smocdmdom  8319  oacomf1o  8517  en2prd  8999  enpr2dOLD  9001  difsnen  9004  undomOLD  9011  enfixsn  9032  domss2  9087  ssenen  9102  marypha1lem  9378  fisupcl  9414  ordtypelem3  9465  ordtypelem8  9470  oieu  9484  oismo  9485  wofib  9490  wemaplem2  9492  wemapso  9496  wemapso2lem  9497  unxpwdom2  9533  infdifsn  9602  oemapvali  9629  cantnflem1c  9632  cantnflem1  9634  cantnf  9638  cnfcom3  9649  r1ordg  9723  dif1card  9955  infxpenlem  9958  dfac8clem  9977  infxp  10160  infmap2  10163  cflim2  10208  coftr  10218  fin2i2  10263  enfin2i  10266  fin23lem26  10270  fin23lem27  10273  fin23lem40  10296  isf32lem2  10299  isf32lem3  10300  isf32lem4  10301  isf32lem7  10304  isf32lem9  10306  fin1a2lem13  10357  fin12  10358  alephexp1  10524  gchdomtri  10574  fpwwe2lem11  10586  fpwwe2lem12  10587  gchpwdom  10615  gchhar  10624  adderpqlem  10899  mulerpqlem  10900  addassnq  10903  mulassnq  10904  distrnq  10906  mulidnq  10908  recmulnq  10909  ltexnq  10920  distrlem1pr  10970  distrlem4pr  10971  prlem936  10992  reclem3pr  10994  mulcmpblnr  11016  mulgt0d  11319  mul4d  11376  add4d  11392  add42d  11393  subcan  11465  addsub4d  11568  subadd4d  11569  sub4d  11570  2addsubd  11571  addsubeq4d  11572  muladdd  11622  mulsubd  11623  addgegt0d  11737  addgtge0d  11738  addge0d  11740  mulge0d  11741  le2addd  11783  le2subd  11784  ltleaddd  11785  leltaddd  11786  lt2subd  11788  divdivdiv  11865  divcan5  11866  divne0d  11956  recdivd  11957  recdiv2d  11958  divcan6d  11959  ddcand  11960  rec11d  11961  divmuldivd  11981  divmul13d  11982  divmul24d  11983  divadddivd  11984  divsubdivd  11985  divmuleqd  11986  divdivdivd  11987  subrecd  11995  mulge0b  12034  recreclt  12063  divgt0d  12099  mulgt1d  12100  lemulge11d  12101  lemulge12d  12102  ltmul12ad  12105  lemul12ad  12106  lemul12bd  12107  supmul1  12133  nndivtr  12209  qreccl  12903  ledivdivd  12991  lediv12ad  13025  lt2mul2divd  13035  xlt2add  13189  supxrun  13245  supxrre  13256  infxrre  13265  elicore  13326  iccss2  13345  iccssico2  13348  lincmb01cmp  13422  iccf1o  13423  fzrev2i  13516  2tnp1ge0ge0  13744  m1modnnsub1  13832  modaddmodup  13849  modaddmodlo  13850  modsubdir  13855  fzennn  13883  sermono  13950  mulexpz  14018  expaddz  14022  sqdiv  14036  expsubd  14072  ltexp2a  14081  expmordi  14082  leexp2a  14087  expmulnbnd  14148  digit1  14150  lt2sqd  14169  le2sqd  14170  sq11d  14171  bcm1k  14225  bcp1n  14226  bcp1nk  14227  hashf1lem1  14365  hashf1lem1OLD  14366  cshw1  14722  2swrd2eqwrdeq  14854  ofccat  14866  absrele  15205  sqreulem  15256  sqrtmuld  15321  sqrtsq2d  15322  sqrtled  15323  sqrtltd  15324  sqr11d  15325  abs3lemd  15358  rlimuni  15444  climuni  15446  lo1resb  15458  o1resb  15460  2clim  15466  addcn2  15488  mulcn2  15490  o1of2  15507  o1rlimmul  15513  lo1add  15521  lo1mul  15522  isercolllem1  15561  caucvgrlem  15569  iseraltlem2  15579  iseraltlem3  15580  mptfzshft  15674  fsumrev  15675  fsum0diag2  15679  binomlem  15725  climcndslem1  15745  climcndslem2  15746  harmonic  15755  mertenslem1  15780  fprodser  15843  fprodrev  15871  efcllem  15971  moddvds  16158  dvds1  16212  dvdsext  16214  evennn2n  16244  bitsinv1  16333  sadaddlem  16357  sadasslem  16361  sadeq  16363  mulgcd  16440  dvdssqlem  16453  lcmftp  16523  rpmulgcd2  16543  coprmproddvdslem  16549  isprm5  16594  isprm6  16601  crth  16661  eulerthlem2  16665  prmdiveq  16669  pythagtriplem11  16708  pythagtriplem13  16710  pcgcd1  16760  pcprmpw2  16765  pcaddlem  16771  fldivp1  16780  4sqlem12  16839  4sqlem14  16841  4sqlem15  16842  4sqlem16  16843  vdwapun  16857  mreexexlem4d  17541  acsfn1  17555  acsfn2  17557  sscpwex  17712  rescabs  17732  rescabsOLD  17733  yonedainv  18184  subm0  18640  pmtrfb  19261  psgnunilem1  19289  odmodnn0  19336  odeq  19346  dfod2  19360  sylow1lem1  19394  lsmsubg  19450  lsmmod  19471  lsmdisj2  19478  ghmplusg  19638  odadd  19642  gexexlem  19644  lt6abl  19686  cyggex2  19688  dprdfinv  19812  dmdprdsplitlem  19830  dpjidcl  19851  ablfacrp  19859  ablfacrp2  19860  ablfac1c  19864  ablfac1eu  19866  acsfn1p  20322  lcomfsupp  20419  lssvancl1  20462  lssvnegcl  20474  lspprvacl  20517  lspsneli  20519  lspsn  20520  lmhmplusg  20562  lmhmima  20565  lmhmpreima  20566  reslmhm  20570  lbsind2  20599  lsmcl  20601  lsmelval2  20603  lsppreli  20608  lspprabs  20613  pj1lmhm  20618  lssvs0or  20630  lspabs3  20641  lspfixed  20648  lspexch  20649  lsmcv  20661  lspsolv  20663  lidlmcl  20746  drngnidl  20758  2idlcpbl  20763  gzrngunit  20900  zringlpirlem3  20922  prmirredlem  20930  znf1o  20995  znunithash  21008  frlmsubgval  21208  frlmvplusgvalc  21210  frlmvscaval  21211  frlmphllem  21223  frlmphl  21224  frlmssuvc1  21237  frlmsslsp  21239  frlmup1  21241  frlmup2  21242  lindfind2  21261  lindfrn  21264  f1lindf  21265  islindf4  21281  mplbas2  21480  evlslem3  21527  evlslem1  21529  coe1addfv  21673  lply1binom  21714  evl1addd  21744  evl1subd  21745  evl1muld  21746  mamudi  21787  mamudir  21788  1marepvmarrepid  21961  mdetrlin  21988  smadiadetglem1  22057  smadiadetg  22059  cramerimplem1  22069  mat2pmatscmxcl  22126  m2pmfzgsumcl  22134  pmatcollpw  22167  pmatcollpwfi  22168  pmatcollpw3fi1lem1  22172  cpmidpmatlem2  22257  cpmadugsumlemF  22262  chcoeffeqlem  22271  ntrin  22449  topssnei  22512  restbas  22546  restntr  22570  cnntri  22659  fiuncmp  22792  nllyrest  22874  nllyidm  22877  hausllycmp  22882  cldllycmp  22883  hauspwdom  22889  txcld  22991  txcn  23014  txlly  23024  txnlly  23025  txhaus  23035  txlm  23036  txkgen  23040  xkococnlem  23047  cnmpt2res  23065  xkoinjcn  23075  basqtop  23099  qtopeu  23104  trfbas2  23231  neifil  23268  hausflim  23369  alexsubALTlem2  23436  cnextfval  23450  cnextfvval  23453  cnextf  23454  cnextfres  23457  clssubg  23497  utop2nei  23639  utop3cls  23640  utopreg  23641  psmetlecl  23705  xmetlecl  23736  prdsxmetlem  23758  bldisj  23788  imasf1obl  23881  prdsbl  23884  stdbdmet  23909  stdbdmopn  23911  met2ndci  23915  metcnp  23934  metustto  23946  metustexhalf  23949  cfilucfil  23952  metucn  23964  lssnlm  24102  nmotri  24140  nmoid  24143  tgioo  24196  blcvx  24198  xrsmopn  24212  reperflem  24218  reconnlem2  24227  opnreen  24231  metdsge  24249  metdsre  24253  metdscnlem  24255  metnrmlem1a  24258  metnrmlem1  24259  metnrmlem3  24261  cncfmet  24309  cnmpopc  24328  icopnfcnv  24342  icopnfhmeo  24343  cnllycmp  24356  evth  24359  lebnumii  24366  nmoleub2lem3  24515  iscfil2  24667  cfil3i  24670  iscfil3  24674  cfilfcls  24675  iscau3  24679  iscmet3lem2  24693  caubl  24709  lmcau  24714  cssbn  24776  rrxcph  24793  minveclem2  24827  pjthlem1  24838  pjthlem2  24839  ivthicc  24859  ovollecl  24884  ovolunlem1a  24897  ovolunnul  24901  ovoliunlem1  24903  ismbl2  24928  nulmbl2  24937  unmbl  24938  volun  24946  voliunlem2  24952  ioombl1lem2  24960  uniioombllem2a  24983  uniioombllem3  24986  uniioombllem4  24987  dyaddisjlem  24996  dyadmaxlem  24998  opnmbllem  25002  volsup2  25006  volcn  25007  ismbfd  25040  mbfi1fseqlem1  25117  mbfi1fseqlem5  25121  itg2lecl  25140  itg2monolem2  25153  itg2gt0  25162  itgspliticc  25238  ellimc3  25280  limcres  25287  dvfval  25298  dvres3  25314  dvres3a  25315  dvmptresicc  25317  dvnff  25324  dvnadd  25330  dvn2bss  25331  dvnres  25332  dvcmul  25345  dvcmulf  25346  dvmptres3  25357  dvmptres2  25363  dvmptntr  25372  dvexp3  25379  dvferm1lem  25385  dvlip  25394  dvlipcn  25395  dvlip2  25396  c1liplem1  25397  dvgt0lem1  25403  dvgt0lem2  25404  dvne0  25412  lhop1lem  25414  lhop2  25416  lhop  25417  dvcnvrelem1  25418  dvcnvrelem2  25419  dvcvx  25421  dvfsumle  25422  dvfsumabs  25424  dvfsumlem2  25428  ftc1lem6  25442  ftc1  25443  ftc2ditglem  25446  itgsubstlem  25449  itgpowd  25451  tdeglem4  25461  tdeglem4OLD  25462  mdegaddle  25476  mdegmullem  25480  ply1rem  25565  fta1glem2  25568  fta1blem  25570  ig1peu  25573  ig1pdvds  25578  dgrmulc  25669  dgrcolem1  25671  plydivlem4  25693  plydiveu  25695  fta1lem  25704  vieta1lem1  25707  vieta1lem2  25708  plyexmo  25710  taylfvallem1  25753  taylfval  25755  tayl0  25758  taylplem1  25759  taylply2  25764  taylply  25765  dvtaylp  25766  dvntaylp  25767  dvntaylp0  25768  taylthlem1  25769  taylthlem2  25770  ulmcaulem  25790  ulmcau  25791  ulmcn  25795  ulmdvlem1  25796  radcnvlem1  25809  radcnvle  25816  psercn  25822  pserdvlem2  25824  pserdv  25825  abelth  25837  tanregt0  25932  dvlog2lem  26044  efopn  26050  logtayllem  26051  logccv  26055  cxplt3  26092  cxpmul2zd  26108  cxpltd  26111  cxpled  26112  cxplt3d  26126  cxple3d  26127  dvsqrt  26132  cxpcn3  26138  cxpaddle  26142  cxpeq  26147  angcan  26189  angvald  26191  ang180lem2  26197  ang180  26201  isosctrlem3  26207  dquartlem1  26238  atantayl2  26325  leibpi  26329  log2tlbnd  26332  birthdaylem3  26340  xrlimcnp  26355  efrlim  26356  o1cxp  26361  jensenlem2  26374  jensen  26375  fsumharmonic  26398  lgamucov  26424  lgamcvg2  26441  wilthlem1  26454  basellem3  26469  basellem6  26472  basellem8  26474  ppisval  26490  chtwordi  26542  ppiwordi  26548  mumullem2  26566  dvdsmulf1o  26580  fsumvma  26598  fsumvma2  26599  chpchtsum  26604  chpub  26605  logfacubnd  26606  dchrmulcl  26634  dchrinv  26646  dchrptlem1  26649  dchrptlem2  26650  sumdchr2  26655  dchr2sum  26658  bposlem7  26675  lgslem1  26682  lgslem3  26684  lgsdirprm  26716  lgsqrlem2  26732  lgseisenlem1  26760  lgseisenlem2  26761  lgseisenlem4  26763  lgseisen  26764  lgsquadlem1  26765  lgsquad2lem1  26769  lgsquad3  26772  m1lgs  26773  2sqlem7  26809  2sq2  26818  2sqmod  26821  chebbnd1lem2  26855  chebbnd1lem3  26856  rplogsumlem1  26869  rpvmasumlem  26872  dchrvmasumlem1  26880  dchrvmasum2lem  26881  dchrvmasumlema  26885  dchrisum0flblem2  26894  dchrisum0fno1  26896  dchrisum0re  26898  logdivsum  26918  pntrsumbnd2  26952  pntpbnd1a  26970  pntpbnd1  26971  pntibndlem2  26976  pntlemr  26987  pntlemj  26988  pntlemf  26990  pnt2  26998  padicabv  27015  ostth2lem2  27019  sltrec  27202  madebday  27272  sltn0  27277  addsproplem6  27329  sleadd1  27341  negsproplem6  27374  f1otrg  27876  brbtwn2  27917  colinearalglem2  27919  axcgrtr  27927  axcgrid  27928  axsegconlem7  27935  axsegcon  27939  ax5seglem3  27943  ax5seglem6  27946  ax5seg  27950  axpaschlem  27952  axlowdimlem17  27970  axcontlem2  27977  axcontlem4  27979  axcontlem7  27982  axcontlem8  27983  ecgrtg  27995  usgredg2v  28238  vtxdgoddnumeven  28564  2trlond  28947  eupthp1  29223  nmobndi  29780  ubthlem2  29876  ubthlem3  29877  minvecolem2  29880  shuni  30305  pjhthlem1  30396  chscllem2  30643  pjcompi  30677  mayete3i  30733  unoplin  30925  hmoplin  30947  nmophmi  31036  mdslmd4i  31338  isoun  31683  xrge0addcld  31735  xrofsup  31740  eliccelico  31748  elicoelioo  31749  difioo  31753  rexdiv  31852  mgcmnt1d  31927  mgcmnt2d  31928  xrge0addgt0  31952  omndadd2d  31986  omndadd2rd  31987  omndmul2  31990  cycpmcl  32035  cycpm2tr  32038  cyc3evpm  32069  cycpmconjslem2  32074  freshmansdream  32137  fldgensdrg  32152  ofldchr  32180  qusker  32212  eqgvscpbl  32213  ringlsmss1  32250  ringlsmss2  32251  intlidl  32274  rhmpreimaidl  32275  elrspunidl  32279  idlinsubrg  32281  isprmidlc  32296  rhmpreimaprmidl  32300  qsidomlem1  32301  mxidlprm  32313  ssmxidllem  32314  ply1degltdimlem  32404  lindsunlem  32406  finexttrb  32438  mdetpmtr2  32494  mdetpmtr12  32495  madjusmdetlem1  32497  madjusmdetlem4  32500  rhmpreimacn  32555  unitdivcld  32571  xrge0mulc1cn  32611  qqhnm  32660  esumcst  32751  esumfsup  32758  esumpmono  32767  esumcvg  32774  difelsiga  32821  sigapisys  32843  sigapildsys  32850  ldgenpisyslem1  32851  1stmbfm  32949  2ndmbfm  32950  dya2icoseg  32966  sibfinima  33028  probmeasb  33119  orvcgteel  33156  orvclteel  33161  ballotlemsima  33204  ballotlemfrceq  33217  sgnmul  33231  ccatmulgnn0dir  33243  fct2relem  33299  ftc2re  33300  chtvalz  33331  subfacp1lem2a  33861  subfaclim  33869  erdsze2lem2  33885  cvmliftlem2  33967  cvmliftlem10  33975  cvmliftlem13  33977  cvmliftiota  33982  cvmlift2lem9  33992  cvmlift2lem11  33994  cvmlift2lem12  33995  cvmliftphtlem  33998  cvmlift3lem6  34005  cvmlift3lem7  34006  cvmlift3lem9  34008  snmlff  34010  mrsubfval  34189  wzel  34485  wsuclem  34486  brsegle  34769  opnregcld  34878  fin2so  36138  poimirlem17  36168  poimirlem23  36174  opnmbllem0  36187  mblfinlem3  36190  mblfinlem4  36191  itg2addnclem  36202  itg2addnc  36205  itg2gt0cn  36206  ftc1cnnclem  36222  ftc1cnnc  36223  areacirclem5  36243  indexdom  36266  sstotbnd2  36306  isbnd3  36316  isbnd3b  36317  cntotbnd  36328  ismtyima  36335  heibor1lem  36341  heiborlem8  36350  rrncmslem  36364  reheibor  36371  lkrlsp  37637  lshpkrlem5  37649  ldualssvscl  37693  ldualssvsubcl  37694  llnmlplnN  38075  llncvrlpln  38094  pmapjat1  38389  pclfinN  38436  lautlt  38627  lauteq  38631  lautco  38633  ltrn11  38662  ltrnle  38665  ltrneq2  38684  cdlemednuN  38836  cdleme20k  38855  cdleme20l2  38857  cdleme20l  38858  cdleme20m  38859  cdleme21c  38863  cdleme22e  38880  cdleme22eALTN  38881  cdlemefrs32fva  38936  cdlemg4g  39152  cdlemg18b  39215  cdlemg18c  39216  cdlemj3  39359  dia2dimlem5  39604  dvhopN  39652  cdlemm10N  39654  dihjatcclem4  39957  dochexmidlem2  39997  lclkrlem2o  40057  lcfrlem5  40082  lcfrlem6  40083  lcdlssvscl  40142  mapdpglem6  40214  mapdpglem9  40216  mapdpglem12  40219  mapdpglem14  40221  mapdindp0  40255  hdmaprnlem7N  40391  hdmaprnlem8N  40392  hdmaprnlem3eN  40394  hgmapvvlem3  40461  evlsaddval  40808  evlsmulval  40809  evladdval  40811  evlmulval  40812  addinvcom  40958  mzpsubst  41129  eldioph2lem1  41141  eldioph2lem2  41142  eldioph2b  41144  diophin  41153  irrapxlem2  41204  irrapxlem4  41206  irrapxlem5  41207  pellexlem1  41210  pellexlem2  41211  pellexlem6  41215  elpell1qr2  41253  pell1qrgaplem  41254  pell1qrgap  41255  pellqrex  41260  pellfundex  41267  pellfund14  41279  rmspecsqrtnq  41287  rmxyadd  41303  congsub  41352  mzpcong  41354  congrep  41355  acongtr  41360  acongrep  41362  jm2.19lem1  41371  jm2.22  41377  jm2.23  41378  jm2.26lem3  41383  jm2.26  41384  jm2.27a  41387  fnwe2lem2  41436  aomclem6  41444  hbtlem2  41509  hbtlem4  41511  hbtlem5  41513  dgraa0p  41534  rngunsnply  41558  proot1hash  41585  nnoeomeqom  41705  cantnf2  41718  omabs2  41725  naddcnff  41755  naddcnffo  41757  naddcnfcom  41759  naddcnfid1  41760  expgrowth  42737  fpmd  43613  abslt2sqd  43715  ioondisj2  43851  ioondisj1  43852  eliocre  43867  ioossioobi  43875  iooiinicc  43900  iooiinioc  43914  icossico2  43922  lptioo2  43992  limcresiooub  44003  limsupequzlem  44083  xlimmnfvlem2  44194  xlimpnfvlem2  44198  cncfuni  44247  cncfiooicclem1  44254  cxpcncf2  44260  dvcnre  44277  dvresntr  44279  dvresioo  44282  dvbdfbdioolem1  44289  dvnmptdivc  44299  dvnxpaek  44303  itgsinexplem1  44315  itgcoscmulx  44330  itgiccshift  44341  itgperiod  44342  ovolsplit  44349  stoweidlem11  44372  stoweidlem26  44387  stoweidlem34  44395  stoweidlem36  44397  stoweidlem38  44399  stirlinglem5  44439  dirkercncflem2  44465  dirkercncflem4  44467  fourierdlem20  44488  fourierdlem58  44525  fourierdlem72  44539  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem79  44546  fourierdlem80  44547  fourierdlem87  44554  fourierdlem94  44561  fourierdlem103  44570  fourierdlem104  44571  fourierdlem107  44574  fourierdlem113  44580  sqwvfoura  44589  sqwvfourb  44590  fourierswlem  44591  fouriersw  44592  etransclem46  44641  etransclem47  44642  rrndistlt  44651  rrnprjdstle  44662  ioorrnopnxrlem  44667  sge0ssre  44758  sge0seq  44807  hsphoidmvle2  44946  hsphoidmvle  44947  hoidmv1lelem1  44952  hoidmv1lelem2  44953  hoidmv1lelem3  44954  hoidmvlelem1  44956  hoidifhspdmvle  44981  hoiqssbllem2  44984  ovolval5lem2  45014  iinhoiicc  45035  iunhoiioo  45037  vonioolem2  45042  vonicclem2  45045  issmflem  45088  iccpartdisj  45749  m1expevenALTV  45959  fpprel2  46053  tgoldbach  46129  strisomgrop  46152  nn0eo  46734  fdivpm  46749  refdivpm  46750  elbigolo1  46763  logbpw2m1  46773  fllog2  46774  dignn0flhalflem1  46821  dignn0flhalflem2  46822  itsclinecirc0in  46981  2itscplem2  46985  itscnhlinecirc02plem1  46988  iccdisj2  47050