Theorem syl22anc 836

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  preqsnd  4782  fr2nr  5527  soltmin  5990  f1oprg  6653  f1prex  7034  fveqf1o  7052  weniso  7101  fr3nr  7488  suppofssd  7861  smogt  7998  smorndom  7999  oacomf1o  8185  enpr2d  8591  difsnen  8593  undom  8599  enfixsn  8620  domss2  8670  ssenen  8685  marypha1lem  8891  fisupcl  8927  ordtypelem3  8978  ordtypelem8  8983  oieu  8997  oismo  8998  wofib  9003  wemaplem2  9005  wemapso  9009  wemapso2lem  9010  unxpwdom2  9046  infdifsn  9114  oemapvali  9141  cantnflem1c  9144  cantnflem1  9146  cantnf  9150  cnfcom3  9161  r1ordg  9201  dif1card  9430  infxpenlem  9433  dfac8clem  9452  infxp  9631  infmap2  9634  cflim2  9679  coftr  9689  fin2i2  9734  enfin2i  9737  fin23lem26  9741  fin23lem27  9744  fin23lem40  9767  isf32lem2  9770  isf32lem3  9771  isf32lem4  9772  isf32lem7  9775  isf32lem9  9777  fin1a2lem13  9828  fin12  9829  alephexp1  9995  gchdomtri  10045  fpwwe2lem12  10057  fpwwe2lem13  10058  gchpwdom  10086  gchhar  10095  adderpqlem  10370  mulerpqlem  10371  addassnq  10374  mulassnq  10375  distrnq  10377  mulidnq  10379  recmulnq  10380  ltexnq  10391  distrlem1pr  10441  distrlem4pr  10442  prlem936  10463  reclem3pr  10465  mulcmpblnr  10487  mulgt0d  10789  mul4d  10846  add4d  10862  add42d  10863  subcan  10935  addsub4d  11038  subadd4d  11039  sub4d  11040  2addsubd  11041  addsubeq4d  11042  muladdd  11092  mulsubd  11093  addgegt0d  11207  addgtge0d  11208  addge0d  11210  mulge0d  11211  le2addd  11253  le2subd  11254  ltleaddd  11255  leltaddd  11256  lt2subd  11258  divdivdiv  11335  divcan5  11336  divne0d  11426  recdivd  11427  recdiv2d  11428  divcan6d  11429  ddcand  11430  rec11d  11431  divmuldivd  11451  divmul13d  11452  divmul24d  11453  divadddivd  11454  divsubdivd  11455  divmuleqd  11456  divdivdivd  11457  subrecd  11465  mulge0b  11504  recreclt  11533  divgt0d  11569  mulgt1d  11570  lemulge11d  11571  lemulge12d  11572  ltmul12ad  11575  lemul12ad  11576  lemul12bd  11577  supmul1  11604  nndivtr  11678  qreccl  12362  ledivdivd  12450  lediv12ad  12484  lt2mul2divd  12494  xlt2add  12647  supxrun  12703  supxrre  12714  infxrre  12723  elicore  12783  iccss2  12801  iccssico2  12804  lincmb01cmp  12875  iccf1o  12876  fzrev2i  12966  2tnp1ge0ge0  13193  m1modnnsub1  13279  modaddmodup  13296  modaddmodlo  13297  modsubdir  13302  fzennn  13330  sermono  13396  mulexpz  13463  expaddz  13467  sqdiv  13481  expsubd  13515  ltexp2a  13524  expmordi  13525  leexp2a  13530  expmulnbnd  13590  digit1  13592  lt2sqd  13613  le2sqd  13614  sq11d  13615  bcm1k  13669  bcp1n  13670  bcp1nk  13671  hashf1lem1  13807  cshw1  14178  2swrd2eqwrdeq  14309  ofccat  14323  absrele  14662  sqreulem  14713  sqrtmuld  14778  sqrtsq2d  14779  sqrtled  14780  sqrtltd  14781  sqr11d  14782  abs3lemd  14815  rlimuni  14901  climuni  14903  lo1resb  14915  o1resb  14917  2clim  14923  addcn2  14944  mulcn2  14946  o1of2  14963  o1rlimmul  14969  lo1add  14977  lo1mul  14978  isercolllem1  15015  caucvgrlem  15023  iseraltlem2  15033  iseraltlem3  15034  mptfzshft  15127  fsumrev  15128  fsum0diag2  15132  binomlem  15178  climcndslem1  15198  climcndslem2  15199  harmonic  15208  mertenslem1  15234  fprodser  15297  fprodrev  15325  efcllem  15425  moddvds  15612  dvds1  15663  dvdsext  15665  evennn2n  15694  bitsinv1  15785  sadaddlem  15809  sadasslem  15813  sadeq  15815  mulgcd  15890  dvdssqlem  15904  lcmftp  15974  rpmulgcd2  15994  coprmproddvdslem  16000  isprm5  16045  isprm6  16052  crth  16109  eulerthlem2  16113  prmdiveq  16117  pythagtriplem11  16156  pythagtriplem13  16158  pcgcd1  16207  pcprmpw2  16212  pcaddlem  16218  fldivp1  16227  4sqlem12  16286  4sqlem14  16288  4sqlem15  16289  4sqlem16  16290  vdwapun  16304  mreexexlem4d  16912  acsfn1  16926  acsfn2  16928  sscpwex  17079  rescabs  17097  yonedainv  17525  subm0  17974  pmtrfb  18587  psgnunilem1  18615  odmodnn0  18662  odeq  18672  dfod2  18685  sylow1lem1  18717  lsmsubg  18773  lsmmod  18795  lsmdisj2  18802  ghmplusg  18960  odadd  18964  gexexlem  18966  lt6abl  19009  cyggex2  19011  dprdfinv  19135  dmdprdsplitlem  19153  dpjidcl  19174  ablfacrp  19182  ablfacrp2  19183  ablfac1c  19187  ablfac1eu  19189  acsfn1p  19572  lcomfsupp  19668  lssvancl1  19710  lssvnegcl  19722  lspprvacl  19765  lspsneli  19767  lspsn  19768  lmhmplusg  19810  lmhmima  19813  lmhmpreima  19814  reslmhm  19818  lbsind2  19847  lsmcl  19849  lsmelval2  19851  lsppreli  19856  lspprabs  19861  pj1lmhm  19866  lssvs0or  19876  lspabs3  19887  lspfixed  19894  lspexch  19895  lsmcv  19907  lspsolv  19909  lidlmcl  19984  drngnidl  19996  2idlcpbl  20001  mplbas2  20245  evlslem3  20287  evlslem1  20289  coe1addfv  20427  lply1binom  20468  evl1addd  20498  evl1subd  20499  evl1muld  20500  gzrngunit  20605  zringlpirlem3  20627  prmirredlem  20634  znf1o  20692  znunithash  20705  frlmsubgval  20903  frlmvplusgvalc  20905  frlmvscaval  20906  frlmphllem  20918  frlmphl  20919  frlmssuvc1  20932  frlmsslsp  20934  frlmup1  20936  frlmup2  20937  lindfind2  20956  lindfrn  20959  f1lindf  20960  islindf4  20976  mamudi  21006  mamudir  21007  1marepvmarrepid  21178  mdetrlin  21205  smadiadetglem1  21274  smadiadetg  21276  cramerimplem1  21286  mat2pmatscmxcl  21342  m2pmfzgsumcl  21350  pmatcollpw  21383  pmatcollpwfi  21384  pmatcollpw3fi1lem1  21388  cpmidpmatlem2  21473  cpmadugsumlemF  21478  chcoeffeqlem  21487  ntrin  21663  topssnei  21726  restbas  21760  restntr  21784  cnntri  21873  fiuncmp  22006  nllyrest  22088  nllyidm  22091  hausllycmp  22096  cldllycmp  22097  hauspwdom  22103  txcld  22205  txcn  22228  txlly  22238  txnlly  22239  txhaus  22249  txlm  22250  txkgen  22254  xkococnlem  22261  cnmpt2res  22279  xkoinjcn  22289  basqtop  22313  qtopeu  22318  trfbas2  22445  neifil  22482  hausflim  22583  alexsubALTlem2  22650  cnextfval  22664  cnextfvval  22667  cnextf  22668  cnextfres  22671  clssubg  22711  utop2nei  22853  utop3cls  22854  utopreg  22855  psmetlecl  22919  xmetlecl  22950  prdsxmetlem  22972  bldisj  23002  imasf1obl  23092  prdsbl  23095  stdbdmet  23120  stdbdmopn  23122  met2ndci  23126  metcnp  23145  metustto  23157  metustexhalf  23160  cfilucfil  23163  metucn  23175  lssnlm  23304  nmotri  23342  nmoid  23345  tgioo  23398  blcvx  23400  xrsmopn  23414  reperflem  23420  reconnlem2  23429  opnreen  23433  metdsge  23451  metdsre  23455  metdscnlem  23457  metnrmlem1a  23460  metnrmlem1  23461  metnrmlem3  23463  cncfmet  23510  cnmpopc  23526  icopnfcnv  23540  icopnfhmeo  23541  cnllycmp  23554  evth  23557  lebnumii  23564  nmoleub2lem3  23713  iscfil2  23863  cfil3i  23866  iscfil3  23870  cfilfcls  23871  iscau3  23875  iscmet3lem2  23889  caubl  23905  lmcau  23910  cssbn  23972  rrxcph  23989  minveclem2  24023  pjthlem1  24034  pjthlem2  24035  ivthicc  24053  ovollecl  24078  ovolunlem1a  24091  ovolunnul  24095  ovoliunlem1  24097  ismbl2  24122  nulmbl2  24131  unmbl  24132  volun  24140  voliunlem2  24146  ioombl1lem2  24154  uniioombllem2a  24177  uniioombllem3  24180  uniioombllem4  24181  dyaddisjlem  24190  dyadmaxlem  24192  opnmbllem  24196  volsup2  24200  volcn  24201  ismbfd  24234  mbfi1fseqlem1  24310  mbfi1fseqlem5  24314  itg2lecl  24333  itg2monolem2  24346  itg2gt0  24355  itgspliticc  24431  ellimc3  24471  limcres  24478  dvfval  24489  dvres3  24505  dvres3a  24506  dvnff  24514  dvnadd  24520  dvn2bss  24521  dvnres  24522  dvcmul  24535  dvcmulf  24536  dvmptres3  24547  dvmptres2  24553  dvmptntr  24562  dvexp3  24569  dvferm1lem  24575  dvlip  24584  dvlipcn  24585  dvlip2  24586  c1liplem1  24587  dvgt0lem1  24593  dvgt0lem2  24594  dvne0  24602  lhop1lem  24604  lhop2  24606  lhop  24607  dvcnvrelem1  24608  dvcnvrelem2  24609  dvcvx  24611  dvfsumle  24612  dvfsumabs  24614  dvfsumlem2  24618  ftc1lem6  24632  ftc1  24633  ftc2ditglem  24636  itgsubstlem  24639  tdeglem4  24648  mdegaddle  24662  mdegmullem  24666  ply1rem  24751  fta1glem2  24754  fta1blem  24756  ig1peu  24759  ig1pdvds  24764  dgrmulc  24855  dgrcolem1  24857  plydivlem4  24879  plydiveu  24881  fta1lem  24890  vieta1lem1  24893  vieta1lem2  24894  plyexmo  24896  taylfvallem1  24939  taylfval  24941  tayl0  24944  taylplem1  24945  taylply2  24950  taylply  24951  dvtaylp  24952  dvntaylp  24953  dvntaylp0  24954  taylthlem1  24955  taylthlem2  24956  ulmcaulem  24976  ulmcau  24977  ulmcn  24981  ulmdvlem1  24982  radcnvlem1  24995  radcnvle  25002  psercn  25008  pserdvlem2  25010  pserdv  25011  abelth  25023  tanregt0  25117  dvlog2lem  25229  efopn  25235  logtayllem  25236  logccv  25240  cxplt3  25277  cxpmul2zd  25293  cxpltd  25296  cxpled  25297  cxplt3d  25311  cxple3d  25312  dvsqrt  25317  cxpcn3  25323  cxpaddle  25327  cxpeq  25332  angcan  25374  angvald  25376  ang180lem2  25382  ang180  25386  isosctrlem3  25392  dquartlem1  25423  atantayl2  25510  leibpi  25514  log2tlbnd  25517  birthdaylem3  25525  xrlimcnp  25540  efrlim  25541  o1cxp  25546  jensenlem2  25559  jensen  25560  fsumharmonic  25583  lgamucov  25609  lgamcvg2  25626  wilthlem1  25639  basellem3  25654  basellem6  25657  basellem8  25659  ppisval  25675  chtwordi  25727  ppiwordi  25733  mumullem2  25751  dvdsmulf1o  25765  fsumvma  25783  fsumvma2  25784  chpchtsum  25789  chpub  25790  logfacubnd  25791  dchrmulcl  25819  dchrinv  25831  dchrptlem1  25834  dchrptlem2  25835  sumdchr2  25840  dchr2sum  25843  bposlem7  25860  lgslem1  25867  lgslem3  25869  lgsdirprm  25901  lgsqrlem2  25917  lgseisenlem1  25945  lgseisenlem2  25946  lgseisenlem4  25948  lgseisen  25949  lgsquadlem1  25950  lgsquad2lem1  25954  lgsquad3  25957  m1lgs  25958  2sqlem7  25994  2sq2  26003  2sqmod  26006  chebbnd1lem2  26040  chebbnd1lem3  26041  rplogsumlem1  26054  rpvmasumlem  26057  dchrvmasumlem1  26065  dchrvmasum2lem  26066  dchrvmasumlema  26070  dchrisum0flblem2  26079  dchrisum0fno1  26081  dchrisum0re  26083  logdivsum  26103  pntrsumbnd2  26137  pntpbnd1a  26155  pntpbnd1  26156  pntibndlem2  26161  pntlemr  26172  pntlemj  26173  pntlemf  26175  pnt2  26183  padicabv  26200  ostth2lem2  26204  f1otrg  26651  brbtwn2  26685  colinearalglem2  26687  axcgrtr  26695  axcgrid  26696  axsegconlem7  26703  axsegcon  26707  ax5seglem3  26711  ax5seglem6  26714  ax5seg  26718  axpaschlem  26720  axlowdimlem17  26738  axcontlem2  26745  axcontlem4  26747  axcontlem7  26750  axcontlem8  26751  ecgrtg  26763  usgredg2v  27003  vtxdgoddnumeven  27329  2trlond  27712  eupthp1  27989  nmobndi  28546  ubthlem2  28642  ubthlem3  28643  minvecolem2  28646  shuni  29071  pjhthlem1  29162  chscllem2  29409  pjcompi  29443  mayete3i  29499  unoplin  29691  hmoplin  29713  nmophmi  29802  mdslmd4i  30104  isoun  30431  xrge0addcld  30480  xrofsup  30486  eliccelico  30494  elicoelioo  30495  difioo  30499  rexdiv  30597  xrge0addgt0  30673  omndadd2d  30704  omndadd2rd  30705  omndmul2  30708  cycpmcl  30753  cycpm2tr  30756  cyc3evpm  30787  cycpmconjslem2  30792  freshmansdream  30854  ofldchr  30882  qusker  30913  eqgvscpbl  30914  isprmidlc  30958  qsidomlem1  30960  mxidlprm  30972  ssmxidllem  30973  lindsunlem  31015  finexttrb  31047  mdetpmtr2  31084  mdetpmtr12  31085  madjusmdetlem1  31087  madjusmdetlem4  31090  unitdivcld  31139  xrge0mulc1cn  31179  qqhnm  31226  esumcst  31317  esumfsup  31324  esumpmono  31333  esumcvg  31340  difelsiga  31387  sigapisys  31409  sigapildsys  31416  ldgenpisyslem1  31417  1stmbfm  31513  2ndmbfm  31514  dya2icoseg  31530  sibfinima  31592  probmeasb  31683  orvcgteel  31720  orvclteel  31725  ballotlemsima  31768  ballotlemfrceq  31781  sgnmul  31795  ccatmulgnn0dir  31807  fct2relem  31863  ftc2re  31864  chtvalz  31895  subfacp1lem2a  32422  subfaclim  32430  erdsze2lem2  32446  cvmliftlem2  32528  cvmliftlem10  32536  cvmliftlem13  32538  cvmliftiota  32543  cvmlift2lem9  32553  cvmlift2lem11  32555  cvmlift2lem12  32556  cvmliftphtlem  32559  cvmlift3lem6  32566  cvmlift3lem7  32567  cvmlift3lem9  32569  snmlff  32571  mrsubfval  32750  trpredelss  33066  trpredpo  33069  wzel  33106  wsuclem  33107  sltrec  33273  brsegle  33564  opnregcld  33673  fin2so  34873  poimirlem17  34903  poimirlem23  34909  opnmbllem0  34922  mblfinlem3  34925  mblfinlem4  34926  itg2addnclem  34937  itg2addnc  34940  itg2gt0cn  34941  ftc1cnnclem  34959  ftc1cnnc  34960  areacirclem5  34980  indexdom  35003  sstotbnd2  35046  isbnd3  35056  isbnd3b  35057  cntotbnd  35068  ismtyima  35075  heibor1lem  35081  heiborlem8  35090  rrncmslem  35104  reheibor  35111  lkrlsp  36232  lshpkrlem5  36244  ldualssvscl  36288  ldualssvsubcl  36289  llnmlplnN  36669  llncvrlpln  36688  pmapjat1  36983  pclfinN  37030  lautlt  37221  lauteq  37225  lautco  37227  ltrn11  37256  ltrnle  37259  ltrneq2  37278  cdlemednuN  37430  cdleme20k  37449  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme21c  37457  cdleme22e  37474  cdleme22eALTN  37475  cdlemefrs32fva  37530  cdlemg4g  37746  cdlemg18b  37809  cdlemg18c  37810  cdlemj3  37953  dia2dimlem5  38198  dvhopN  38246  cdlemm10N  38248  dihjatcclem4  38551  dochexmidlem2  38591  lclkrlem2o  38651  lcfrlem5  38676  lcfrlem6  38677  lcdlssvscl  38736  mapdpglem6  38808  mapdpglem9  38810  mapdpglem12  38813  mapdpglem14  38815  mapdindp0  38849  hdmaprnlem7N  38985  hdmaprnlem8N  38986  hdmaprnlem3eN  38988  hgmapvvlem3  39055  mzpsubst  39338  eldioph2lem1  39350  eldioph2lem2  39351  eldioph2b  39353  diophin  39362  irrapxlem2  39413  irrapxlem4  39415  irrapxlem5  39416  pellexlem1  39419  pellexlem2  39420  pellexlem6  39424  elpell1qr2  39462  pell1qrgaplem  39463  pell1qrgap  39464  pellqrex  39469  pellfundex  39476  pellfund14  39488  rmspecsqrtnq  39496  rmxyadd  39511  congsub  39560  mzpcong  39562  congrep  39563  acongtr  39568  acongrep  39570  jm2.19lem1  39579  jm2.22  39585  jm2.23  39586  jm2.26lem3  39591  jm2.26  39592  jm2.27a  39595  fnwe2lem2  39644  aomclem6  39652  hbtlem2  39717  hbtlem4  39719  hbtlem5  39721  dgraa0p  39742  rngunsnply  39766  proot1hash  39793  itgpowd  39814  expgrowth  40660  fpmd  41531  abslt2sqd  41621  ioondisj2  41760  ioondisj1  41761  eliocre  41778  ioossioobi  41786  iooiinicc  41811  iooiinioc  41825  icossico2  41833  lptioo2  41905  limcresiooub  41916  limsupequzlem  41996  xlimmnfvlem2  42107  xlimpnfvlem2  42111  cncfuni  42162  cncfiooicclem1  42169  cxpcncf2  42176  dvcnre  42193  dvresntr  42195  dvmptresicc  42197  dvresioo  42199  dvbdfbdioolem1  42206  dvnmptdivc  42216  dvnxpaek  42220  itgsinexplem1  42232  itgcoscmulx  42247  itgiccshift  42258  itgperiod  42259  ovolsplit  42267  stoweidlem11  42290  stoweidlem26  42305  stoweidlem34  42313  stoweidlem36  42315  stoweidlem38  42317  stirlinglem5  42357  dirkercncflem2  42383  dirkercncflem4  42385  fourierdlem20  42406  fourierdlem58  42443  fourierdlem72  42457  fourierdlem73  42458  fourierdlem74  42459  fourierdlem75  42460  fourierdlem76  42461  fourierdlem79  42464  fourierdlem80  42465  fourierdlem87  42472  fourierdlem94  42479  fourierdlem103  42488  fourierdlem104  42489  fourierdlem107  42492  fourierdlem113  42498  sqwvfoura  42507  sqwvfourb  42508  fourierswlem  42509  fouriersw  42510  etransclem46  42559  etransclem47  42560  rrndistlt  42569  rrnprjdstle  42580  ioorrnopnxrlem  42585  sge0ssre  42673  sge0seq  42722  hsphoidmvle2  42861  hsphoidmvle  42862  hoidmv1lelem1  42867  hoidmv1lelem2  42868  hoidmv1lelem3  42869  hoidmvlelem1  42871  hoidifhspdmvle  42896  hoiqssbllem2  42899  ovolval5lem2  42929  iinhoiicc  42950  iunhoiioo  42952  vonioolem2  42957  vonicclem2  42960  issmflem  42998  iccpartdisj  43591  m1expevenALTV  43806  fpprel2  43900  tgoldbach  43976  strisomgrop  43999  nn0eo  44582  fdivpm  44597  refdivpm  44598  elbigolo1  44611  logbpw2m1  44621  fllog2  44622  dignn0flhalflem1  44669  dignn0flhalflem2  44670  itsclinecirc0in  44756  2itscplem2  44760  itscnhlinecirc02plem1  44763