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 512	. 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 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  4790  fr2nr  5568  soltmin  6046  f1oprg  6770  f1prex  7165  fveqf1o  7184  weniso  7234  fr3nr  7631  suppofssd  8028  smogt  8207  smorndom  8208  oacomf1o  8405  enpr2d  8847  difsnen  8849  undomOLD  8856  enfixsn  8877  domss2  8932  ssenen  8947  marypha1lem  9201  fisupcl  9237  ordtypelem3  9288  ordtypelem8  9293  oieu  9307  oismo  9308  wofib  9313  wemaplem2  9315  wemapso  9319  wemapso2lem  9320  unxpwdom2  9356  infdifsn  9424  oemapvali  9451  cantnflem1c  9454  cantnflem1  9456  cantnf  9460  cnfcom3  9471  r1ordg  9545  dif1card  9775  infxpenlem  9778  dfac8clem  9797  infxp  9980  infmap2  9983  cflim2  10028  coftr  10038  fin2i2  10083  enfin2i  10086  fin23lem26  10090  fin23lem27  10093  fin23lem40  10116  isf32lem2  10119  isf32lem3  10120  isf32lem4  10121  isf32lem7  10124  isf32lem9  10126  fin1a2lem13  10177  fin12  10178  alephexp1  10344  gchdomtri  10394  fpwwe2lem11  10406  fpwwe2lem12  10407  gchpwdom  10435  gchhar  10444  adderpqlem  10719  mulerpqlem  10720  addassnq  10723  mulassnq  10724  distrnq  10726  mulidnq  10728  recmulnq  10729  ltexnq  10740  distrlem1pr  10790  distrlem4pr  10791  prlem936  10812  reclem3pr  10814  mulcmpblnr  10836  mulgt0d  11139  mul4d  11196  add4d  11212  add42d  11213  subcan  11285  addsub4d  11388  subadd4d  11389  sub4d  11390  2addsubd  11391  addsubeq4d  11392  muladdd  11442  mulsubd  11443  addgegt0d  11557  addgtge0d  11558  addge0d  11560  mulge0d  11561  le2addd  11603  le2subd  11604  ltleaddd  11605  leltaddd  11606  lt2subd  11608  divdivdiv  11685  divcan5  11686  divne0d  11776  recdivd  11777  recdiv2d  11778  divcan6d  11779  ddcand  11780  rec11d  11781  divmuldivd  11801  divmul13d  11802  divmul24d  11803  divadddivd  11804  divsubdivd  11805  divmuleqd  11806  divdivdivd  11807  subrecd  11815  mulge0b  11854  recreclt  11883  divgt0d  11919  mulgt1d  11920  lemulge11d  11921  lemulge12d  11922  ltmul12ad  11925  lemul12ad  11926  lemul12bd  11927  supmul1  11953  nndivtr  12029  qreccl  12718  ledivdivd  12806  lediv12ad  12840  lt2mul2divd  12850  xlt2add  13003  supxrun  13059  supxrre  13070  infxrre  13079  elicore  13140  iccss2  13159  iccssico2  13162  lincmb01cmp  13236  iccf1o  13237  fzrev2i  13330  2tnp1ge0ge0  13558  m1modnnsub1  13646  modaddmodup  13663  modaddmodlo  13664  modsubdir  13669  fzennn  13697  sermono  13764  mulexpz  13832  expaddz  13836  sqdiv  13850  expsubd  13884  ltexp2a  13893  expmordi  13894  leexp2a  13899  expmulnbnd  13959  digit1  13961  lt2sqd  13982  le2sqd  13983  sq11d  13984  bcm1k  14038  bcp1n  14039  bcp1nk  14040  hashf1lem1  14177  hashf1lem1OLD  14178  cshw1  14544  2swrd2eqwrdeq  14675  ofccat  14689  absrele  15029  sqreulem  15080  sqrtmuld  15145  sqrtsq2d  15146  sqrtled  15147  sqrtltd  15148  sqr11d  15149  abs3lemd  15182  rlimuni  15268  climuni  15270  lo1resb  15282  o1resb  15284  2clim  15290  addcn2  15312  mulcn2  15314  o1of2  15331  o1rlimmul  15337  lo1add  15345  lo1mul  15346  isercolllem1  15385  caucvgrlem  15393  iseraltlem2  15403  iseraltlem3  15404  mptfzshft  15499  fsumrev  15500  fsum0diag2  15504  binomlem  15550  climcndslem1  15570  climcndslem2  15571  harmonic  15580  mertenslem1  15605  fprodser  15668  fprodrev  15696  efcllem  15796  moddvds  15983  dvds1  16037  dvdsext  16039  evennn2n  16069  bitsinv1  16158  sadaddlem  16182  sadasslem  16186  sadeq  16188  mulgcd  16265  dvdssqlem  16280  lcmftp  16350  rpmulgcd2  16370  coprmproddvdslem  16376  isprm5  16421  isprm6  16428  crth  16488  eulerthlem2  16492  prmdiveq  16496  pythagtriplem11  16535  pythagtriplem13  16537  pcgcd1  16587  pcprmpw2  16592  pcaddlem  16598  fldivp1  16607  4sqlem12  16666  4sqlem14  16668  4sqlem15  16669  4sqlem16  16670  vdwapun  16684  mreexexlem4d  17365  acsfn1  17379  acsfn2  17381  sscpwex  17536  rescabs  17556  rescabsOLD  17557  yonedainv  18008  subm0  18463  pmtrfb  19082  psgnunilem1  19110  odmodnn0  19157  odeq  19167  dfod2  19180  sylow1lem1  19212  lsmsubg  19268  lsmmod  19290  lsmdisj2  19297  ghmplusg  19456  odadd  19460  gexexlem  19462  lt6abl  19505  cyggex2  19507  dprdfinv  19631  dmdprdsplitlem  19649  dpjidcl  19670  ablfacrp  19678  ablfacrp2  19679  ablfac1c  19683  ablfac1eu  19685  acsfn1p  20076  lcomfsupp  20172  lssvancl1  20215  lssvnegcl  20227  lspprvacl  20270  lspsneli  20272  lspsn  20273  lmhmplusg  20315  lmhmima  20318  lmhmpreima  20319  reslmhm  20323  lbsind2  20352  lsmcl  20354  lsmelval2  20356  lsppreli  20361  lspprabs  20366  pj1lmhm  20371  lssvs0or  20381  lspabs3  20392  lspfixed  20399  lspexch  20400  lsmcv  20412  lspsolv  20414  lidlmcl  20497  drngnidl  20509  2idlcpbl  20514  gzrngunit  20673  zringlpirlem3  20695  prmirredlem  20703  znf1o  20768  znunithash  20781  frlmsubgval  20981  frlmvplusgvalc  20983  frlmvscaval  20984  frlmphllem  20996  frlmphl  20997  frlmssuvc1  21010  frlmsslsp  21012  frlmup1  21014  frlmup2  21015  lindfind2  21034  lindfrn  21037  f1lindf  21038  islindf4  21054  mplbas2  21252  evlslem3  21299  evlslem1  21301  coe1addfv  21445  lply1binom  21486  evl1addd  21516  evl1subd  21517  evl1muld  21518  mamudi  21559  mamudir  21560  1marepvmarrepid  21733  mdetrlin  21760  smadiadetglem1  21829  smadiadetg  21831  cramerimplem1  21841  mat2pmatscmxcl  21898  m2pmfzgsumcl  21906  pmatcollpw  21939  pmatcollpwfi  21940  pmatcollpw3fi1lem1  21944  cpmidpmatlem2  22029  cpmadugsumlemF  22034  chcoeffeqlem  22043  ntrin  22221  topssnei  22284  restbas  22318  restntr  22342  cnntri  22431  fiuncmp  22564  nllyrest  22646  nllyidm  22649  hausllycmp  22654  cldllycmp  22655  hauspwdom  22661  txcld  22763  txcn  22786  txlly  22796  txnlly  22797  txhaus  22807  txlm  22808  txkgen  22812  xkococnlem  22819  cnmpt2res  22837  xkoinjcn  22847  basqtop  22871  qtopeu  22876  trfbas2  23003  neifil  23040  hausflim  23141  alexsubALTlem2  23208  cnextfval  23222  cnextfvval  23225  cnextf  23226  cnextfres  23229  clssubg  23269  utop2nei  23411  utop3cls  23412  utopreg  23413  psmetlecl  23477  xmetlecl  23508  prdsxmetlem  23530  bldisj  23560  imasf1obl  23653  prdsbl  23656  stdbdmet  23681  stdbdmopn  23683  met2ndci  23687  metcnp  23706  metustto  23718  metustexhalf  23721  cfilucfil  23724  metucn  23736  lssnlm  23874  nmotri  23912  nmoid  23915  tgioo  23968  blcvx  23970  xrsmopn  23984  reperflem  23990  reconnlem2  23999  opnreen  24003  metdsge  24021  metdsre  24025  metdscnlem  24027  metnrmlem1a  24030  metnrmlem1  24031  metnrmlem3  24033  cncfmet  24081  cnmpopc  24100  icopnfcnv  24114  icopnfhmeo  24115  cnllycmp  24128  evth  24131  lebnumii  24138  nmoleub2lem3  24287  iscfil2  24439  cfil3i  24442  iscfil3  24446  cfilfcls  24447  iscau3  24451  iscmet3lem2  24465  caubl  24481  lmcau  24486  cssbn  24548  rrxcph  24565  minveclem2  24599  pjthlem1  24610  pjthlem2  24611  ivthicc  24631  ovollecl  24656  ovolunlem1a  24669  ovolunnul  24673  ovoliunlem1  24675  ismbl2  24700  nulmbl2  24709  unmbl  24710  volun  24718  voliunlem2  24724  ioombl1lem2  24732  uniioombllem2a  24755  uniioombllem3  24758  uniioombllem4  24759  dyaddisjlem  24768  dyadmaxlem  24770  opnmbllem  24774  volsup2  24778  volcn  24779  ismbfd  24812  mbfi1fseqlem1  24889  mbfi1fseqlem5  24893  itg2lecl  24912  itg2monolem2  24925  itg2gt0  24934  itgspliticc  25010  ellimc3  25052  limcres  25059  dvfval  25070  dvres3  25086  dvres3a  25087  dvmptresicc  25089  dvnff  25096  dvnadd  25102  dvn2bss  25103  dvnres  25104  dvcmul  25117  dvcmulf  25118  dvmptres3  25129  dvmptres2  25135  dvmptntr  25144  dvexp3  25151  dvferm1lem  25157  dvlip  25166  dvlipcn  25167  dvlip2  25168  c1liplem1  25169  dvgt0lem1  25175  dvgt0lem2  25176  dvne0  25184  lhop1lem  25186  lhop2  25188  lhop  25189  dvcnvrelem1  25190  dvcnvrelem2  25191  dvcvx  25193  dvfsumle  25194  dvfsumabs  25196  dvfsumlem2  25200  ftc1lem6  25214  ftc1  25215  ftc2ditglem  25218  itgsubstlem  25221  itgpowd  25223  tdeglem4  25233  tdeglem4OLD  25234  mdegaddle  25248  mdegmullem  25252  ply1rem  25337  fta1glem2  25340  fta1blem  25342  ig1peu  25345  ig1pdvds  25350  dgrmulc  25441  dgrcolem1  25443  plydivlem4  25465  plydiveu  25467  fta1lem  25476  vieta1lem1  25479  vieta1lem2  25480  plyexmo  25482  taylfvallem1  25525  taylfval  25527  tayl0  25530  taylplem1  25531  taylply2  25536  taylply  25537  dvtaylp  25538  dvntaylp  25539  dvntaylp0  25540  taylthlem1  25541  taylthlem2  25542  ulmcaulem  25562  ulmcau  25563  ulmcn  25567  ulmdvlem1  25568  radcnvlem1  25581  radcnvle  25588  psercn  25594  pserdvlem2  25596  pserdv  25597  abelth  25609  tanregt0  25704  dvlog2lem  25816  efopn  25822  logtayllem  25823  logccv  25827  cxplt3  25864  cxpmul2zd  25880  cxpltd  25883  cxpled  25884  cxplt3d  25898  cxple3d  25899  dvsqrt  25904  cxpcn3  25910  cxpaddle  25914  cxpeq  25919  angcan  25961  angvald  25963  ang180lem2  25969  ang180  25973  isosctrlem3  25979  dquartlem1  26010  atantayl2  26097  leibpi  26101  log2tlbnd  26104  birthdaylem3  26112  xrlimcnp  26127  efrlim  26128  o1cxp  26133  jensenlem2  26146  jensen  26147  fsumharmonic  26170  lgamucov  26196  lgamcvg2  26213  wilthlem1  26226  basellem3  26241  basellem6  26244  basellem8  26246  ppisval  26262  chtwordi  26314  ppiwordi  26320  mumullem2  26338  dvdsmulf1o  26352  fsumvma  26370  fsumvma2  26371  chpchtsum  26376  chpub  26377  logfacubnd  26378  dchrmulcl  26406  dchrinv  26418  dchrptlem1  26421  dchrptlem2  26422  sumdchr2  26427  dchr2sum  26430  bposlem7  26447  lgslem1  26454  lgslem3  26456  lgsdirprm  26488  lgsqrlem2  26504  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem4  26535  lgseisen  26536  lgsquadlem1  26537  lgsquad2lem1  26541  lgsquad3  26544  m1lgs  26545  2sqlem7  26581  2sq2  26590  2sqmod  26593  chebbnd1lem2  26627  chebbnd1lem3  26628  rplogsumlem1  26641  rpvmasumlem  26644  dchrvmasumlem1  26652  dchrvmasum2lem  26653  dchrvmasumlema  26657  dchrisum0flblem2  26666  dchrisum0fno1  26668  dchrisum0re  26670  logdivsum  26690  pntrsumbnd2  26724  pntpbnd1a  26742  pntpbnd1  26743  pntibndlem2  26748  pntlemr  26759  pntlemj  26760  pntlemf  26762  pnt2  26770  padicabv  26787  ostth2lem2  26791  f1otrg  27241  brbtwn2  27282  colinearalglem2  27284  axcgrtr  27292  axcgrid  27293  axsegconlem7  27300  axsegcon  27304  ax5seglem3  27308  ax5seglem6  27311  ax5seg  27315  axpaschlem  27317  axlowdimlem17  27335  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  axcontlem8  27348  ecgrtg  27360  usgredg2v  27603  vtxdgoddnumeven  27929  2trlond  28313  eupthp1  28589  nmobndi  29146  ubthlem2  29242  ubthlem3  29243  minvecolem2  29246  shuni  29671  pjhthlem1  29762  chscllem2  30009  pjcompi  30043  mayete3i  30099  unoplin  30291  hmoplin  30313  nmophmi  30402  mdslmd4i  30704  isoun  31043  xrge0addcld  31094  xrofsup  31099  eliccelico  31107  elicoelioo  31108  difioo  31112  rexdiv  31209  mgcmnt1d  31284  mgcmnt2d  31285  xrge0addgt0  31309  omndadd2d  31343  omndadd2rd  31344  omndmul2  31347  cycpmcl  31392  cycpm2tr  31395  cyc3evpm  31426  cycpmconjslem2  31431  freshmansdream  31493  ofldchr  31522  qusker  31558  eqgvscpbl  31559  ringlsmss1  31593  ringlsmss2  31594  intlidl  31611  rhmpreimaidl  31612  elrspunidl  31615  idlinsubrg  31617  isprmidlc  31632  rhmpreimaprmidl  31636  qsidomlem1  31637  mxidlprm  31649  ssmxidllem  31650  lindsunlem  31714  finexttrb  31746  mdetpmtr2  31783  mdetpmtr12  31784  madjusmdetlem1  31786  madjusmdetlem4  31789  rhmpreimacn  31844  unitdivcld  31860  xrge0mulc1cn  31900  qqhnm  31949  esumcst  32040  esumfsup  32047  esumpmono  32056  esumcvg  32063  difelsiga  32110  sigapisys  32132  sigapildsys  32139  ldgenpisyslem1  32140  1stmbfm  32236  2ndmbfm  32237  dya2icoseg  32253  sibfinima  32315  probmeasb  32406  orvcgteel  32443  orvclteel  32448  ballotlemsima  32491  ballotlemfrceq  32504  sgnmul  32518  ccatmulgnn0dir  32530  fct2relem  32586  ftc2re  32587  chtvalz  32618  subfacp1lem2a  33151  subfaclim  33159  erdsze2lem2  33175  cvmliftlem2  33257  cvmliftlem10  33265  cvmliftlem13  33267  cvmliftiota  33272  cvmlift2lem9  33282  cvmlift2lem11  33284  cvmlift2lem12  33285  cvmliftphtlem  33288  cvmlift3lem6  33295  cvmlift3lem7  33296  cvmlift3lem9  33298  snmlff  33300  mrsubfval  33479  wzel  33827  wsuclem  33828  sltrec  34023  madebday  34089  sltn0  34094  brsegle  34419  opnregcld  34528  fin2so  35773  poimirlem17  35803  poimirlem23  35809  opnmbllem0  35822  mblfinlem3  35825  mblfinlem4  35826  itg2addnclem  35837  itg2addnc  35840  itg2gt0cn  35841  ftc1cnnclem  35857  ftc1cnnc  35858  areacirclem5  35878  indexdom  35901  sstotbnd2  35941  isbnd3  35951  isbnd3b  35952  cntotbnd  35963  ismtyima  35970  heibor1lem  35976  heiborlem8  35985  rrncmslem  35999  reheibor  36006  lkrlsp  37123  lshpkrlem5  37135  ldualssvscl  37179  ldualssvsubcl  37180  llnmlplnN  37560  llncvrlpln  37579  pmapjat1  37874  pclfinN  37921  lautlt  38112  lauteq  38116  lautco  38118  ltrn11  38147  ltrnle  38150  ltrneq2  38169  cdlemednuN  38321  cdleme20k  38340  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme21c  38348  cdleme22e  38365  cdleme22eALTN  38366  cdlemefrs32fva  38421  cdlemg4g  38637  cdlemg18b  38700  cdlemg18c  38701  cdlemj3  38844  dia2dimlem5  39089  dvhopN  39137  cdlemm10N  39139  dihjatcclem4  39442  dochexmidlem2  39482  lclkrlem2o  39542  lcfrlem5  39567  lcfrlem6  39568  lcdlssvscl  39627  mapdpglem6  39699  mapdpglem9  39701  mapdpglem12  39704  mapdpglem14  39706  mapdindp0  39740  hdmaprnlem7N  39876  hdmaprnlem8N  39877  hdmaprnlem3eN  39879  hgmapvvlem3  39946  evlsaddval  40284  evlsmulval  40285  addinvcom  40420  mzpsubst  40577  eldioph2lem1  40589  eldioph2lem2  40590  eldioph2b  40592  diophin  40601  irrapxlem2  40652  irrapxlem4  40654  irrapxlem5  40655  pellexlem1  40658  pellexlem2  40659  pellexlem6  40663  elpell1qr2  40701  pell1qrgaplem  40702  pell1qrgap  40703  pellqrex  40708  pellfundex  40715  pellfund14  40727  rmspecsqrtnq  40735  rmxyadd  40750  congsub  40799  mzpcong  40801  congrep  40802  acongtr  40807  acongrep  40809  jm2.19lem1  40818  jm2.22  40824  jm2.23  40825  jm2.26lem3  40830  jm2.26  40831  jm2.27a  40834  fnwe2lem2  40883  aomclem6  40891  hbtlem2  40956  hbtlem4  40958  hbtlem5  40960  dgraa0p  40981  rngunsnply  41005  proot1hash  41032  expgrowth  41960  fpmd  42818  abslt2sqd  42906  ioondisj2  43038  ioondisj1  43039  eliocre  43054  ioossioobi  43062  iooiinicc  43087  iooiinioc  43101  icossico2  43109  lptioo2  43179  limcresiooub  43190  limsupequzlem  43270  xlimmnfvlem2  43381  xlimpnfvlem2  43385  cncfuni  43434  cncfiooicclem1  43441  cxpcncf2  43447  dvcnre  43464  dvresntr  43466  dvresioo  43469  dvbdfbdioolem1  43476  dvnmptdivc  43486  dvnxpaek  43490  itgsinexplem1  43502  itgcoscmulx  43517  itgiccshift  43528  itgperiod  43529  ovolsplit  43536  stoweidlem11  43559  stoweidlem26  43574  stoweidlem34  43582  stoweidlem36  43584  stoweidlem38  43586  stirlinglem5  43626  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem20  43675  fourierdlem58  43712  fourierdlem72  43726  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem79  43733  fourierdlem80  43734  fourierdlem87  43741  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem113  43767  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  etransclem46  43828  etransclem47  43829  rrndistlt  43838  rrnprjdstle  43849  ioorrnopnxrlem  43854  sge0ssre  43942  sge0seq  43991  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidifhspdmvle  44165  hoiqssbllem2  44168  ovolval5lem2  44198  iinhoiicc  44219  iunhoiioo  44221  vonioolem2  44226  vonicclem2  44229  issmflem  44272  iccpartdisj  44900  m1expevenALTV  45110  fpprel2  45204  tgoldbach  45280  strisomgrop  45303  nn0eo  45885  fdivpm  45900  refdivpm  45901  elbigolo1  45914  logbpw2m1  45924  fllog2  45925  dignn0flhalflem1  45972  dignn0flhalflem2  45973  itsclinecirc0in  46132  2itscplem2  46136  itscnhlinecirc02plem1  46139  iccdisj2  46202