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 511	. 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 395

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 207  df-an 396

This theorem is referenced by:  preqsnd  4863  fr2nr  5665  soltmin  6158  f1oprg  6893  f1prex  7303  fveqf1o  7321  weniso  7373  fr3nr  7790  suppofssd  8226  smogt  8405  smocdmdom  8406  oacomf1o  8601  en2prd  9086  enpr2dOLD  9088  difsnen  9091  undomOLD  9098  enfixsn  9119  domss2  9174  ssenen  9189  marypha1lem  9470  fisupcl  9506  ordtypelem3  9557  ordtypelem8  9562  oieu  9576  oismo  9577  wofib  9582  wemaplem2  9584  wemapso  9588  wemapso2lem  9589  unxpwdom2  9625  infdifsn  9694  oemapvali  9721  cantnflem1c  9724  cantnflem1  9726  cantnf  9730  cnfcom3  9741  r1ordg  9815  dif1card  10047  infxpenlem  10050  dfac8clem  10069  infxp  10251  infmap2  10254  cflim2  10300  coftr  10310  fin2i2  10355  enfin2i  10358  fin23lem26  10362  fin23lem27  10365  fin23lem40  10388  isf32lem2  10391  isf32lem3  10392  isf32lem4  10393  isf32lem7  10396  isf32lem9  10398  fin1a2lem13  10449  fin12  10450  alephexp1  10616  gchdomtri  10666  fpwwe2lem11  10678  fpwwe2lem12  10679  gchpwdom  10707  gchhar  10716  adderpqlem  10991  mulerpqlem  10992  addassnq  10995  mulassnq  10996  distrnq  10998  mulidnq  11000  recmulnq  11001  ltexnq  11012  distrlem1pr  11062  distrlem4pr  11063  prlem936  11084  reclem3pr  11086  mulcmpblnr  11108  mulgt0d  11413  mul4d  11470  add4d  11487  add42d  11488  subcan  11561  addsub4d  11664  subadd4d  11665  sub4d  11666  2addsubd  11667  addsubeq4d  11668  muladdd  11718  mulsubd  11719  addgegt0d  11833  addgtge0d  11834  addge0d  11836  mulge0d  11837  le2addd  11879  le2subd  11880  ltleaddd  11881  leltaddd  11882  lt2subd  11884  divdivdiv  11965  divcan5  11966  divne0d  12056  recdivd  12057  recdiv2d  12058  divcan6d  12059  ddcand  12060  rec11d  12061  divmuldivd  12081  divmul13d  12082  divmul24d  12083  divadddivd  12084  divsubdivd  12085  divmuleqd  12086  divdivdivd  12087  subrecd  12095  mulge0b  12135  recreclt  12164  divgt0d  12200  mulgt1d  12201  lemulge11d  12202  lemulge12d  12203  ltmul12ad  12206  lemul12ad  12207  lemul12bd  12208  supmul1  12234  nndivtr  12310  qreccl  13008  ledivdivd  13099  lediv12ad  13133  lt2mul2divd  13143  xlt2add  13298  supxrun  13354  supxrre  13365  infxrre  13374  elicore  13435  iccss2  13454  iccssico2  13457  lincmb01cmp  13531  iccf1o  13532  fzrev2i  13625  2tnp1ge0ge0  13865  m1modnnsub1  13954  modaddmodup  13971  modaddmodlo  13972  modsubdir  13977  fzennn  14005  sermono  14071  mulexpz  14139  expaddz  14143  sqdiv  14157  expsubd  14193  ltexp2a  14202  expmordi  14203  leexp2a  14208  expmulnbnd  14270  digit1  14272  lt2sqd  14291  le2sqd  14292  sq11d  14293  bcm1k  14350  bcp1n  14351  bcp1nk  14352  hashf1lem1  14490  cshw1  14856  2swrd2eqwrdeq  14988  ofccat  15004  absrele  15343  sqreulem  15394  sqrtmuld  15459  sqrtsq2d  15460  sqrtled  15461  sqrtltd  15462  sqr11d  15463  abs3lemd  15496  rlimuni  15582  climuni  15584  lo1resb  15596  o1resb  15598  2clim  15604  addcn2  15626  mulcn2  15628  o1of2  15645  o1rlimmul  15651  lo1add  15659  lo1mul  15660  isercolllem1  15697  caucvgrlem  15705  iseraltlem2  15715  iseraltlem3  15716  mptfzshft  15810  fsumrev  15811  fsum0diag2  15815  binomlem  15861  climcndslem1  15881  climcndslem2  15882  harmonic  15891  mertenslem1  15916  fprodser  15981  fprodrev  16009  efcllem  16109  moddvds  16297  dvds1  16352  dvdsext  16354  evennn2n  16384  bitsinv1  16475  sadaddlem  16499  sadasslem  16503  sadeq  16505  mulgcd  16581  dvdssqlem  16599  lcmftp  16669  rpmulgcd2  16689  coprmproddvdslem  16695  isprm5  16740  isprm6  16747  crth  16811  eulerthlem2  16815  prmdiveq  16819  pythagtriplem11  16858  pythagtriplem13  16860  pcgcd1  16910  pcprmpw2  16915  pcaddlem  16921  fldivp1  16930  4sqlem12  16989  4sqlem14  16991  4sqlem15  16992  4sqlem16  16993  vdwapun  17007  mreexexlem4d  17691  acsfn1  17705  acsfn2  17707  sscpwex  17862  rescabs  17882  rescabsOLD  17883  yonedainv  18337  subm0  18840  pmtrfb  19497  psgnunilem1  19525  odmodnn0  19572  odeq  19582  dfod2  19596  sylow1lem1  19630  lsmsubg  19686  lsmmod  19707  lsmdisj2  19714  ghmplusg  19878  odadd  19882  gexexlem  19884  lt6abl  19927  cyggex2  19929  dprdfinv  20053  dmdprdsplitlem  20071  dpjidcl  20092  ablfacrp  20100  ablfacrp2  20101  ablfac1c  20105  ablfac1eu  20107  acsfn1p  20816  lcomfsupp  20916  lssvancl1  20960  lssvnegcl  20971  lspprvacl  21014  ellspsni  21016  lspsn  21017  lmhmplusg  21060  lmhmima  21063  lmhmpreima  21064  reslmhm  21068  lbsind2  21097  lsmcl  21099  lsmelval2  21101  lsppreli  21106  lspprabs  21111  pj1lmhm  21116  lssvs0or  21129  lspabs3  21140  lspfixed  21147  lspexch  21148  lsmcv  21160  lspsolv  21162  drngnidl  21270  rhmpreimaidl  21304  rngqiprngimfo  21328  rngqiprngfulem4  21341  gzrngunit  21468  zringlpirlem3  21492  prmirredlem  21500  znf1o  21587  znunithash  21600  freshmansdream  21610  frlmsubgval  21802  frlmvplusgvalc  21804  frlmvscaval  21805  frlmphllem  21817  frlmphl  21818  frlmssuvc1  21831  frlmsslsp  21833  frlmup1  21835  frlmup2  21836  lindfind2  21855  lindfrn  21858  f1lindf  21859  islindf4  21875  mplbas2  22077  evlslem3  22121  evlslem1  22123  coe1addfv  22283  lply1binom  22329  evl1addd  22360  evl1subd  22361  evl1muld  22362  mamudi  22422  mamudir  22423  1marepvmarrepid  22596  mdetrlin  22623  smadiadetglem1  22692  smadiadetg  22694  cramerimplem1  22704  mat2pmatscmxcl  22761  m2pmfzgsumcl  22769  pmatcollpw  22802  pmatcollpwfi  22803  pmatcollpw3fi1lem1  22807  cpmidpmatlem2  22892  cpmadugsumlemF  22897  chcoeffeqlem  22906  ntrin  23084  topssnei  23147  restbas  23181  restntr  23205  cnntri  23294  fiuncmp  23427  nllyrest  23509  nllyidm  23512  hausllycmp  23517  cldllycmp  23518  hauspwdom  23524  txcld  23626  txcn  23649  txlly  23659  txnlly  23660  txhaus  23670  txlm  23671  txkgen  23675  xkococnlem  23682  cnmpt2res  23700  xkoinjcn  23710  basqtop  23734  qtopeu  23739  trfbas2  23866  neifil  23903  hausflim  24004  alexsubALTlem2  24071  cnextfval  24085  cnextfvval  24088  cnextf  24089  cnextfres  24092  clssubg  24132  utop2nei  24274  utop3cls  24275  utopreg  24276  psmetlecl  24340  xmetlecl  24371  prdsxmetlem  24393  bldisj  24423  imasf1obl  24516  prdsbl  24519  stdbdmet  24544  stdbdmopn  24546  met2ndci  24550  metcnp  24569  metustto  24581  metustexhalf  24584  cfilucfil  24587  metucn  24599  lssnlm  24737  nmotri  24775  nmoid  24778  tgioo  24831  blcvx  24833  xrsmopn  24847  reperflem  24853  reconnlem2  24862  opnreen  24866  metdsge  24884  metdsre  24888  metdscnlem  24890  metnrmlem1a  24893  metnrmlem1  24894  metnrmlem3  24896  cncfmet  24948  cnmpopc  24968  icopnfcnv  24986  icopnfhmeo  24987  cnllycmp  25001  evth  25004  lebnumii  25011  nmoleub2lem3  25161  iscfil2  25313  cfil3i  25316  iscfil3  25320  cfilfcls  25321  iscau3  25325  iscmet3lem2  25339  caubl  25355  lmcau  25360  cssbn  25422  rrxcph  25439  minveclem2  25473  pjthlem1  25484  pjthlem2  25485  ivthicc  25506  ovollecl  25531  ovolunlem1a  25544  ovolunnul  25548  ovoliunlem1  25550  ismbl2  25575  nulmbl2  25584  unmbl  25585  volun  25593  voliunlem2  25599  ioombl1lem2  25607  uniioombllem2a  25630  uniioombllem3  25633  uniioombllem4  25634  dyaddisjlem  25643  dyadmaxlem  25645  opnmbllem  25649  volsup2  25653  volcn  25654  ismbfd  25687  mbfi1fseqlem1  25764  mbfi1fseqlem5  25768  itg2lecl  25787  itg2monolem2  25800  itg2gt0  25809  itgspliticc  25886  ellimc3  25928  limcres  25935  dvfval  25946  dvres3  25962  dvres3a  25963  dvmptresicc  25965  dvnff  25973  dvnadd  25979  dvn2bss  25980  dvnres  25981  dvcmul  25995  dvcmulf  25996  dvmptres3  26008  dvmptres2  26014  dvmptntr  26023  dvexp3  26030  dvferm1lem  26036  dvlip  26046  dvlipcn  26047  dvlip2  26048  c1liplem1  26049  dvgt0lem1  26055  dvgt0lem2  26056  dvne0  26064  lhop1lem  26066  lhop2  26068  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc1lem6  26096  ftc1  26097  ftc2ditglem  26100  itgsubstlem  26103  itgpowd  26105  tdeglem4  26113  mdegaddle  26127  mdegmullem  26131  ply1rem  26219  fta1glem2  26222  fta1blem  26224  ig1peu  26228  ig1pdvds  26233  dgrmulc  26325  dgrcolem1  26327  plydivlem4  26352  plydiveu  26354  fta1lem  26363  vieta1lem1  26366  vieta1lem2  26367  plyexmo  26369  taylfvallem1  26412  taylfval  26414  tayl0  26417  taylplem1  26418  taylply2  26423  taylply2OLD  26424  taylply  26425  dvtaylp  26426  dvntaylp  26427  dvntaylp0  26428  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmcaulem  26451  ulmcau  26452  ulmcn  26456  ulmdvlem1  26457  radcnvlem1  26470  radcnvle  26477  psercn  26484  pserdvlem2  26486  pserdv  26487  abelth  26499  tanregt0  26595  dvlog2lem  26708  efopn  26714  logtayllem  26715  logccv  26719  cxplt3  26756  cxpmul2zd  26772  cxpltd  26775  cxpled  26776  cxplt3d  26791  cxple3d  26792  dvsqrt  26798  cxpcn3  26805  cxpaddle  26809  cxpeq  26814  angcan  26859  angvald  26861  ang180lem2  26867  ang180  26871  isosctrlem3  26877  dquartlem1  26908  atantayl2  26995  leibpi  26999  log2tlbnd  27002  birthdaylem3  27010  xrlimcnp  27025  efrlim  27026  efrlimOLD  27027  o1cxp  27032  jensenlem2  27045  jensen  27046  fsumharmonic  27069  lgamucov  27095  lgamcvg2  27112  wilthlem1  27125  basellem3  27140  basellem6  27143  basellem8  27145  ppisval  27161  chtwordi  27213  ppiwordi  27219  mumullem2  27237  mpodvdsmulf1o  27251  dvdsmulf1o  27253  fsumvma  27271  fsumvma2  27272  chpchtsum  27277  chpub  27278  logfacubnd  27279  dchrmulcl  27307  dchrinv  27319  dchrptlem1  27322  dchrptlem2  27323  sumdchr2  27328  dchr2sum  27331  bposlem7  27348  lgslem1  27355  lgslem3  27357  lgsdirprm  27389  lgsqrlem2  27405  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem4  27436  lgseisen  27437  lgsquadlem1  27438  lgsquad2lem1  27442  lgsquad3  27445  m1lgs  27446  2sqlem7  27482  2sq2  27491  2sqmod  27494  chebbnd1lem2  27528  chebbnd1lem3  27529  rplogsumlem1  27542  rpvmasumlem  27545  dchrvmasumlem1  27553  dchrvmasum2lem  27554  dchrvmasumlema  27558  dchrisum0flblem2  27567  dchrisum0fno1  27569  dchrisum0re  27571  logdivsum  27591  pntrsumbnd2  27625  pntpbnd1a  27643  pntpbnd1  27644  pntibndlem2  27649  pntlemr  27660  pntlemj  27661  pntlemf  27663  pnt2  27671  padicabv  27688  ostth2lem2  27692  sltrec  27879  madebday  27952  sltn0  27957  addsproplem6  28021  sleadd1  28036  negsproplem6  28079  mulsproplem13  28168  mulsproplem14  28169  sltmuld  28177  mulsgt0d  28185  halfcut  28430  f1otrg  28893  brbtwn2  28934  colinearalglem2  28936  axcgrtr  28944  axcgrid  28945  axsegconlem7  28952  axsegcon  28956  ax5seglem3  28960  ax5seglem6  28963  ax5seg  28967  axpaschlem  28969  axlowdimlem17  28987  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  ecgrtg  29012  usgredg2v  29258  vtxdgoddnumeven  29585  2trlond  29968  eupthp1  30244  nmobndi  30803  ubthlem2  30899  ubthlem3  30900  minvecolem2  30903  shuni  31328  pjhthlem1  31419  chscllem2  31666  pjcompi  31700  mayete3i  31756  unoplin  31948  hmoplin  31970  nmophmi  32059  mdslmd4i  32361  isoun  32716  submuladdd  32756  xrge0addcld  32772  xrofsup  32777  eliccelico  32785  elicoelioo  32786  difioo  32790  rexdiv  32892  mgcmnt1d  32971  mgcmnt2d  32972  chnub  32985  xrge0addgt0  33004  omndadd2d  33067  omndadd2rd  33068  omndmul2  33071  cycpmcl  33118  cycpm2tr  33121  cyc3evpm  33152  cycpmconjslem2  33157  fldgensdrg  33295  ofldchr  33323  qusker  33356  eqgvscpbl  33357  ringlsmss1  33403  ringlsmss2  33404  lidlmcld  33426  intlidl  33427  lidlunitel  33430  elrspunidl  33435  idlinsubrg  33438  isprmidlc  33454  rhmpreimaprmidl  33458  qsidomlem1  33459  ssdifidllem  33463  mxidlmaxv  33475  mxidlprm  33477  ssmxidllem  33480  opprmxidlabs  33494  qsdrnglem2  33503  resssra  33616  ply1degltdimlem  33649  lindsunlem  33651  finexttrb  33689  fldgenfldext  33692  algextdeglem4  33725  algextdeglem8  33729  mdetpmtr2  33784  mdetpmtr12  33785  madjusmdetlem1  33787  madjusmdetlem4  33790  rhmpreimacn  33845  unitdivcld  33861  xrge0mulc1cn  33901  qqhnm  33952  esumcst  34043  esumfsup  34050  esumpmono  34059  esumcvg  34066  difelsiga  34113  sigapisys  34135  sigapildsys  34142  ldgenpisyslem1  34143  1stmbfm  34241  2ndmbfm  34242  dya2icoseg  34258  sibfinima  34320  probmeasb  34411  orvcgteel  34448  orvclteel  34453  ballotlemsima  34496  ballotlemfrceq  34509  sgnmul  34523  ccatmulgnn0dir  34535  fct2relem  34590  ftc2re  34591  chtvalz  34622  subfacp1lem2a  35164  subfaclim  35172  erdsze2lem2  35188  cvmliftlem2  35270  cvmliftlem10  35278  cvmliftlem13  35280  cvmliftiota  35285  cvmlift2lem9  35295  cvmlift2lem11  35297  cvmlift2lem12  35298  cvmliftphtlem  35301  cvmlift3lem6  35308  cvmlift3lem7  35309  cvmlift3lem9  35311  snmlff  35313  mrsubfval  35492  wzel  35805  wsuclem  35806  brsegle  36089  opnregcld  36312  weiunfrlem  36446  fin2so  37593  poimirlem17  37623  poimirlem23  37629  opnmbllem0  37642  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  itg2addnc  37660  itg2gt0cn  37661  ftc1cnnclem  37677  ftc1cnnc  37678  areacirclem5  37698  indexdom  37720  sstotbnd2  37760  isbnd3  37770  isbnd3b  37771  cntotbnd  37782  ismtyima  37789  heibor1lem  37795  heiborlem8  37804  rrncmslem  37818  reheibor  37825  lkrlsp  39083  lshpkrlem5  39095  ldualssvscl  39139  ldualssvsubcl  39140  llnmlplnN  39521  llncvrlpln  39540  pmapjat1  39835  pclfinN  39882  lautlt  40073  lauteq  40077  lautco  40079  ltrn11  40108  ltrnle  40111  ltrneq2  40130  cdlemednuN  40282  cdleme20k  40301  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21c  40309  cdleme22e  40326  cdleme22eALTN  40327  cdlemefrs32fva  40382  cdlemg4g  40598  cdlemg18b  40661  cdlemg18c  40662  cdlemj3  40805  dia2dimlem5  41050  dvhopN  41098  cdlemm10N  41100  dihjatcclem4  41403  dochexmidlem2  41443  lclkrlem2o  41503  lcfrlem5  41528  lcfrlem6  41529  lcdlssvscl  41588  mapdpglem6  41660  mapdpglem9  41662  mapdpglem12  41665  mapdpglem14  41667  mapdindp0  41701  hdmaprnlem7N  41837  hdmaprnlem8N  41838  hdmaprnlem3eN  41840  hgmapvvlem3  41907  dvun  42367  addinvcom  42437  evlsaddval  42554  evlsmulval  42555  evladdval  42561  evlmulval  42562  mzpsubst  42735  eldioph2lem1  42747  eldioph2lem2  42748  eldioph2b  42750  diophin  42759  irrapxlem2  42810  irrapxlem4  42812  irrapxlem5  42813  pellexlem1  42816  pellexlem2  42817  pellexlem6  42821  elpell1qr2  42859  pell1qrgaplem  42860  pell1qrgap  42861  pellqrex  42866  pellfundex  42873  pellfund14  42885  rmspecsqrtnq  42893  rmxyadd  42909  congsub  42958  mzpcong  42960  congrep  42961  acongtr  42966  acongrep  42968  jm2.19lem1  42977  jm2.22  42983  jm2.23  42984  jm2.26lem3  42989  jm2.26  42990  jm2.27a  42993  fnwe2lem2  43039  aomclem6  43047  hbtlem2  43112  hbtlem4  43114  hbtlem5  43116  dgraa0p  43137  rngunsnply  43157  proot1hash  43183  nnoeomeqom  43301  cantnf2  43314  omabs2  43321  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  expgrowth  44330  fpmd  45208  abslt2sqd  45309  ioondisj2  45445  ioondisj1  45446  eliocre  45461  ioossioobi  45469  iooiinicc  45494  iooiinioc  45508  icossico2  45516  lptioo2  45586  limcresiooub  45597  limsupequzlem  45677  xlimmnfvlem2  45788  xlimpnfvlem2  45792  cncfuni  45841  cncfiooicclem1  45848  cxpcncf2  45854  dvcnre  45871  dvresntr  45873  dvresioo  45876  dvbdfbdioolem1  45883  dvnmptdivc  45893  dvnxpaek  45897  itgsinexplem1  45909  itgcoscmulx  45924  itgiccshift  45935  itgperiod  45936  ovolsplit  45943  stoweidlem11  45966  stoweidlem26  45981  stoweidlem34  45989  stoweidlem36  45991  stoweidlem38  45993  stirlinglem5  46033  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem20  46082  fourierdlem58  46119  fourierdlem72  46133  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem79  46140  fourierdlem80  46141  fourierdlem87  46148  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  fourierdlem113  46174  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem46  46235  etransclem47  46236  rrndistlt  46245  rrnprjdstle  46256  ioorrnopnxrlem  46261  sge0ssre  46352  sge0seq  46401  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidifhspdmvle  46575  hoiqssbllem2  46578  ovolval5lem2  46608  iinhoiicc  46629  iunhoiioo  46631  vonioolem2  46636  vonicclem2  46639  issmflem  46682  submodlt  47289  iccpartdisj  47361  m1expevenALTV  47571  fpprel2  47665  tgoldbach  47741  opstrgric  47832  nn0eo  48377  fdivpm  48392  refdivpm  48393  elbigolo1  48406  logbpw2m1  48416  fllog2  48417  dignn0flhalflem1  48464  dignn0flhalflem2  48465  itsclinecirc0in  48624  2itscplem2  48628  itscnhlinecirc02plem1  48631  iccdisj2  48693