Theorem syl22anc 839

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  preqsnd  4769  fr2nr  5529  soltmin  6001  f1oprg  6705  f1prex  7094  fveqf1o  7113  weniso  7163  fr3nr  7557  suppofssd  7945  smogt  8104  smorndom  8105  oacomf1o  8293  enpr2d  8725  difsnen  8727  undom  8733  enfixsn  8754  domss2  8805  ssenen  8820  marypha1lem  9049  fisupcl  9085  ordtypelem3  9136  ordtypelem8  9141  oieu  9155  oismo  9156  wofib  9161  wemaplem2  9163  wemapso  9167  wemapso2lem  9168  unxpwdom2  9204  infdifsn  9272  oemapvali  9299  cantnflem1c  9302  cantnflem1  9304  cantnf  9308  cnfcom3  9319  trpredelss  9338  trpredpo  9341  r1ordg  9394  dif1card  9624  infxpenlem  9627  dfac8clem  9646  infxp  9829  infmap2  9832  cflim2  9877  coftr  9887  fin2i2  9932  enfin2i  9935  fin23lem26  9939  fin23lem27  9942  fin23lem40  9965  isf32lem2  9968  isf32lem3  9969  isf32lem4  9970  isf32lem7  9973  isf32lem9  9975  fin1a2lem13  10026  fin12  10027  alephexp1  10193  gchdomtri  10243  fpwwe2lem11  10255  fpwwe2lem12  10256  gchpwdom  10284  gchhar  10293  adderpqlem  10568  mulerpqlem  10569  addassnq  10572  mulassnq  10573  distrnq  10575  mulidnq  10577  recmulnq  10578  ltexnq  10589  distrlem1pr  10639  distrlem4pr  10640  prlem936  10661  reclem3pr  10663  mulcmpblnr  10685  mulgt0d  10987  mul4d  11044  add4d  11060  add42d  11061  subcan  11133  addsub4d  11236  subadd4d  11237  sub4d  11238  2addsubd  11239  addsubeq4d  11240  muladdd  11290  mulsubd  11291  addgegt0d  11405  addgtge0d  11406  addge0d  11408  mulge0d  11409  le2addd  11451  le2subd  11452  ltleaddd  11453  leltaddd  11454  lt2subd  11456  divdivdiv  11533  divcan5  11534  divne0d  11624  recdivd  11625  recdiv2d  11626  divcan6d  11627  ddcand  11628  rec11d  11629  divmuldivd  11649  divmul13d  11650  divmul24d  11651  divadddivd  11652  divsubdivd  11653  divmuleqd  11654  divdivdivd  11655  subrecd  11663  mulge0b  11702  recreclt  11731  divgt0d  11767  mulgt1d  11768  lemulge11d  11769  lemulge12d  11770  ltmul12ad  11773  lemul12ad  11774  lemul12bd  11775  supmul1  11801  nndivtr  11877  qreccl  12565  ledivdivd  12653  lediv12ad  12687  lt2mul2divd  12697  xlt2add  12850  supxrun  12906  supxrre  12917  infxrre  12926  elicore  12987  iccss2  13006  iccssico2  13009  lincmb01cmp  13083  iccf1o  13084  fzrev2i  13177  2tnp1ge0ge0  13404  m1modnnsub1  13490  modaddmodup  13507  modaddmodlo  13508  modsubdir  13513  fzennn  13541  sermono  13608  mulexpz  13675  expaddz  13679  sqdiv  13693  expsubd  13727  ltexp2a  13736  expmordi  13737  leexp2a  13742  expmulnbnd  13802  digit1  13804  lt2sqd  13825  le2sqd  13826  sq11d  13827  bcm1k  13881  bcp1n  13882  bcp1nk  13883  hashf1lem1  14020  hashf1lem1OLD  14021  cshw1  14387  2swrd2eqwrdeq  14518  ofccat  14532  absrele  14872  sqreulem  14923  sqrtmuld  14988  sqrtsq2d  14989  sqrtled  14990  sqrtltd  14991  sqr11d  14992  abs3lemd  15025  rlimuni  15111  climuni  15113  lo1resb  15125  o1resb  15127  2clim  15133  addcn2  15155  mulcn2  15157  o1of2  15174  o1rlimmul  15180  lo1add  15188  lo1mul  15189  isercolllem1  15228  caucvgrlem  15236  iseraltlem2  15246  iseraltlem3  15247  mptfzshft  15342  fsumrev  15343  fsum0diag2  15347  binomlem  15393  climcndslem1  15413  climcndslem2  15414  harmonic  15423  mertenslem1  15448  fprodser  15511  fprodrev  15539  efcllem  15639  moddvds  15826  dvds1  15880  dvdsext  15882  evennn2n  15912  bitsinv1  16001  sadaddlem  16025  sadasslem  16029  sadeq  16031  mulgcd  16108  dvdssqlem  16123  lcmftp  16193  rpmulgcd2  16213  coprmproddvdslem  16219  isprm5  16264  isprm6  16271  crth  16331  eulerthlem2  16335  prmdiveq  16339  pythagtriplem11  16378  pythagtriplem13  16380  pcgcd1  16430  pcprmpw2  16435  pcaddlem  16441  fldivp1  16450  4sqlem12  16509  4sqlem14  16511  4sqlem15  16512  4sqlem16  16513  vdwapun  16527  mreexexlem4d  17150  acsfn1  17164  acsfn2  17166  sscpwex  17320  rescabs  17339  yonedainv  17789  subm0  18242  pmtrfb  18857  psgnunilem1  18885  odmodnn0  18932  odeq  18942  dfod2  18955  sylow1lem1  18987  lsmsubg  19043  lsmmod  19065  lsmdisj2  19072  ghmplusg  19231  odadd  19235  gexexlem  19237  lt6abl  19280  cyggex2  19282  dprdfinv  19406  dmdprdsplitlem  19424  dpjidcl  19445  ablfacrp  19453  ablfacrp2  19454  ablfac1c  19458  ablfac1eu  19460  acsfn1p  19843  lcomfsupp  19939  lssvancl1  19981  lssvnegcl  19993  lspprvacl  20036  lspsneli  20038  lspsn  20039  lmhmplusg  20081  lmhmima  20084  lmhmpreima  20085  reslmhm  20089  lbsind2  20118  lsmcl  20120  lsmelval2  20122  lsppreli  20127  lspprabs  20132  pj1lmhm  20137  lssvs0or  20147  lspabs3  20158  lspfixed  20165  lspexch  20166  lsmcv  20178  lspsolv  20180  lidlmcl  20255  drngnidl  20267  2idlcpbl  20272  gzrngunit  20429  zringlpirlem3  20451  prmirredlem  20459  znf1o  20516  znunithash  20529  frlmsubgval  20727  frlmvplusgvalc  20729  frlmvscaval  20730  frlmphllem  20742  frlmphl  20743  frlmssuvc1  20756  frlmsslsp  20758  frlmup1  20760  frlmup2  20761  lindfind2  20780  lindfrn  20783  f1lindf  20784  islindf4  20800  mplbas2  20999  evlslem3  21040  evlslem1  21042  coe1addfv  21186  lply1binom  21227  evl1addd  21257  evl1subd  21258  evl1muld  21259  mamudi  21300  mamudir  21301  1marepvmarrepid  21472  mdetrlin  21499  smadiadetglem1  21568  smadiadetg  21570  cramerimplem1  21580  mat2pmatscmxcl  21637  m2pmfzgsumcl  21645  pmatcollpw  21678  pmatcollpwfi  21679  pmatcollpw3fi1lem1  21683  cpmidpmatlem2  21768  cpmadugsumlemF  21773  chcoeffeqlem  21782  ntrin  21958  topssnei  22021  restbas  22055  restntr  22079  cnntri  22168  fiuncmp  22301  nllyrest  22383  nllyidm  22386  hausllycmp  22391  cldllycmp  22392  hauspwdom  22398  txcld  22500  txcn  22523  txlly  22533  txnlly  22534  txhaus  22544  txlm  22545  txkgen  22549  xkococnlem  22556  cnmpt2res  22574  xkoinjcn  22584  basqtop  22608  qtopeu  22613  trfbas2  22740  neifil  22777  hausflim  22878  alexsubALTlem2  22945  cnextfval  22959  cnextfvval  22962  cnextf  22963  cnextfres  22966  clssubg  23006  utop2nei  23148  utop3cls  23149  utopreg  23150  psmetlecl  23213  xmetlecl  23244  prdsxmetlem  23266  bldisj  23296  imasf1obl  23386  prdsbl  23389  stdbdmet  23414  stdbdmopn  23416  met2ndci  23420  metcnp  23439  metustto  23451  metustexhalf  23454  cfilucfil  23457  metucn  23469  lssnlm  23599  nmotri  23637  nmoid  23640  tgioo  23693  blcvx  23695  xrsmopn  23709  reperflem  23715  reconnlem2  23724  opnreen  23728  metdsge  23746  metdsre  23750  metdscnlem  23752  metnrmlem1a  23755  metnrmlem1  23756  metnrmlem3  23758  cncfmet  23806  cnmpopc  23825  icopnfcnv  23839  icopnfhmeo  23840  cnllycmp  23853  evth  23856  lebnumii  23863  nmoleub2lem3  24012  iscfil2  24163  cfil3i  24166  iscfil3  24170  cfilfcls  24171  iscau3  24175  iscmet3lem2  24189  caubl  24205  lmcau  24210  cssbn  24272  rrxcph  24289  minveclem2  24323  pjthlem1  24334  pjthlem2  24335  ivthicc  24355  ovollecl  24380  ovolunlem1a  24393  ovolunnul  24397  ovoliunlem1  24399  ismbl2  24424  nulmbl2  24433  unmbl  24434  volun  24442  voliunlem2  24448  ioombl1lem2  24456  uniioombllem2a  24479  uniioombllem3  24482  uniioombllem4  24483  dyaddisjlem  24492  dyadmaxlem  24494  opnmbllem  24498  volsup2  24502  volcn  24503  ismbfd  24536  mbfi1fseqlem1  24613  mbfi1fseqlem5  24617  itg2lecl  24636  itg2monolem2  24649  itg2gt0  24658  itgspliticc  24734  ellimc3  24776  limcres  24783  dvfval  24794  dvres3  24810  dvres3a  24811  dvmptresicc  24813  dvnff  24820  dvnadd  24826  dvn2bss  24827  dvnres  24828  dvcmul  24841  dvcmulf  24842  dvmptres3  24853  dvmptres2  24859  dvmptntr  24868  dvexp3  24875  dvferm1lem  24881  dvlip  24890  dvlipcn  24891  dvlip2  24892  c1liplem1  24893  dvgt0lem1  24899  dvgt0lem2  24900  dvne0  24908  lhop1lem  24910  lhop2  24912  lhop  24913  dvcnvrelem1  24914  dvcnvrelem2  24915  dvcvx  24917  dvfsumle  24918  dvfsumabs  24920  dvfsumlem2  24924  ftc1lem6  24938  ftc1  24939  ftc2ditglem  24942  itgsubstlem  24945  itgpowd  24947  tdeglem4  24957  tdeglem4OLD  24958  mdegaddle  24972  mdegmullem  24976  ply1rem  25061  fta1glem2  25064  fta1blem  25066  ig1peu  25069  ig1pdvds  25074  dgrmulc  25165  dgrcolem1  25167  plydivlem4  25189  plydiveu  25191  fta1lem  25200  vieta1lem1  25203  vieta1lem2  25204  plyexmo  25206  taylfvallem1  25249  taylfval  25251  tayl0  25254  taylplem1  25255  taylply2  25260  taylply  25261  dvtaylp  25262  dvntaylp  25263  dvntaylp0  25264  taylthlem1  25265  taylthlem2  25266  ulmcaulem  25286  ulmcau  25287  ulmcn  25291  ulmdvlem1  25292  radcnvlem1  25305  radcnvle  25312  psercn  25318  pserdvlem2  25320  pserdv  25321  abelth  25333  tanregt0  25428  dvlog2lem  25540  efopn  25546  logtayllem  25547  logccv  25551  cxplt3  25588  cxpmul2zd  25604  cxpltd  25607  cxpled  25608  cxplt3d  25622  cxple3d  25623  dvsqrt  25628  cxpcn3  25634  cxpaddle  25638  cxpeq  25643  angcan  25685  angvald  25687  ang180lem2  25693  ang180  25697  isosctrlem3  25703  dquartlem1  25734  atantayl2  25821  leibpi  25825  log2tlbnd  25828  birthdaylem3  25836  xrlimcnp  25851  efrlim  25852  o1cxp  25857  jensenlem2  25870  jensen  25871  fsumharmonic  25894  lgamucov  25920  lgamcvg2  25937  wilthlem1  25950  basellem3  25965  basellem6  25968  basellem8  25970  ppisval  25986  chtwordi  26038  ppiwordi  26044  mumullem2  26062  dvdsmulf1o  26076  fsumvma  26094  fsumvma2  26095  chpchtsum  26100  chpub  26101  logfacubnd  26102  dchrmulcl  26130  dchrinv  26142  dchrptlem1  26145  dchrptlem2  26146  sumdchr2  26151  dchr2sum  26154  bposlem7  26171  lgslem1  26178  lgslem3  26180  lgsdirprm  26212  lgsqrlem2  26228  lgseisenlem1  26256  lgseisenlem2  26257  lgseisenlem4  26259  lgseisen  26260  lgsquadlem1  26261  lgsquad2lem1  26265  lgsquad3  26268  m1lgs  26269  2sqlem7  26305  2sq2  26314  2sqmod  26317  chebbnd1lem2  26351  chebbnd1lem3  26352  rplogsumlem1  26365  rpvmasumlem  26368  dchrvmasumlem1  26376  dchrvmasum2lem  26377  dchrvmasumlema  26381  dchrisum0flblem2  26390  dchrisum0fno1  26392  dchrisum0re  26394  logdivsum  26414  pntrsumbnd2  26448  pntpbnd1a  26466  pntpbnd1  26467  pntibndlem2  26472  pntlemr  26483  pntlemj  26484  pntlemf  26486  pnt2  26494  padicabv  26511  ostth2lem2  26515  f1otrg  26962  brbtwn2  26996  colinearalglem2  26998  axcgrtr  27006  axcgrid  27007  axsegconlem7  27014  axsegcon  27018  ax5seglem3  27022  ax5seglem6  27025  ax5seg  27029  axpaschlem  27031  axlowdimlem17  27049  axcontlem2  27056  axcontlem4  27058  axcontlem7  27061  axcontlem8  27062  ecgrtg  27074  usgredg2v  27315  vtxdgoddnumeven  27641  2trlond  28023  eupthp1  28299  nmobndi  28856  ubthlem2  28952  ubthlem3  28953  minvecolem2  28956  shuni  29381  pjhthlem1  29472  chscllem2  29719  pjcompi  29753  mayete3i  29809  unoplin  30001  hmoplin  30023  nmophmi  30112  mdslmd4i  30414  isoun  30754  xrge0addcld  30805  xrofsup  30810  eliccelico  30818  elicoelioo  30819  difioo  30823  rexdiv  30920  mgcmnt1d  30994  mgcmnt2d  30995  xrge0addgt0  31019  omndadd2d  31053  omndadd2rd  31054  omndmul2  31057  cycpmcl  31102  cycpm2tr  31105  cyc3evpm  31136  cycpmconjslem2  31141  freshmansdream  31203  ofldchr  31232  qusker  31263  eqgvscpbl  31264  ringlsmss1  31298  ringlsmss2  31299  intlidl  31316  rhmpreimaidl  31317  elrspunidl  31320  idlinsubrg  31322  isprmidlc  31337  rhmpreimaprmidl  31341  qsidomlem1  31342  mxidlprm  31354  ssmxidllem  31355  lindsunlem  31419  finexttrb  31451  mdetpmtr2  31488  mdetpmtr12  31489  madjusmdetlem1  31491  madjusmdetlem4  31494  rhmpreimacn  31549  unitdivcld  31565  xrge0mulc1cn  31605  qqhnm  31652  esumcst  31743  esumfsup  31750  esumpmono  31759  esumcvg  31766  difelsiga  31813  sigapisys  31835  sigapildsys  31842  ldgenpisyslem1  31843  1stmbfm  31939  2ndmbfm  31940  dya2icoseg  31956  sibfinima  32018  probmeasb  32109  orvcgteel  32146  orvclteel  32151  ballotlemsima  32194  ballotlemfrceq  32207  sgnmul  32221  ccatmulgnn0dir  32233  fct2relem  32289  ftc2re  32290  chtvalz  32321  subfacp1lem2a  32855  subfaclim  32863  erdsze2lem2  32879  cvmliftlem2  32961  cvmliftlem10  32969  cvmliftlem13  32971  cvmliftiota  32976  cvmlift2lem9  32986  cvmlift2lem11  32988  cvmlift2lem12  32989  cvmliftphtlem  32992  cvmlift3lem6  32999  cvmlift3lem7  33000  cvmlift3lem9  33002  snmlff  33004  mrsubfval  33183  wzel  33555  wsuclem  33556  sltrec  33751  madebday  33817  sltn0  33822  brsegle  34147  opnregcld  34256  fin2so  35501  poimirlem17  35531  poimirlem23  35537  opnmbllem0  35550  mblfinlem3  35553  mblfinlem4  35554  itg2addnclem  35565  itg2addnc  35568  itg2gt0cn  35569  ftc1cnnclem  35585  ftc1cnnc  35586  areacirclem5  35606  indexdom  35629  sstotbnd2  35669  isbnd3  35679  isbnd3b  35680  cntotbnd  35691  ismtyima  35698  heibor1lem  35704  heiborlem8  35713  rrncmslem  35727  reheibor  35734  lkrlsp  36853  lshpkrlem5  36865  ldualssvscl  36909  ldualssvsubcl  36910  llnmlplnN  37290  llncvrlpln  37309  pmapjat1  37604  pclfinN  37651  lautlt  37842  lauteq  37846  lautco  37848  ltrn11  37877  ltrnle  37880  ltrneq2  37899  cdlemednuN  38051  cdleme20k  38070  cdleme20l2  38072  cdleme20l  38073  cdleme20m  38074  cdleme21c  38078  cdleme22e  38095  cdleme22eALTN  38096  cdlemefrs32fva  38151  cdlemg4g  38367  cdlemg18b  38430  cdlemg18c  38431  cdlemj3  38574  dia2dimlem5  38819  dvhopN  38867  cdlemm10N  38869  dihjatcclem4  39172  dochexmidlem2  39212  lclkrlem2o  39272  lcfrlem5  39297  lcfrlem6  39298  lcdlssvscl  39357  mapdpglem6  39429  mapdpglem9  39431  mapdpglem12  39434  mapdpglem14  39436  mapdindp0  39470  hdmaprnlem7N  39606  hdmaprnlem8N  39607  hdmaprnlem3eN  39609  hgmapvvlem3  39676  evlsaddval  39987  evlsmulval  39988  addinvcom  40121  mzpsubst  40273  eldioph2lem1  40285  eldioph2lem2  40286  eldioph2b  40288  diophin  40297  irrapxlem2  40348  irrapxlem4  40350  irrapxlem5  40351  pellexlem1  40354  pellexlem2  40355  pellexlem6  40359  elpell1qr2  40397  pell1qrgaplem  40398  pell1qrgap  40399  pellqrex  40404  pellfundex  40411  pellfund14  40423  rmspecsqrtnq  40431  rmxyadd  40446  congsub  40495  mzpcong  40497  congrep  40498  acongtr  40503  acongrep  40505  jm2.19lem1  40514  jm2.22  40520  jm2.23  40521  jm2.26lem3  40526  jm2.26  40527  jm2.27a  40530  fnwe2lem2  40579  aomclem6  40587  hbtlem2  40652  hbtlem4  40654  hbtlem5  40656  dgraa0p  40677  rngunsnply  40701  proot1hash  40728  expgrowth  41626  fpmd  42483  abslt2sqd  42572  ioondisj2  42706  ioondisj1  42707  eliocre  42722  ioossioobi  42730  iooiinicc  42755  iooiinioc  42769  icossico2  42777  lptioo2  42847  limcresiooub  42858  limsupequzlem  42938  xlimmnfvlem2  43049  xlimpnfvlem2  43053  cncfuni  43102  cncfiooicclem1  43109  cxpcncf2  43115  dvcnre  43132  dvresntr  43134  dvresioo  43137  dvbdfbdioolem1  43144  dvnmptdivc  43154  dvnxpaek  43158  itgsinexplem1  43170  itgcoscmulx  43185  itgiccshift  43196  itgperiod  43197  ovolsplit  43204  stoweidlem11  43227  stoweidlem26  43242  stoweidlem34  43250  stoweidlem36  43252  stoweidlem38  43254  stirlinglem5  43294  dirkercncflem2  43320  dirkercncflem4  43322  fourierdlem20  43343  fourierdlem58  43380  fourierdlem72  43394  fourierdlem73  43395  fourierdlem74  43396  fourierdlem75  43397  fourierdlem76  43398  fourierdlem79  43401  fourierdlem80  43402  fourierdlem87  43409  fourierdlem94  43416  fourierdlem103  43425  fourierdlem104  43426  fourierdlem107  43429  fourierdlem113  43435  sqwvfoura  43444  sqwvfourb  43445  fourierswlem  43446  fouriersw  43447  etransclem46  43496  etransclem47  43497  rrndistlt  43506  rrnprjdstle  43517  ioorrnopnxrlem  43522  sge0ssre  43610  sge0seq  43659  hsphoidmvle2  43798  hsphoidmvle  43799  hoidmv1lelem1  43804  hoidmv1lelem2  43805  hoidmv1lelem3  43806  hoidmvlelem1  43808  hoidifhspdmvle  43833  hoiqssbllem2  43836  ovolval5lem2  43866  iinhoiicc  43887  iunhoiioo  43889  vonioolem2  43894  vonicclem2  43897  issmflem  43935  iccpartdisj  44562  m1expevenALTV  44772  fpprel2  44866  tgoldbach  44942  strisomgrop  44965  nn0eo  45547  fdivpm  45562  refdivpm  45563  elbigolo1  45576  logbpw2m1  45586  fllog2  45587  dignn0flhalflem1  45634  dignn0flhalflem2  45635  itsclinecirc0in  45794  2itscplem2  45798  itscnhlinecirc02plem1  45801  iccdisj2  45864