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  4789  fr2nr  5533  soltmin  5996  f1oprg  6659  f1prex  7040  fveqf1o  7058  weniso  7107  fr3nr  7494  suppofssd  7867  smogt  8004  smorndom  8005  oacomf1o  8191  enpr2d  8597  difsnen  8599  undom  8605  enfixsn  8626  domss2  8676  ssenen  8691  marypha1lem  8897  fisupcl  8933  ordtypelem3  8984  ordtypelem8  8989  oieu  9003  oismo  9004  wofib  9009  wemaplem2  9011  wemapso  9015  wemapso2lem  9016  unxpwdom2  9052  infdifsn  9120  oemapvali  9147  cantnflem1c  9150  cantnflem1  9152  cantnf  9156  cnfcom3  9167  r1ordg  9207  dif1card  9436  infxpenlem  9439  dfac8clem  9458  infxp  9637  infmap2  9640  cflim2  9685  coftr  9695  fin2i2  9740  enfin2i  9743  fin23lem26  9747  fin23lem27  9750  fin23lem40  9773  isf32lem2  9776  isf32lem3  9777  isf32lem4  9778  isf32lem7  9781  isf32lem9  9783  fin1a2lem13  9834  fin12  9835  alephexp1  10001  gchdomtri  10051  fpwwe2lem12  10063  fpwwe2lem13  10064  gchpwdom  10092  gchhar  10101  adderpqlem  10376  mulerpqlem  10377  addassnq  10380  mulassnq  10381  distrnq  10383  mulidnq  10385  recmulnq  10386  ltexnq  10397  distrlem1pr  10447  distrlem4pr  10448  prlem936  10469  reclem3pr  10471  mulcmpblnr  10493  mulgt0d  10795  mul4d  10852  add4d  10868  add42d  10869  subcan  10941  addsub4d  11044  subadd4d  11045  sub4d  11046  2addsubd  11047  addsubeq4d  11048  muladdd  11098  mulsubd  11099  addgegt0d  11213  addgtge0d  11214  addge0d  11216  mulge0d  11217  le2addd  11259  le2subd  11260  ltleaddd  11261  leltaddd  11262  lt2subd  11264  divdivdiv  11341  divcan5  11342  divne0d  11432  recdivd  11433  recdiv2d  11434  divcan6d  11435  ddcand  11436  rec11d  11437  divmuldivd  11457  divmul13d  11458  divmul24d  11459  divadddivd  11460  divsubdivd  11461  divmuleqd  11462  divdivdivd  11463  subrecd  11471  mulge0b  11510  recreclt  11539  divgt0d  11575  mulgt1d  11576  lemulge11d  11577  lemulge12d  11578  ltmul12ad  11581  lemul12ad  11582  lemul12bd  11583  supmul1  11610  nndivtr  11685  qreccl  12369  ledivdivd  12457  lediv12ad  12491  lt2mul2divd  12501  xlt2add  12654  supxrun  12710  supxrre  12721  infxrre  12730  elicore  12790  iccss2  12808  iccssico2  12811  lincmb01cmp  12882  iccf1o  12883  fzrev2i  12973  2tnp1ge0ge0  13200  m1modnnsub1  13286  modaddmodup  13303  modaddmodlo  13304  modsubdir  13309  fzennn  13337  sermono  13403  mulexpz  13470  expaddz  13474  sqdiv  13488  expsubd  13522  ltexp2a  13531  expmordi  13532  leexp2a  13537  expmulnbnd  13597  digit1  13599  lt2sqd  13620  le2sqd  13621  sq11d  13622  bcm1k  13676  bcp1n  13677  bcp1nk  13678  hashf1lem1  13814  cshw1  14184  2swrd2eqwrdeq  14315  ofccat  14329  absrele  14668  sqreulem  14719  sqrtmuld  14784  sqrtsq2d  14785  sqrtled  14786  sqrtltd  14787  sqr11d  14788  abs3lemd  14821  rlimuni  14907  climuni  14909  lo1resb  14921  o1resb  14923  2clim  14929  addcn2  14950  mulcn2  14952  o1of2  14969  o1rlimmul  14975  lo1add  14983  lo1mul  14984  isercolllem1  15021  caucvgrlem  15029  iseraltlem2  15039  iseraltlem3  15040  mptfzshft  15133  fsumrev  15134  fsum0diag2  15138  binomlem  15184  climcndslem1  15204  climcndslem2  15205  harmonic  15214  mertenslem1  15240  fprodser  15303  fprodrev  15331  efcllem  15431  moddvds  15618  dvds1  15669  dvdsext  15671  evennn2n  15700  bitsinv1  15791  sadaddlem  15815  sadasslem  15819  sadeq  15821  mulgcd  15896  dvdssqlem  15910  lcmftp  15980  rpmulgcd2  16000  coprmproddvdslem  16006  isprm5  16051  isprm6  16058  crth  16115  eulerthlem2  16119  prmdiveq  16123  pythagtriplem11  16162  pythagtriplem13  16164  pcgcd1  16213  pcprmpw2  16218  pcaddlem  16224  fldivp1  16233  4sqlem12  16292  4sqlem14  16294  4sqlem15  16295  4sqlem16  16296  vdwapun  16310  mreexexlem4d  16918  acsfn1  16932  acsfn2  16934  sscpwex  17085  rescabs  17103  yonedainv  17531  subm0  17980  pmtrfb  18593  psgnunilem1  18621  odmodnn0  18668  odeq  18678  dfod2  18691  sylow1lem1  18723  lsmsubg  18779  lsmmod  18801  lsmdisj2  18808  ghmplusg  18966  odadd  18970  gexexlem  18972  lt6abl  19015  cyggex2  19017  dprdfinv  19141  dmdprdsplitlem  19159  dpjidcl  19180  ablfacrp  19188  ablfacrp2  19189  ablfac1c  19193  ablfac1eu  19195  acsfn1p  19578  lcomfsupp  19674  lssvancl1  19716  lssvnegcl  19728  lspprvacl  19771  lspsneli  19773  lspsn  19774  lmhmplusg  19816  lmhmima  19819  lmhmpreima  19820  reslmhm  19824  lbsind2  19853  lsmcl  19855  lsmelval2  19857  lsppreli  19862  lspprabs  19867  pj1lmhm  19872  lssvs0or  19882  lspabs3  19893  lspfixed  19900  lspexch  19901  lsmcv  19913  lspsolv  19915  lidlmcl  19990  drngnidl  20002  2idlcpbl  20007  mplbas2  20251  evlslem3  20293  evlslem1  20295  coe1addfv  20433  lply1binom  20474  evl1addd  20504  evl1subd  20505  evl1muld  20506  gzrngunit  20611  zringlpirlem3  20633  prmirredlem  20640  znf1o  20698  znunithash  20711  frlmsubgval  20909  frlmvplusgvalc  20911  frlmvscaval  20912  frlmphllem  20924  frlmphl  20925  frlmssuvc1  20938  frlmsslsp  20940  frlmup1  20942  frlmup2  20943  lindfind2  20962  lindfrn  20965  f1lindf  20966  islindf4  20982  mamudi  21012  mamudir  21013  1marepvmarrepid  21184  mdetrlin  21211  smadiadetglem1  21280  smadiadetg  21282  cramerimplem1  21292  mat2pmatscmxcl  21348  m2pmfzgsumcl  21356  pmatcollpw  21389  pmatcollpwfi  21390  pmatcollpw3fi1lem1  21394  cpmidpmatlem2  21479  cpmadugsumlemF  21484  chcoeffeqlem  21493  ntrin  21669  topssnei  21732  restbas  21766  restntr  21790  cnntri  21879  fiuncmp  22012  nllyrest  22094  nllyidm  22097  hausllycmp  22102  cldllycmp  22103  hauspwdom  22109  txcld  22211  txcn  22234  txlly  22244  txnlly  22245  txhaus  22255  txlm  22256  txkgen  22260  xkococnlem  22267  cnmpt2res  22285  xkoinjcn  22295  basqtop  22319  qtopeu  22324  trfbas2  22451  neifil  22488  hausflim  22589  alexsubALTlem2  22656  cnextfval  22670  cnextfvval  22673  cnextf  22674  cnextfres  22677  clssubg  22717  utop2nei  22859  utop3cls  22860  utopreg  22861  psmetlecl  22925  xmetlecl  22956  prdsxmetlem  22978  bldisj  23008  imasf1obl  23098  prdsbl  23101  stdbdmet  23126  stdbdmopn  23128  met2ndci  23132  metcnp  23151  metustto  23163  metustexhalf  23166  cfilucfil  23169  metucn  23181  lssnlm  23310  nmotri  23348  nmoid  23351  tgioo  23404  blcvx  23406  xrsmopn  23420  reperflem  23426  reconnlem2  23435  opnreen  23439  metdsge  23457  metdsre  23461  metdscnlem  23463  metnrmlem1a  23466  metnrmlem1  23467  metnrmlem3  23469  cncfmet  23516  cnmpopc  23532  icopnfcnv  23546  icopnfhmeo  23547  cnllycmp  23560  evth  23563  lebnumii  23570  nmoleub2lem3  23719  iscfil2  23869  cfil3i  23872  iscfil3  23876  cfilfcls  23877  iscau3  23881  iscmet3lem2  23895  caubl  23911  lmcau  23916  cssbn  23978  rrxcph  23995  minveclem2  24029  pjthlem1  24040  pjthlem2  24041  ivthicc  24059  ovollecl  24084  ovolunlem1a  24097  ovolunnul  24101  ovoliunlem1  24103  ismbl2  24128  nulmbl2  24137  unmbl  24138  volun  24146  voliunlem2  24152  ioombl1lem2  24160  uniioombllem2a  24183  uniioombllem3  24186  uniioombllem4  24187  dyaddisjlem  24196  dyadmaxlem  24198  opnmbllem  24202  volsup2  24206  volcn  24207  ismbfd  24240  mbfi1fseqlem1  24316  mbfi1fseqlem5  24320  itg2lecl  24339  itg2monolem2  24352  itg2gt0  24361  itgspliticc  24437  ellimc3  24477  limcres  24484  dvfval  24495  dvres3  24511  dvres3a  24512  dvnff  24520  dvnadd  24526  dvn2bss  24527  dvnres  24528  dvcmul  24541  dvcmulf  24542  dvmptres3  24553  dvmptres2  24559  dvmptntr  24568  dvexp3  24575  dvferm1lem  24581  dvlip  24590  dvlipcn  24591  dvlip2  24592  c1liplem1  24593  dvgt0lem1  24599  dvgt0lem2  24600  dvne0  24608  lhop1lem  24610  lhop2  24612  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcvx  24617  dvfsumle  24618  dvfsumabs  24620  dvfsumlem2  24624  ftc1lem6  24638  ftc1  24639  ftc2ditglem  24642  itgsubstlem  24645  tdeglem4  24654  mdegaddle  24668  mdegmullem  24672  ply1rem  24757  fta1glem2  24760  fta1blem  24762  ig1peu  24765  ig1pdvds  24770  dgrmulc  24861  dgrcolem1  24863  plydivlem4  24885  plydiveu  24887  fta1lem  24896  vieta1lem1  24899  vieta1lem2  24900  plyexmo  24902  taylfvallem1  24945  taylfval  24947  tayl0  24950  taylplem1  24951  taylply2  24956  taylply  24957  dvtaylp  24958  dvntaylp  24959  dvntaylp0  24960  taylthlem1  24961  taylthlem2  24962  ulmcaulem  24982  ulmcau  24983  ulmcn  24987  ulmdvlem1  24988  radcnvlem1  25001  radcnvle  25008  psercn  25014  pserdvlem2  25016  pserdv  25017  abelth  25029  tanregt0  25123  dvlog2lem  25235  efopn  25241  logtayllem  25242  logccv  25246  cxplt3  25283  cxpmul2zd  25299  cxpltd  25302  cxpled  25303  cxplt3d  25317  cxple3d  25318  dvsqrt  25323  cxpcn3  25329  cxpaddle  25333  cxpeq  25338  angcan  25380  angvald  25382  ang180lem2  25388  ang180  25392  isosctrlem3  25398  dquartlem1  25429  atantayl2  25516  leibpi  25520  log2tlbnd  25523  birthdaylem3  25531  xrlimcnp  25546  efrlim  25547  o1cxp  25552  jensenlem2  25565  jensen  25566  fsumharmonic  25589  lgamucov  25615  lgamcvg2  25632  wilthlem1  25645  basellem3  25660  basellem6  25663  basellem8  25665  ppisval  25681  chtwordi  25733  ppiwordi  25739  mumullem2  25757  dvdsmulf1o  25771  fsumvma  25789  fsumvma2  25790  chpchtsum  25795  chpub  25796  logfacubnd  25797  dchrmulcl  25825  dchrinv  25837  dchrptlem1  25840  dchrptlem2  25841  sumdchr2  25846  dchr2sum  25849  bposlem7  25866  lgslem1  25873  lgslem3  25875  lgsdirprm  25907  lgsqrlem2  25923  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem4  25954  lgseisen  25955  lgsquadlem1  25956  lgsquad2lem1  25960  lgsquad3  25963  m1lgs  25964  2sqlem7  26000  2sq2  26009  2sqmod  26012  chebbnd1lem2  26046  chebbnd1lem3  26047  rplogsumlem1  26060  rpvmasumlem  26063  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasumlema  26076  dchrisum0flblem2  26085  dchrisum0fno1  26087  dchrisum0re  26089  logdivsum  26109  pntrsumbnd2  26143  pntpbnd1a  26161  pntpbnd1  26162  pntibndlem2  26167  pntlemr  26178  pntlemj  26179  pntlemf  26181  pnt2  26189  padicabv  26206  ostth2lem2  26210  f1otrg  26657  brbtwn2  26691  colinearalglem2  26693  axcgrtr  26701  axcgrid  26702  axsegconlem7  26709  axsegcon  26713  ax5seglem3  26717  ax5seglem6  26720  ax5seg  26724  axpaschlem  26726  axlowdimlem17  26744  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  ecgrtg  26769  usgredg2v  27009  vtxdgoddnumeven  27335  2trlond  27718  eupthp1  27995  nmobndi  28552  ubthlem2  28648  ubthlem3  28649  minvecolem2  28652  shuni  29077  pjhthlem1  29168  chscllem2  29415  pjcompi  29449  mayete3i  29505  unoplin  29697  hmoplin  29719  nmophmi  29808  mdslmd4i  30110  isoun  30437  xrge0addcld  30486  xrofsup  30492  eliccelico  30500  elicoelioo  30501  difioo  30505  rexdiv  30602  xrge0addgt0  30678  omndadd2d  30709  omndadd2rd  30710  omndmul2  30713  cycpmcl  30758  cycpm2tr  30761  cyc3evpm  30792  cycpmconjslem2  30797  freshmansdream  30859  ofldchr  30887  qusker  30918  eqgvscpbl  30919  isprmidlc  30963  qsidomlem1  30965  mxidlprm  30977  ssmxidllem  30978  lindsunlem  31020  finexttrb  31052  mdetpmtr2  31089  mdetpmtr12  31090  madjusmdetlem1  31092  madjusmdetlem4  31095  unitdivcld  31144  xrge0mulc1cn  31184  qqhnm  31231  esumcst  31322  esumfsup  31329  esumpmono  31338  esumcvg  31345  difelsiga  31392  sigapisys  31414  sigapildsys  31421  ldgenpisyslem1  31422  1stmbfm  31518  2ndmbfm  31519  dya2icoseg  31535  sibfinima  31597  probmeasb  31688  orvcgteel  31725  orvclteel  31730  ballotlemsima  31773  ballotlemfrceq  31786  sgnmul  31800  ccatmulgnn0dir  31812  fct2relem  31868  ftc2re  31869  chtvalz  31900  subfacp1lem2a  32427  subfaclim  32435  erdsze2lem2  32451  cvmliftlem2  32533  cvmliftlem10  32541  cvmliftlem13  32543  cvmliftiota  32548  cvmlift2lem9  32558  cvmlift2lem11  32560  cvmlift2lem12  32561  cvmliftphtlem  32564  cvmlift3lem6  32571  cvmlift3lem7  32572  cvmlift3lem9  32574  snmlff  32576  mrsubfval  32755  trpredelss  33071  trpredpo  33074  wzel  33111  wsuclem  33112  sltrec  33278  brsegle  33569  opnregcld  33678  fin2so  34894  poimirlem17  34924  poimirlem23  34930  opnmbllem0  34943  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem  34958  itg2addnc  34961  itg2gt0cn  34962  ftc1cnnclem  34980  ftc1cnnc  34981  areacirclem5  35001  indexdom  35024  sstotbnd2  35067  isbnd3  35077  isbnd3b  35078  cntotbnd  35089  ismtyima  35096  heibor1lem  35102  heiborlem8  35111  rrncmslem  35125  reheibor  35132  lkrlsp  36253  lshpkrlem5  36265  ldualssvscl  36309  ldualssvsubcl  36310  llnmlplnN  36690  llncvrlpln  36709  pmapjat1  37004  pclfinN  37051  lautlt  37242  lauteq  37246  lautco  37248  ltrn11  37277  ltrnle  37280  ltrneq2  37299  cdlemednuN  37451  cdleme20k  37470  cdleme20l2  37472  cdleme20l  37473  cdleme20m  37474  cdleme21c  37478  cdleme22e  37495  cdleme22eALTN  37496  cdlemefrs32fva  37551  cdlemg4g  37767  cdlemg18b  37830  cdlemg18c  37831  cdlemj3  37974  dia2dimlem5  38219  dvhopN  38267  cdlemm10N  38269  dihjatcclem4  38572  dochexmidlem2  38612  lclkrlem2o  38672  lcfrlem5  38697  lcfrlem6  38698  lcdlssvscl  38757  mapdpglem6  38829  mapdpglem9  38831  mapdpglem12  38834  mapdpglem14  38836  mapdindp0  38870  hdmaprnlem7N  39006  hdmaprnlem8N  39007  hdmaprnlem3eN  39009  hgmapvvlem3  39076  mzpsubst  39394  eldioph2lem1  39406  eldioph2lem2  39407  eldioph2b  39409  diophin  39418  irrapxlem2  39469  irrapxlem4  39471  irrapxlem5  39472  pellexlem1  39475  pellexlem2  39476  pellexlem6  39480  elpell1qr2  39518  pell1qrgaplem  39519  pell1qrgap  39520  pellqrex  39525  pellfundex  39532  pellfund14  39544  rmspecsqrtnq  39552  rmxyadd  39567  congsub  39616  mzpcong  39618  congrep  39619  acongtr  39624  acongrep  39626  jm2.19lem1  39635  jm2.22  39641  jm2.23  39642  jm2.26lem3  39647  jm2.26  39648  jm2.27a  39651  fnwe2lem2  39700  aomclem6  39708  hbtlem2  39773  hbtlem4  39775  hbtlem5  39777  dgraa0p  39798  rngunsnply  39822  proot1hash  39849  itgpowd  39870  expgrowth  40716  fpmd  41587  abslt2sqd  41677  ioondisj2  41816  ioondisj1  41817  eliocre  41834  ioossioobi  41842  iooiinicc  41867  iooiinioc  41881  icossico2  41889  lptioo2  41961  limcresiooub  41972  limsupequzlem  42052  xlimmnfvlem2  42163  xlimpnfvlem2  42167  cncfuni  42218  cncfiooicclem1  42225  cxpcncf2  42232  dvcnre  42249  dvresntr  42251  dvmptresicc  42253  dvresioo  42255  dvbdfbdioolem1  42262  dvnmptdivc  42272  dvnxpaek  42276  itgsinexplem1  42288  itgcoscmulx  42303  itgiccshift  42314  itgperiod  42315  ovolsplit  42322  stoweidlem11  42345  stoweidlem26  42360  stoweidlem34  42368  stoweidlem36  42370  stoweidlem38  42372  stirlinglem5  42412  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem20  42461  fourierdlem58  42498  fourierdlem72  42512  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem79  42519  fourierdlem80  42520  fourierdlem87  42527  fourierdlem94  42534  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem113  42553  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  etransclem46  42614  etransclem47  42615  rrndistlt  42624  rrnprjdstle  42635  ioorrnopnxrlem  42640  sge0ssre  42728  sge0seq  42777  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem1  42926  hoidifhspdmvle  42951  hoiqssbllem2  42954  ovolval5lem2  42984  iinhoiicc  43005  iunhoiioo  43007  vonioolem2  43012  vonicclem2  43015  issmflem  43053  iccpartdisj  43646  m1expevenALTV  43861  fpprel2  43955  tgoldbach  44031  strisomgrop  44054  nn0eo  44637  fdivpm  44652  refdivpm  44653  elbigolo1  44666  logbpw2m1  44676  fllog2  44677  dignn0flhalflem1  44724  dignn0flhalflem2  44725  itsclinecirc0in  44811  2itscplem2  44815  itscnhlinecirc02plem1  44818