Theorem syl22anc 838

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  preqsnd  4860  fr2nr  5655  soltmin  6138  f1oprg  6879  f1prex  7282  fveqf1o  7301  weniso  7351  fr3nr  7759  suppofssd  8188  smogt  8367  smocdmdom  8368  oacomf1o  8565  en2prd  9048  enpr2dOLD  9050  difsnen  9053  undomOLD  9060  enfixsn  9081  domss2  9136  ssenen  9151  marypha1lem  9428  fisupcl  9464  ordtypelem3  9515  ordtypelem8  9520  oieu  9534  oismo  9535  wofib  9540  wemaplem2  9542  wemapso  9546  wemapso2lem  9547  unxpwdom2  9583  infdifsn  9652  oemapvali  9679  cantnflem1c  9682  cantnflem1  9684  cantnf  9688  cnfcom3  9699  r1ordg  9773  dif1card  10005  infxpenlem  10008  dfac8clem  10027  infxp  10210  infmap2  10213  cflim2  10258  coftr  10268  fin2i2  10313  enfin2i  10316  fin23lem26  10320  fin23lem27  10323  fin23lem40  10346  isf32lem2  10349  isf32lem3  10350  isf32lem4  10351  isf32lem7  10354  isf32lem9  10356  fin1a2lem13  10407  fin12  10408  alephexp1  10574  gchdomtri  10624  fpwwe2lem11  10636  fpwwe2lem12  10637  gchpwdom  10665  gchhar  10674  adderpqlem  10949  mulerpqlem  10950  addassnq  10953  mulassnq  10954  distrnq  10956  mulidnq  10958  recmulnq  10959  ltexnq  10970  distrlem1pr  11020  distrlem4pr  11021  prlem936  11042  reclem3pr  11044  mulcmpblnr  11066  mulgt0d  11369  mul4d  11426  add4d  11442  add42d  11443  subcan  11515  addsub4d  11618  subadd4d  11619  sub4d  11620  2addsubd  11621  addsubeq4d  11622  muladdd  11672  mulsubd  11673  addgegt0d  11787  addgtge0d  11788  addge0d  11790  mulge0d  11791  le2addd  11833  le2subd  11834  ltleaddd  11835  leltaddd  11836  lt2subd  11838  divdivdiv  11915  divcan5  11916  divne0d  12006  recdivd  12007  recdiv2d  12008  divcan6d  12009  ddcand  12010  rec11d  12011  divmuldivd  12031  divmul13d  12032  divmul24d  12033  divadddivd  12034  divsubdivd  12035  divmuleqd  12036  divdivdivd  12037  subrecd  12045  mulge0b  12084  recreclt  12113  divgt0d  12149  mulgt1d  12150  lemulge11d  12151  lemulge12d  12152  ltmul12ad  12155  lemul12ad  12156  lemul12bd  12157  supmul1  12183  nndivtr  12259  qreccl  12953  ledivdivd  13041  lediv12ad  13075  lt2mul2divd  13085  xlt2add  13239  supxrun  13295  supxrre  13306  infxrre  13315  elicore  13376  iccss2  13395  iccssico2  13398  lincmb01cmp  13472  iccf1o  13473  fzrev2i  13566  2tnp1ge0ge0  13794  m1modnnsub1  13882  modaddmodup  13899  modaddmodlo  13900  modsubdir  13905  fzennn  13933  sermono  14000  mulexpz  14068  expaddz  14072  sqdiv  14086  expsubd  14122  ltexp2a  14131  expmordi  14132  leexp2a  14137  expmulnbnd  14198  digit1  14200  lt2sqd  14219  le2sqd  14220  sq11d  14221  bcm1k  14275  bcp1n  14276  bcp1nk  14277  hashf1lem1  14415  hashf1lem1OLD  14416  cshw1  14772  2swrd2eqwrdeq  14904  ofccat  14916  absrele  15255  sqreulem  15306  sqrtmuld  15371  sqrtsq2d  15372  sqrtled  15373  sqrtltd  15374  sqr11d  15375  abs3lemd  15408  rlimuni  15494  climuni  15496  lo1resb  15508  o1resb  15510  2clim  15516  addcn2  15538  mulcn2  15540  o1of2  15557  o1rlimmul  15563  lo1add  15571  lo1mul  15572  isercolllem1  15611  caucvgrlem  15619  iseraltlem2  15629  iseraltlem3  15630  mptfzshft  15724  fsumrev  15725  fsum0diag2  15729  binomlem  15775  climcndslem1  15795  climcndslem2  15796  harmonic  15805  mertenslem1  15830  fprodser  15893  fprodrev  15921  efcllem  16021  moddvds  16208  dvds1  16262  dvdsext  16264  evennn2n  16294  bitsinv1  16383  sadaddlem  16407  sadasslem  16411  sadeq  16413  mulgcd  16490  dvdssqlem  16503  lcmftp  16573  rpmulgcd2  16593  coprmproddvdslem  16599  isprm5  16644  isprm6  16651  crth  16711  eulerthlem2  16715  prmdiveq  16719  pythagtriplem11  16758  pythagtriplem13  16760  pcgcd1  16810  pcprmpw2  16815  pcaddlem  16821  fldivp1  16830  4sqlem12  16889  4sqlem14  16891  4sqlem15  16892  4sqlem16  16893  vdwapun  16907  mreexexlem4d  17591  acsfn1  17605  acsfn2  17607  sscpwex  17762  rescabs  17782  rescabsOLD  17783  yonedainv  18234  subm0  18696  pmtrfb  19333  psgnunilem1  19361  odmodnn0  19408  odeq  19418  dfod2  19432  sylow1lem1  19466  lsmsubg  19522  lsmmod  19543  lsmdisj2  19550  ghmplusg  19714  odadd  19718  gexexlem  19720  lt6abl  19763  cyggex2  19765  dprdfinv  19889  dmdprdsplitlem  19907  dpjidcl  19928  ablfacrp  19936  ablfacrp2  19937  ablfac1c  19941  ablfac1eu  19943  acsfn1p  20415  lcomfsupp  20512  lssvancl1  20555  lssvnegcl  20567  lspprvacl  20610  lspsneli  20612  lspsn  20613  lmhmplusg  20655  lmhmima  20658  lmhmpreima  20659  reslmhm  20663  lbsind2  20692  lsmcl  20694  lsmelval2  20696  lsppreli  20701  lspprabs  20706  pj1lmhm  20711  lssvs0or  20723  lspabs3  20734  lspfixed  20741  lspexch  20742  lsmcv  20754  lspsolv  20756  lidlmcl  20840  drngnidl  20854  2idlcpbl  20871  gzrngunit  21011  zringlpirlem3  21034  prmirredlem  21042  znf1o  21107  znunithash  21120  frlmsubgval  21320  frlmvplusgvalc  21322  frlmvscaval  21323  frlmphllem  21335  frlmphl  21336  frlmssuvc1  21349  frlmsslsp  21351  frlmup1  21353  frlmup2  21354  lindfind2  21373  lindfrn  21376  f1lindf  21377  islindf4  21393  mplbas2  21597  evlslem3  21643  evlslem1  21645  coe1addfv  21787  lply1binom  21830  evl1addd  21860  evl1subd  21861  evl1muld  21862  mamudi  21903  mamudir  21904  1marepvmarrepid  22077  mdetrlin  22104  smadiadetglem1  22173  smadiadetg  22175  cramerimplem1  22185  mat2pmatscmxcl  22242  m2pmfzgsumcl  22250  pmatcollpw  22283  pmatcollpwfi  22284  pmatcollpw3fi1lem1  22288  cpmidpmatlem2  22373  cpmadugsumlemF  22378  chcoeffeqlem  22387  ntrin  22565  topssnei  22628  restbas  22662  restntr  22686  cnntri  22775  fiuncmp  22908  nllyrest  22990  nllyidm  22993  hausllycmp  22998  cldllycmp  22999  hauspwdom  23005  txcld  23107  txcn  23130  txlly  23140  txnlly  23141  txhaus  23151  txlm  23152  txkgen  23156  xkococnlem  23163  cnmpt2res  23181  xkoinjcn  23191  basqtop  23215  qtopeu  23220  trfbas2  23347  neifil  23384  hausflim  23485  alexsubALTlem2  23552  cnextfval  23566  cnextfvval  23569  cnextf  23570  cnextfres  23573  clssubg  23613  utop2nei  23755  utop3cls  23756  utopreg  23757  psmetlecl  23821  xmetlecl  23852  prdsxmetlem  23874  bldisj  23904  imasf1obl  23997  prdsbl  24000  stdbdmet  24025  stdbdmopn  24027  met2ndci  24031  metcnp  24050  metustto  24062  metustexhalf  24065  cfilucfil  24068  metucn  24080  lssnlm  24218  nmotri  24256  nmoid  24259  tgioo  24312  blcvx  24314  xrsmopn  24328  reperflem  24334  reconnlem2  24343  opnreen  24347  metdsge  24365  metdsre  24369  metdscnlem  24371  metnrmlem1a  24374  metnrmlem1  24375  metnrmlem3  24377  cncfmet  24425  cnmpopc  24444  icopnfcnv  24458  icopnfhmeo  24459  cnllycmp  24472  evth  24475  lebnumii  24482  nmoleub2lem3  24631  iscfil2  24783  cfil3i  24786  iscfil3  24790  cfilfcls  24791  iscau3  24795  iscmet3lem2  24809  caubl  24825  lmcau  24830  cssbn  24892  rrxcph  24909  minveclem2  24943  pjthlem1  24954  pjthlem2  24955  ivthicc  24975  ovollecl  25000  ovolunlem1a  25013  ovolunnul  25017  ovoliunlem1  25019  ismbl2  25044  nulmbl2  25053  unmbl  25054  volun  25062  voliunlem2  25068  ioombl1lem2  25076  uniioombllem2a  25099  uniioombllem3  25102  uniioombllem4  25103  dyaddisjlem  25112  dyadmaxlem  25114  opnmbllem  25118  volsup2  25122  volcn  25123  ismbfd  25156  mbfi1fseqlem1  25233  mbfi1fseqlem5  25237  itg2lecl  25256  itg2monolem2  25269  itg2gt0  25278  itgspliticc  25354  ellimc3  25396  limcres  25403  dvfval  25414  dvres3  25430  dvres3a  25431  dvmptresicc  25433  dvnff  25440  dvnadd  25446  dvn2bss  25447  dvnres  25448  dvcmul  25461  dvcmulf  25462  dvmptres3  25473  dvmptres2  25479  dvmptntr  25488  dvexp3  25495  dvferm1lem  25501  dvlip  25510  dvlipcn  25511  dvlip2  25512  c1liplem1  25513  dvgt0lem1  25519  dvgt0lem2  25520  dvne0  25528  lhop1lem  25530  lhop2  25532  lhop  25533  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcvx  25537  dvfsumle  25538  dvfsumabs  25540  dvfsumlem2  25544  ftc1lem6  25558  ftc1  25559  ftc2ditglem  25562  itgsubstlem  25565  itgpowd  25567  tdeglem4  25577  tdeglem4OLD  25578  mdegaddle  25592  mdegmullem  25596  ply1rem  25681  fta1glem2  25684  fta1blem  25686  ig1peu  25689  ig1pdvds  25694  dgrmulc  25785  dgrcolem1  25787  plydivlem4  25809  plydiveu  25811  fta1lem  25820  vieta1lem1  25823  vieta1lem2  25824  plyexmo  25826  taylfvallem1  25869  taylfval  25871  tayl0  25874  taylplem1  25875  taylply2  25880  taylply  25881  dvtaylp  25882  dvntaylp  25883  dvntaylp0  25884  taylthlem1  25885  taylthlem2  25886  ulmcaulem  25906  ulmcau  25907  ulmcn  25911  ulmdvlem1  25912  radcnvlem1  25925  radcnvle  25932  psercn  25938  pserdvlem2  25940  pserdv  25941  abelth  25953  tanregt0  26048  dvlog2lem  26160  efopn  26166  logtayllem  26167  logccv  26171  cxplt3  26208  cxpmul2zd  26224  cxpltd  26227  cxpled  26228  cxplt3d  26243  cxple3d  26244  dvsqrt  26250  cxpcn3  26256  cxpaddle  26260  cxpeq  26265  angcan  26307  angvald  26309  ang180lem2  26315  ang180  26319  isosctrlem3  26325  dquartlem1  26356  atantayl2  26443  leibpi  26447  log2tlbnd  26450  birthdaylem3  26458  xrlimcnp  26473  efrlim  26474  o1cxp  26479  jensenlem2  26492  jensen  26493  fsumharmonic  26516  lgamucov  26542  lgamcvg2  26559  wilthlem1  26572  basellem3  26587  basellem6  26590  basellem8  26592  ppisval  26608  chtwordi  26660  ppiwordi  26666  mumullem2  26684  dvdsmulf1o  26698  fsumvma  26716  fsumvma2  26717  chpchtsum  26722  chpub  26723  logfacubnd  26724  dchrmulcl  26752  dchrinv  26764  dchrptlem1  26767  dchrptlem2  26768  sumdchr2  26773  dchr2sum  26776  bposlem7  26793  lgslem1  26800  lgslem3  26802  lgsdirprm  26834  lgsqrlem2  26850  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem4  26881  lgseisen  26882  lgsquadlem1  26883  lgsquad2lem1  26887  lgsquad3  26890  m1lgs  26891  2sqlem7  26927  2sq2  26936  2sqmod  26939  chebbnd1lem2  26973  chebbnd1lem3  26974  rplogsumlem1  26987  rpvmasumlem  26990  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrvmasumlema  27003  dchrisum0flblem2  27012  dchrisum0fno1  27014  dchrisum0re  27016  logdivsum  27036  pntrsumbnd2  27070  pntpbnd1a  27088  pntpbnd1  27089  pntibndlem2  27094  pntlemr  27105  pntlemj  27106  pntlemf  27108  pnt2  27116  padicabv  27133  ostth2lem2  27137  sltrec  27321  madebday  27394  sltn0  27399  addsproplem6  27458  sleadd1  27472  negsproplem6  27507  mulsproplem13  27584  mulsproplem14  27585  sltmuld  27593  mulsgt0d  27601  f1otrg  28122  brbtwn2  28163  colinearalglem2  28165  axcgrtr  28173  axcgrid  28174  axsegconlem7  28181  axsegcon  28185  ax5seglem3  28189  ax5seglem6  28192  ax5seg  28196  axpaschlem  28198  axlowdimlem17  28216  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  axcontlem8  28229  ecgrtg  28241  usgredg2v  28484  vtxdgoddnumeven  28810  2trlond  29193  eupthp1  29469  nmobndi  30028  ubthlem2  30124  ubthlem3  30125  minvecolem2  30128  shuni  30553  pjhthlem1  30644  chscllem2  30891  pjcompi  30925  mayete3i  30981  unoplin  31173  hmoplin  31195  nmophmi  31284  mdslmd4i  31586  isoun  31923  xrge0addcld  31975  xrofsup  31980  eliccelico  31988  elicoelioo  31989  difioo  31993  rexdiv  32092  mgcmnt1d  32167  mgcmnt2d  32168  xrge0addgt0  32192  omndadd2d  32226  omndadd2rd  32227  omndmul2  32230  cycpmcl  32275  cycpm2tr  32278  cyc3evpm  32309  cycpmconjslem2  32314  freshmansdream  32381  fldgensdrg  32404  ofldchr  32432  qusker  32464  eqgvscpbl  32465  ringlsmss1  32506  ringlsmss2  32507  intlidl  32536  rhmpreimaidl  32537  lidlunitel  32541  elrspunidl  32546  idlinsubrg  32549  isprmidlc  32566  rhmpreimaprmidl  32570  qsidomlem1  32571  mxidlmaxv  32584  mxidlprm  32586  ssmxidllem  32589  opprmxidlabs  32601  qsdrnglem2  32610  ply1degltdimlem  32707  lindsunlem  32709  finexttrb  32741  algextdeglem1  32772  mdetpmtr2  32804  mdetpmtr12  32805  madjusmdetlem1  32807  madjusmdetlem4  32810  rhmpreimacn  32865  unitdivcld  32881  xrge0mulc1cn  32921  qqhnm  32970  esumcst  33061  esumfsup  33068  esumpmono  33077  esumcvg  33084  difelsiga  33131  sigapisys  33153  sigapildsys  33160  ldgenpisyslem1  33161  1stmbfm  33259  2ndmbfm  33260  dya2icoseg  33276  sibfinima  33338  probmeasb  33429  orvcgteel  33466  orvclteel  33471  ballotlemsima  33514  ballotlemfrceq  33527  sgnmul  33541  ccatmulgnn0dir  33553  fct2relem  33609  ftc2re  33610  chtvalz  33641  subfacp1lem2a  34171  subfaclim  34179  erdsze2lem2  34195  cvmliftlem2  34277  cvmliftlem10  34285  cvmliftlem13  34287  cvmliftiota  34292  cvmlift2lem9  34302  cvmlift2lem11  34304  cvmlift2lem12  34305  cvmliftphtlem  34308  cvmlift3lem6  34315  cvmlift3lem7  34316  cvmlift3lem9  34318  snmlff  34320  mrsubfval  34499  wzel  34796  wsuclem  34797  brsegle  35080  gg-dvfsumle  35182  gg-dvfsumlem2  35183  opnregcld  35215  fin2so  36475  poimirlem17  36505  poimirlem23  36511  opnmbllem0  36524  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem  36539  itg2addnc  36542  itg2gt0cn  36543  ftc1cnnclem  36559  ftc1cnnc  36560  areacirclem5  36580  indexdom  36602  sstotbnd2  36642  isbnd3  36652  isbnd3b  36653  cntotbnd  36664  ismtyima  36671  heibor1lem  36677  heiborlem8  36686  rrncmslem  36700  reheibor  36707  lkrlsp  37972  lshpkrlem5  37984  ldualssvscl  38028  ldualssvsubcl  38029  llnmlplnN  38410  llncvrlpln  38429  pmapjat1  38724  pclfinN  38771  lautlt  38962  lauteq  38966  lautco  38968  ltrn11  38997  ltrnle  39000  ltrneq2  39019  cdlemednuN  39171  cdleme20k  39190  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme21c  39198  cdleme22e  39215  cdleme22eALTN  39216  cdlemefrs32fva  39271  cdlemg4g  39487  cdlemg18b  39550  cdlemg18c  39551  cdlemj3  39694  dia2dimlem5  39939  dvhopN  39987  cdlemm10N  39989  dihjatcclem4  40292  dochexmidlem2  40332  lclkrlem2o  40392  lcfrlem5  40417  lcfrlem6  40418  lcdlssvscl  40477  mapdpglem6  40549  mapdpglem9  40551  mapdpglem12  40554  mapdpglem14  40556  mapdindp0  40590  hdmaprnlem7N  40726  hdmaprnlem8N  40727  hdmaprnlem3eN  40729  hgmapvvlem3  40796  evlsaddval  41140  evlsmulval  41141  evladdval  41147  evlmulval  41148  addinvcom  41304  mzpsubst  41486  eldioph2lem1  41498  eldioph2lem2  41499  eldioph2b  41501  diophin  41510  irrapxlem2  41561  irrapxlem4  41563  irrapxlem5  41564  pellexlem1  41567  pellexlem2  41568  pellexlem6  41572  elpell1qr2  41610  pell1qrgaplem  41611  pell1qrgap  41612  pellqrex  41617  pellfundex  41624  pellfund14  41636  rmspecsqrtnq  41644  rmxyadd  41660  congsub  41709  mzpcong  41711  congrep  41712  acongtr  41717  acongrep  41719  jm2.19lem1  41728  jm2.22  41734  jm2.23  41735  jm2.26lem3  41740  jm2.26  41741  jm2.27a  41744  fnwe2lem2  41793  aomclem6  41801  hbtlem2  41866  hbtlem4  41868  hbtlem5  41870  dgraa0p  41891  rngunsnply  41915  proot1hash  41942  nnoeomeqom  42062  cantnf2  42075  omabs2  42082  naddcnff  42112  naddcnffo  42114  naddcnfcom  42116  naddcnfid1  42117  expgrowth  43094  fpmd  43968  abslt2sqd  44070  ioondisj2  44206  ioondisj1  44207  eliocre  44222  ioossioobi  44230  iooiinicc  44255  iooiinioc  44269  icossico2  44277  lptioo2  44347  limcresiooub  44358  limsupequzlem  44438  xlimmnfvlem2  44549  xlimpnfvlem2  44553  cncfuni  44602  cncfiooicclem1  44609  cxpcncf2  44615  dvcnre  44632  dvresntr  44634  dvresioo  44637  dvbdfbdioolem1  44644  dvnmptdivc  44654  dvnxpaek  44658  itgsinexplem1  44670  itgcoscmulx  44685  itgiccshift  44696  itgperiod  44697  ovolsplit  44704  stoweidlem11  44727  stoweidlem26  44742  stoweidlem34  44750  stoweidlem36  44752  stoweidlem38  44754  stirlinglem5  44794  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem20  44843  fourierdlem58  44880  fourierdlem72  44894  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem79  44901  fourierdlem80  44902  fourierdlem87  44909  fourierdlem94  44916  fourierdlem103  44925  fourierdlem104  44926  fourierdlem107  44929  fourierdlem113  44935  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  etransclem46  44996  etransclem47  44997  rrndistlt  45006  rrnprjdstle  45017  ioorrnopnxrlem  45022  sge0ssre  45113  sge0seq  45162  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmvlelem1  45311  hoidifhspdmvle  45336  hoiqssbllem2  45339  ovolval5lem2  45369  iinhoiicc  45390  iunhoiioo  45392  vonioolem2  45397  vonicclem2  45400  issmflem  45443  iccpartdisj  46105  m1expevenALTV  46315  fpprel2  46409  tgoldbach  46485  strisomgrop  46508  rngqiprngimfo  46786  rngqiprngfulem4  46799  nn0eo  47214  fdivpm  47229  refdivpm  47230  elbigolo1  47243  logbpw2m1  47253  fllog2  47254  dignn0flhalflem1  47301  dignn0flhalflem2  47302  itsclinecirc0in  47461  2itscplem2  47465  itscnhlinecirc02plem1  47468  iccdisj2  47530