Theorem syl22anc 1319

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  preqsnd  4330  fr2nr  5016  soltmin  5451  f1oprg  6093  f1prex  6439  fveqf1o  6457  weniso  6504  fr3nr  6871  smogt  7351  smorndom  7352  oacomf1o  7532  difsnen  7927  undom  7933  enfixsn  7954  domss2  8004  ssenen  8019  marypha1lem  8222  fisupcl  8258  ordtypelem3  8308  ordtypelem8  8313  oieu  8327  oismo  8328  wofib  8333  wemaplem2  8335  wemapso  8339  wemapso2lem  8340  unxpwdom2  8376  infdifsn  8437  oemapvali  8464  cantnflem1c  8467  cantnflem1  8469  cantnf  8473  cnfcom3  8484  r1ordg  8524  dif1card  8716  infxpenlem  8719  dfac8clem  8738  infxp  8920  infmap2  8923  cflim2  8968  coftr  8978  fin2i2  9023  enfin2i  9026  fin23lem26  9030  fin23lem27  9033  fin23lem40  9056  isf32lem2  9059  isf32lem3  9060  isf32lem4  9061  isf32lem7  9064  isf32lem9  9066  fin1a2lem13  9117  fin12  9118  alephexp1  9280  gchdomtri  9330  fpwwe2lem12  9342  fpwwe2lem13  9343  gchpwdom  9371  gchhar  9380  adderpqlem  9655  mulerpqlem  9656  addassnq  9659  mulassnq  9660  distrnq  9662  mulidnq  9664  recmulnq  9665  ltexnq  9676  distrlem1pr  9726  distrlem4pr  9727  prlem936  9748  reclem3pr  9750  mulcmpblnr  9771  mulgt0d  10071  mul4d  10127  add4d  10143  add42d  10144  subcan  10215  addsub4d  10318  subadd4d  10319  sub4d  10320  2addsubd  10321  addsubeq4d  10322  muladdd  10368  mulsubd  10369  addgegt0d  10480  addge0d  10482  mulge0d  10483  le2addd  10525  le2subd  10526  ltleaddd  10527  leltaddd  10528  lt2subd  10530  divdivdiv  10605  divcan5  10606  divne0d  10696  recdivd  10697  recdiv2d  10698  divcan6d  10699  ddcand  10700  rec11d  10701  divmuldivd  10721  divmul13d  10722  divmul24d  10723  divadddivd  10724  divsubdivd  10725  divmuleqd  10726  divdivdivd  10727  subrecd  10735  mulge0b  10772  recreclt  10801  divgt0d  10838  mulgt1d  10839  lemulge11d  10840  lemulge12d  10841  ltmul12ad  10844  lemul12ad  10845  lemul12bd  10846  supmul1  10869  nndivtr  10939  qreccl  11684  ledivdivd  11773  lediv12ad  11807  lt2mul2divd  11815  xlt2add  11962  supxrun  12018  supxrre  12029  infxrre  12038  elicore  12097  iccss2  12115  iccssico2  12118  lincmb01cmp  12186  iccf1o  12187  fzrev2i  12275  fz1fzo0m1  12383  2tnp1ge0ge0  12492  m1modnnsub1  12578  modaddmodup  12595  modaddmodlo  12596  modsubdir  12601  fzennn  12629  sermono  12695  mulexpz  12762  expaddz  12766  ltexp2a  12774  leexp2a  12778  sqdiv  12790  expmulnbnd  12858  digit1  12860  expsubd  12881  lt2sqd  12905  le2sqd  12906  sq11d  12907  bcm1k  12964  bcp1n  12965  bcp1nk  12966  hashf1lem1  13096  cshw1  13419  2swrd2eqwrdeq  13544  ofccat  13556  absrele  13896  sqreulem  13947  sqrtmuld  14011  sqrtsq2d  14012  sqrtled  14013  sqrtltd  14014  sqr11d  14015  abs3lemd  14048  rlimuni  14129  climuni  14131  lo1resb  14143  o1resb  14145  2clim  14151  addcn2  14172  mulcn2  14174  o1of2  14191  o1rlimmul  14197  lo1add  14205  lo1mul  14206  isercolllem1  14243  caucvgrlem  14251  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  mptfzshft  14352  fsumrev  14353  fsum0diag2  14357  binomlem  14400  climcndslem1  14420  climcndslem2  14421  harmonic  14430  mertenslem1  14455  fprodser  14518  fprodrev  14546  rprisefaccl  14593  efcllem  14647  moddvds  14829  dvds1  14879  dvdsext  14881  oexpneg  14907  evennn02n  14912  evennn2n  14913  bitsinv1  15002  sadaddlem  15026  sadasslem  15030  sadeq  15032  mulgcd  15103  dvdssqlem  15117  lcmftp  15187  rpmulgcd2  15208  coprmproddvdslem  15214  isprm5  15257  isprm6  15264  crth  15321  eulerthlem2  15325  prmdiveq  15329  pythagtriplem11  15368  pythagtriplem13  15370  iserodd  15378  pcgcd1  15419  pcprmpw2  15424  pcaddlem  15430  fldivp1  15439  4sqlem12  15498  4sqlem14  15500  4sqlem15  15501  4sqlem16  15502  vdwapun  15516  mreexexlem4d  16130  acsfn1  16145  acsfn2  16147  sscpwex  16298  rescabs  16316  yonedainv  16744  subm0  17179  pmtrfb  17708  psgnunilem1  17736  odmodnn0  17782  odeq  17792  dfod2  17804  sylow1lem1  17836  lsmsubg  17892  lsmmod  17911  lsmdisj2  17918  ghmplusg  18072  odadd  18076  gexexlem  18078  lt6abl  18119  cyggex2  18121  dprdfinv  18241  dmdprdsplitlem  18259  dpjidcl  18280  ablfacrp  18288  ablfacrp2  18289  ablfac1c  18293  ablfac1eu  18295  lcomfsupp  18726  lssvancl1  18766  lssvnegcl  18777  lspprvacl  18820  lspsneli  18822  lspsn  18823  lmhmplusg  18865  lmhmima  18868  lmhmpreima  18869  reslmhm  18873  lbsind2  18902  lsmcl  18904  lsmelval2  18906  lsppreli  18911  lspprabs  18916  pj1lmhm  18921  lssvs0or  18931  lspabs3  18942  lspfixed  18949  lspexch  18950  lsmcv  18962  lspsolv  18964  lidlmcl  19038  drngnidl  19050  2idlcpbl  19055  mplbas2  19291  evlslem3  19335  evlslem1  19336  coe1addfv  19456  lply1binom  19497  evl1addd  19526  evl1subd  19527  evl1muld  19528  gzrngunit  19631  zringlpirlem3  19653  prmirredlem  19660  znf1o  19719  znunithash  19732  frlmsubgval  19927  frlmvscaval  19929  frlmphllem  19938  frlmphl  19939  frlmssuvc1  19952  frlmsslsp  19954  frlmup1  19956  frlmup2  19957  lindfind2  19976  lindfrn  19979  f1lindf  19980  islindf4  19996  mamudi  20028  mamudir  20029  1marepvmarrepid  20200  mdetrlin  20227  smadiadetglem1  20296  smadiadetg  20298  cramerimplem1  20308  mat2pmatscmxcl  20364  m2pmfzgsumcl  20372  pmatcollpw  20405  pmatcollpwfi  20406  pmatcollpw3fi1lem1  20410  cpmidpmatlem2  20495  cpmadugsumlemF  20500  chcoeffeqlem  20509  ntrin  20675  topssnei  20738  restbas  20772  restntr  20796  cnntri  20885  fiuncmp  21017  nllyrest  21099  nllyidm  21102  hausllycmp  21107  cldllycmp  21108  hauspwdom  21114  txcld  21216  txcn  21239  txlly  21249  txnlly  21250  txhaus  21260  txlm  21261  txkgen  21265  xkococnlem  21272  cnmpt2res  21290  xkoinjcn  21300  basqtop  21324  qtopeu  21329  trfbas2  21457  neifil  21494  hausflim  21595  alexsubALTlem2  21662  cnextfval  21676  cnextfvval  21679  cnextf  21680  cnextfres  21683  clssubg  21722  utop2nei  21864  utop3cls  21865  utopreg  21866  psmetlecl  21930  xmetlecl  21961  prdsxmetlem  21983  bldisj  22013  imasf1obl  22103  prdsbl  22106  stdbdmet  22131  stdbdmopn  22133  met2ndci  22137  metcnp  22156  metustto  22168  metustexhalf  22171  cfilucfil  22174  metucn  22186  lssnlm  22315  nmotri  22353  nmoid  22356  tgioo  22407  blcvx  22409  xrsmopn  22423  reperflem  22429  reconnlem2  22438  opnreen  22442  metdsge  22460  metdsre  22464  metdscnlem  22466  metnrmlem1a  22469  metnrmlem1  22470  metnrmlem3  22472  cncfmet  22519  cnmpt2pc  22535  icopnfcnv  22549  icopnfhmeo  22550  cnllycmp  22563  evth  22566  lebnumii  22573  nmoleub2lem3  22723  iscfil2  22872  cfil3i  22875  iscfil3  22879  cfilfcls  22880  iscau3  22884  iscmet3lem2  22898  caubl  22914  lmcau  22919  rrxcph  22988  minveclem2  23005  pjthlem1  23016  pjthlem2  23017  ivthicc  23034  ovollecl  23058  ovolunlem1a  23071  ovolunnul  23075  ovoliunlem1  23077  ismbl2  23102  nulmbl2  23111  unmbl  23112  volun  23120  voliunlem2  23126  ioombl1lem2  23134  uniioombllem2a  23156  uniioombllem3  23159  uniioombllem4  23160  dyaddisjlem  23169  dyadmaxlem  23171  opnmbllem  23175  volsup2  23179  volcn  23180  ismbfd  23213  mbfi1fseqlem1  23288  mbfi1fseqlem5  23292  itg2lecl  23311  itg2monolem2  23324  itg2gt0  23333  itgspliticc  23409  ellimc3  23449  limcres  23456  dvfval  23467  dvres3  23483  dvres3a  23484  dvnff  23492  dvnadd  23498  dvn2bss  23499  dvnres  23500  dvcmul  23513  dvcmulf  23514  dvmptres3  23525  dvmptres2  23531  dvmptntr  23540  dvexp3  23545  dvferm1lem  23551  dvlip  23560  dvlipcn  23561  dvlip2  23562  c1liplem1  23563  dvgt0lem1  23569  dvgt0lem2  23570  dvne0  23578  lhop1lem  23580  lhop2  23582  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcvx  23587  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  ftc1lem6  23608  ftc1  23609  ftc2ditglem  23612  itgsubstlem  23615  tdeglem4  23624  mdegaddle  23638  mdegmullem  23642  ply1rem  23727  fta1glem2  23730  fta1blem  23732  ig1peu  23735  ig1pdvds  23740  dgrmulc  23831  dgrcolem1  23833  plydivlem4  23855  plydiveu  23857  fta1lem  23866  vieta1lem1  23869  vieta1lem2  23870  plyexmo  23872  taylfvallem1  23915  taylfval  23917  tayl0  23920  taylplem1  23921  taylply2  23926  taylply  23927  dvtaylp  23928  dvntaylp  23929  dvntaylp0  23930  taylthlem1  23931  taylthlem2  23932  ulmcaulem  23952  ulmcau  23953  ulmcn  23957  ulmdvlem1  23958  radcnvlem1  23971  radcnvle  23978  psercn  23984  pserdvlem2  23986  pserdv  23987  abelth  23999  cosordlem  24081  tanregt0  24089  dvlog2lem  24198  efopn  24204  logtayllem  24205  logccv  24209  cxplt3  24246  cxpmul2zd  24262  cxpltd  24265  cxpled  24266  cxplt3d  24278  cxple3d  24279  dvsqrt  24283  cxpcn3  24289  cxpaddle  24293  cxpeq  24298  angcan  24332  angvald  24334  ang180lem2  24340  ang180  24344  isosctrlem3  24350  dquartlem1  24378  atantayl2  24465  leibpilem1  24467  leibpi  24469  log2tlbnd  24472  birthdaylem3  24480  xrlimcnp  24495  efrlim  24496  o1cxp  24501  jensenlem2  24514  jensen  24515  fsumharmonic  24538  lgamucov  24564  lgamcvg2  24581  wilthlem1  24594  basellem3  24609  basellem6  24612  basellem8  24614  ppisval  24630  chtwordi  24682  ppiwordi  24688  mumullem2  24706  dvdsmulf1o  24720  fsumvma  24738  fsumvma2  24739  chpchtsum  24744  chpub  24745  logfacubnd  24746  dchrmulcl  24774  dchrinv  24786  dchrptlem1  24789  dchrptlem2  24790  sumdchr2  24795  dchr2sum  24798  bposlem7  24815  lgslem1  24822  lgslem3  24824  lgsdirprm  24856  lgsqrlem2  24872  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem4  24903  lgseisen  24904  lgsquadlem1  24905  lgsquad2lem1  24909  lgsquad3  24912  m1lgs  24913  2sqlem7  24949  chebbnd1lem2  24959  chebbnd1lem3  24960  rplogsumlem1  24973  rpvmasumlem  24976  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasumlema  24989  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0re  25002  logdivsum  25022  pntrsumbnd2  25056  pntpbnd1a  25074  pntpbnd1  25075  pntibndlem2  25080  pntlemr  25091  pntlemj  25092  pntlemf  25094  pnt2  25102  padicabv  25119  ostth2lem2  25123  f1otrg  25551  brbtwn2  25585  colinearalglem2  25587  axcgrtr  25595  axcgrid  25596  axsegconlem7  25603  axsegcon  25607  ax5seglem3  25611  ax5seglem6  25614  ax5seg  25618  axpaschlem  25620  axlowdimlem17  25638  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  ecgrtg  25663  usgraidx2v  25922  iseupa  26492  eupap1  26503  eupath2lem3  26506  numclwwlkovf2ex  26613  nmobndi  27014  ubthlem2  27111  ubthlem3  27112  minvecolem2  27115  shuni  27543  pjhthlem1  27634  chscllem2  27881  pjcompi  27915  mayete3i  27971  unoplin  28163  hmoplin  28185  nmophmi  28274  mdslmd4i  28576  isoun  28862  xrge0addcld  28917  xrofsup  28923  eliccelico  28929  elicoelioo  28930  difioo  28934  rexdiv  28965  2sqmod  28979  xrge0addgt0  29022  omndadd2d  29039  omndadd2rd  29040  omndmul2  29043  ofldchr  29145  mdetpmtr2  29218  mdetpmtr12  29219  madjusmdetlem1  29221  madjusmdetlem4  29224  unitdivcld  29275  xrge0mulc1cn  29315  qqhnm  29362  esumcst  29452  esumfsup  29459  esumpmono  29468  esumcvg  29475  difelsiga  29523  sigapisys  29545  sigapildsys  29552  ldgenpisyslem1  29553  1stmbfm  29649  2ndmbfm  29650  dya2icoseg  29666  sibfinima  29728  probmeasb  29819  orvcgteel  29856  orvclteel  29861  ballotlemsima  29904  ballotlemfrceq  29917  sgnmul  29931  ccatmulgnn0dir  29945  subfacp1lem2a  30416  subfaclim  30424  erdsze2lem2  30440  cvmliftlem2  30522  cvmliftlem10  30530  cvmliftlem13  30532  cvmliftiota  30537  cvmlift2lem9  30547  cvmlift2lem11  30549  cvmlift2lem12  30550  cvmliftphtlem  30553  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  snmlff  30565  mrsubfval  30659  trpredelss  30976  trpredpo  30979  wzel  31015  wzelOLD  31016  wsuclem  31017  wsuclemOLD  31018  nodenselem5  31084  nobndlem6  31096  brsegle  31385  opnregcld  31495  addgtge0d  31666  fin2so  32566  poimirlem17  32596  poimirlem23  32602  opnmbllem0  32615  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  itg2addnc  32634  itg2gt0cn  32635  ftc1cnnclem  32653  ftc1cnnc  32654  areacirclem5  32674  indexdom  32699  sstotbnd2  32743  isbnd3  32753  isbnd3b  32754  cntotbnd  32765  ismtyima  32772  heibor1lem  32778  heiborlem8  32787  rrncmslem  32801  reheibor  32808  lkrlsp  33407  lshpkrlem5  33419  ldualssvscl  33463  ldualssvsubcl  33464  llnmlplnN  33843  llncvrlpln  33862  pmapjat1  34157  pclfinN  34204  lautlt  34395  lauteq  34399  lautco  34401  ltrn11  34430  ltrnle  34433  ltrneq2  34452  cdlemednuN  34605  cdleme20k  34625  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21c  34633  cdleme22e  34650  cdleme22eALTN  34651  cdlemefrs32fva  34706  cdlemg4g  34922  cdlemg18b  34985  cdlemg18c  34986  cdlemj3  35129  dia2dimlem5  35375  dvhopN  35423  cdlemm10N  35425  dihjatcclem4  35728  dochexmidlem2  35768  lclkrlem2o  35828  lcfrlem5  35853  lcfrlem6  35854  lcdlssvscl  35913  mapdpglem6  35985  mapdpglem9  35987  mapdpglem12  35990  mapdpglem14  35992  mapdindp0  36026  hdmaprnlem7N  36165  hdmaprnlem8N  36166  hdmaprnlem3eN  36168  hgmapvvlem3  36235  mzpsubst  36329  eldioph2lem1  36341  eldioph2lem2  36342  eldioph2b  36344  diophin  36354  irrapxlem2  36405  irrapxlem4  36407  irrapxlem5  36408  pellexlem1  36411  pellexlem2  36412  pellexlem6  36416  elpell1qr2  36454  pell1qrgaplem  36455  pell1qrgap  36456  pellqrex  36461  pellfundex  36468  pellfund14  36480  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  rmxyadd  36504  expmordi  36530  rmxypos  36532  jm2.24  36548  congsub  36555  mzpcong  36557  congrep  36558  acongtr  36563  acongrep  36565  jm2.19lem1  36574  jm2.22  36580  jm2.23  36581  jm2.26lem3  36586  jm2.26  36587  jm2.27a  36590  fnwe2lem2  36639  aomclem6  36647  hbtlem2  36713  hbtlem4  36715  hbtlem5  36717  dgraa0p  36738  rngunsnply  36762  acsfn1p  36788  proot1hash  36797  itgpowd  36819  expgrowth  37556  abslt2sqd  38517  ioondisj2  38561  ioondisj1  38562  eliocre  38581  ioossioobi  38590  iooiinicc  38616  iooiinioc  38630  lptioo2  38698  limcresiooub  38709  cncfuni  38772  cncfiooicclem1  38779  cxpcncf2  38786  dvcnre  38804  dvresntr  38806  dvmptresicc  38809  dvresioo  38811  dvbdfbdioolem1  38818  dvnmptdivc  38828  dvnxpaek  38832  itgsinexplem1  38845  itgcoscmulx  38861  itgiccshift  38872  itgperiod  38873  ovolsplit  38881  stoweidlem11  38904  stoweidlem26  38919  stoweidlem34  38927  stoweidlem36  38929  stoweidlem38  38931  stirlinglem5  38971  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem20  39020  fourierdlem58  39057  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem79  39078  fourierdlem80  39079  fourierdlem87  39086  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem113  39112  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem46  39173  etransclem47  39174  rrndistlt  39186  rrnprjdstle  39197  ioorrnopnxrlem  39202  sge0ssre  39290  sge0seq  39339  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmvlelem1  39485  hoidifhspdmvle  39510  hoiqssbllem2  39513  ovolval5lem2  39543  iinhoiicc  39565  iunhoiioo  39567  vonioolem2  39572  vonicclem2  39575  issmflem  39613  iccpartdisj  39975  m1expevenALTV  40098  oexpnegALTV  40126  tgoldbach  40232  tgoldbachOLD  40239  usgredg2v  40454  2trlond  41146  eupthp1  41384  av-numclwwlkovf2ex  41517  nn0eo  42116  fdivpm  42135  refdivpm  42136  elbigolo1  42149  logbpw2m1  42159  fllog2  42160  dignn0flhalflem1  42207  dignn0flhalflem2  42208