Theorem syl22anc 835

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 833	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 206  df-an 396

This theorem is referenced by:  preqsnd  4786  fr2nr  5558  soltmin  6030  f1oprg  6744  f1prex  7136  fveqf1o  7155  weniso  7205  fr3nr  7600  suppofssd  7990  smogt  8169  smorndom  8170  oacomf1o  8358  enpr2d  8792  difsnen  8794  undom  8800  enfixsn  8821  domss2  8872  ssenen  8887  marypha1lem  9122  fisupcl  9158  ordtypelem3  9209  ordtypelem8  9214  oieu  9228  oismo  9229  wofib  9234  wemaplem2  9236  wemapso  9240  wemapso2lem  9241  unxpwdom2  9277  infdifsn  9345  oemapvali  9372  cantnflem1c  9375  cantnflem1  9377  cantnf  9381  cnfcom3  9392  trpredelss  9411  trpredpo  9414  r1ordg  9467  dif1card  9697  infxpenlem  9700  dfac8clem  9719  infxp  9902  infmap2  9905  cflim2  9950  coftr  9960  fin2i2  10005  enfin2i  10008  fin23lem26  10012  fin23lem27  10015  fin23lem40  10038  isf32lem2  10041  isf32lem3  10042  isf32lem4  10043  isf32lem7  10046  isf32lem9  10048  fin1a2lem13  10099  fin12  10100  alephexp1  10266  gchdomtri  10316  fpwwe2lem11  10328  fpwwe2lem12  10329  gchpwdom  10357  gchhar  10366  adderpqlem  10641  mulerpqlem  10642  addassnq  10645  mulassnq  10646  distrnq  10648  mulidnq  10650  recmulnq  10651  ltexnq  10662  distrlem1pr  10712  distrlem4pr  10713  prlem936  10734  reclem3pr  10736  mulcmpblnr  10758  mulgt0d  11060  mul4d  11117  add4d  11133  add42d  11134  subcan  11206  addsub4d  11309  subadd4d  11310  sub4d  11311  2addsubd  11312  addsubeq4d  11313  muladdd  11363  mulsubd  11364  addgegt0d  11478  addgtge0d  11479  addge0d  11481  mulge0d  11482  le2addd  11524  le2subd  11525  ltleaddd  11526  leltaddd  11527  lt2subd  11529  divdivdiv  11606  divcan5  11607  divne0d  11697  recdivd  11698  recdiv2d  11699  divcan6d  11700  ddcand  11701  rec11d  11702  divmuldivd  11722  divmul13d  11723  divmul24d  11724  divadddivd  11725  divsubdivd  11726  divmuleqd  11727  divdivdivd  11728  subrecd  11736  mulge0b  11775  recreclt  11804  divgt0d  11840  mulgt1d  11841  lemulge11d  11842  lemulge12d  11843  ltmul12ad  11846  lemul12ad  11847  lemul12bd  11848  supmul1  11874  nndivtr  11950  qreccl  12638  ledivdivd  12726  lediv12ad  12760  lt2mul2divd  12770  xlt2add  12923  supxrun  12979  supxrre  12990  infxrre  12999  elicore  13060  iccss2  13079  iccssico2  13082  lincmb01cmp  13156  iccf1o  13157  fzrev2i  13250  2tnp1ge0ge0  13477  m1modnnsub1  13565  modaddmodup  13582  modaddmodlo  13583  modsubdir  13588  fzennn  13616  sermono  13683  mulexpz  13751  expaddz  13755  sqdiv  13769  expsubd  13803  ltexp2a  13812  expmordi  13813  leexp2a  13818  expmulnbnd  13878  digit1  13880  lt2sqd  13901  le2sqd  13902  sq11d  13903  bcm1k  13957  bcp1n  13958  bcp1nk  13959  hashf1lem1  14096  hashf1lem1OLD  14097  cshw1  14463  2swrd2eqwrdeq  14594  ofccat  14608  absrele  14948  sqreulem  14999  sqrtmuld  15064  sqrtsq2d  15065  sqrtled  15066  sqrtltd  15067  sqr11d  15068  abs3lemd  15101  rlimuni  15187  climuni  15189  lo1resb  15201  o1resb  15203  2clim  15209  addcn2  15231  mulcn2  15233  o1of2  15250  o1rlimmul  15256  lo1add  15264  lo1mul  15265  isercolllem1  15304  caucvgrlem  15312  iseraltlem2  15322  iseraltlem3  15323  mptfzshft  15418  fsumrev  15419  fsum0diag2  15423  binomlem  15469  climcndslem1  15489  climcndslem2  15490  harmonic  15499  mertenslem1  15524  fprodser  15587  fprodrev  15615  efcllem  15715  moddvds  15902  dvds1  15956  dvdsext  15958  evennn2n  15988  bitsinv1  16077  sadaddlem  16101  sadasslem  16105  sadeq  16107  mulgcd  16184  dvdssqlem  16199  lcmftp  16269  rpmulgcd2  16289  coprmproddvdslem  16295  isprm5  16340  isprm6  16347  crth  16407  eulerthlem2  16411  prmdiveq  16415  pythagtriplem11  16454  pythagtriplem13  16456  pcgcd1  16506  pcprmpw2  16511  pcaddlem  16517  fldivp1  16526  4sqlem12  16585  4sqlem14  16587  4sqlem15  16588  4sqlem16  16589  vdwapun  16603  mreexexlem4d  17273  acsfn1  17287  acsfn2  17289  sscpwex  17444  rescabs  17464  yonedainv  17915  subm0  18369  pmtrfb  18988  psgnunilem1  19016  odmodnn0  19063  odeq  19073  dfod2  19086  sylow1lem1  19118  lsmsubg  19174  lsmmod  19196  lsmdisj2  19203  ghmplusg  19362  odadd  19366  gexexlem  19368  lt6abl  19411  cyggex2  19413  dprdfinv  19537  dmdprdsplitlem  19555  dpjidcl  19576  ablfacrp  19584  ablfacrp2  19585  ablfac1c  19589  ablfac1eu  19591  acsfn1p  19982  lcomfsupp  20078  lssvancl1  20121  lssvnegcl  20133  lspprvacl  20176  lspsneli  20178  lspsn  20179  lmhmplusg  20221  lmhmima  20224  lmhmpreima  20225  reslmhm  20229  lbsind2  20258  lsmcl  20260  lsmelval2  20262  lsppreli  20267  lspprabs  20272  pj1lmhm  20277  lssvs0or  20287  lspabs3  20298  lspfixed  20305  lspexch  20306  lsmcv  20318  lspsolv  20320  lidlmcl  20401  drngnidl  20413  2idlcpbl  20418  gzrngunit  20576  zringlpirlem3  20598  prmirredlem  20606  znf1o  20671  znunithash  20684  frlmsubgval  20882  frlmvplusgvalc  20884  frlmvscaval  20885  frlmphllem  20897  frlmphl  20898  frlmssuvc1  20911  frlmsslsp  20913  frlmup1  20915  frlmup2  20916  lindfind2  20935  lindfrn  20938  f1lindf  20939  islindf4  20955  mplbas2  21153  evlslem3  21200  evlslem1  21202  coe1addfv  21346  lply1binom  21387  evl1addd  21417  evl1subd  21418  evl1muld  21419  mamudi  21460  mamudir  21461  1marepvmarrepid  21632  mdetrlin  21659  smadiadetglem1  21728  smadiadetg  21730  cramerimplem1  21740  mat2pmatscmxcl  21797  m2pmfzgsumcl  21805  pmatcollpw  21838  pmatcollpwfi  21839  pmatcollpw3fi1lem1  21843  cpmidpmatlem2  21928  cpmadugsumlemF  21933  chcoeffeqlem  21942  ntrin  22120  topssnei  22183  restbas  22217  restntr  22241  cnntri  22330  fiuncmp  22463  nllyrest  22545  nllyidm  22548  hausllycmp  22553  cldllycmp  22554  hauspwdom  22560  txcld  22662  txcn  22685  txlly  22695  txnlly  22696  txhaus  22706  txlm  22707  txkgen  22711  xkococnlem  22718  cnmpt2res  22736  xkoinjcn  22746  basqtop  22770  qtopeu  22775  trfbas2  22902  neifil  22939  hausflim  23040  alexsubALTlem2  23107  cnextfval  23121  cnextfvval  23124  cnextf  23125  cnextfres  23128  clssubg  23168  utop2nei  23310  utop3cls  23311  utopreg  23312  psmetlecl  23376  xmetlecl  23407  prdsxmetlem  23429  bldisj  23459  imasf1obl  23550  prdsbl  23553  stdbdmet  23578  stdbdmopn  23580  met2ndci  23584  metcnp  23603  metustto  23615  metustexhalf  23618  cfilucfil  23621  metucn  23633  lssnlm  23771  nmotri  23809  nmoid  23812  tgioo  23865  blcvx  23867  xrsmopn  23881  reperflem  23887  reconnlem2  23896  opnreen  23900  metdsge  23918  metdsre  23922  metdscnlem  23924  metnrmlem1a  23927  metnrmlem1  23928  metnrmlem3  23930  cncfmet  23978  cnmpopc  23997  icopnfcnv  24011  icopnfhmeo  24012  cnllycmp  24025  evth  24028  lebnumii  24035  nmoleub2lem3  24184  iscfil2  24335  cfil3i  24338  iscfil3  24342  cfilfcls  24343  iscau3  24347  iscmet3lem2  24361  caubl  24377  lmcau  24382  cssbn  24444  rrxcph  24461  minveclem2  24495  pjthlem1  24506  pjthlem2  24507  ivthicc  24527  ovollecl  24552  ovolunlem1a  24565  ovolunnul  24569  ovoliunlem1  24571  ismbl2  24596  nulmbl2  24605  unmbl  24606  volun  24614  voliunlem2  24620  ioombl1lem2  24628  uniioombllem2a  24651  uniioombllem3  24654  uniioombllem4  24655  dyaddisjlem  24664  dyadmaxlem  24666  opnmbllem  24670  volsup2  24674  volcn  24675  ismbfd  24708  mbfi1fseqlem1  24785  mbfi1fseqlem5  24789  itg2lecl  24808  itg2monolem2  24821  itg2gt0  24830  itgspliticc  24906  ellimc3  24948  limcres  24955  dvfval  24966  dvres3  24982  dvres3a  24983  dvmptresicc  24985  dvnff  24992  dvnadd  24998  dvn2bss  24999  dvnres  25000  dvcmul  25013  dvcmulf  25014  dvmptres3  25025  dvmptres2  25031  dvmptntr  25040  dvexp3  25047  dvferm1lem  25053  dvlip  25062  dvlipcn  25063  dvlip2  25064  c1liplem1  25065  dvgt0lem1  25071  dvgt0lem2  25072  dvne0  25080  lhop1lem  25082  lhop2  25084  lhop  25085  dvcnvrelem1  25086  dvcnvrelem2  25087  dvcvx  25089  dvfsumle  25090  dvfsumabs  25092  dvfsumlem2  25096  ftc1lem6  25110  ftc1  25111  ftc2ditglem  25114  itgsubstlem  25117  itgpowd  25119  tdeglem4  25129  tdeglem4OLD  25130  mdegaddle  25144  mdegmullem  25148  ply1rem  25233  fta1glem2  25236  fta1blem  25238  ig1peu  25241  ig1pdvds  25246  dgrmulc  25337  dgrcolem1  25339  plydivlem4  25361  plydiveu  25363  fta1lem  25372  vieta1lem1  25375  vieta1lem2  25376  plyexmo  25378  taylfvallem1  25421  taylfval  25423  tayl0  25426  taylplem1  25427  taylply2  25432  taylply  25433  dvtaylp  25434  dvntaylp  25435  dvntaylp0  25436  taylthlem1  25437  taylthlem2  25438  ulmcaulem  25458  ulmcau  25459  ulmcn  25463  ulmdvlem1  25464  radcnvlem1  25477  radcnvle  25484  psercn  25490  pserdvlem2  25492  pserdv  25493  abelth  25505  tanregt0  25600  dvlog2lem  25712  efopn  25718  logtayllem  25719  logccv  25723  cxplt3  25760  cxpmul2zd  25776  cxpltd  25779  cxpled  25780  cxplt3d  25794  cxple3d  25795  dvsqrt  25800  cxpcn3  25806  cxpaddle  25810  cxpeq  25815  angcan  25857  angvald  25859  ang180lem2  25865  ang180  25869  isosctrlem3  25875  dquartlem1  25906  atantayl2  25993  leibpi  25997  log2tlbnd  26000  birthdaylem3  26008  xrlimcnp  26023  efrlim  26024  o1cxp  26029  jensenlem2  26042  jensen  26043  fsumharmonic  26066  lgamucov  26092  lgamcvg2  26109  wilthlem1  26122  basellem3  26137  basellem6  26140  basellem8  26142  ppisval  26158  chtwordi  26210  ppiwordi  26216  mumullem2  26234  dvdsmulf1o  26248  fsumvma  26266  fsumvma2  26267  chpchtsum  26272  chpub  26273  logfacubnd  26274  dchrmulcl  26302  dchrinv  26314  dchrptlem1  26317  dchrptlem2  26318  sumdchr2  26323  dchr2sum  26326  bposlem7  26343  lgslem1  26350  lgslem3  26352  lgsdirprm  26384  lgsqrlem2  26400  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem4  26431  lgseisen  26432  lgsquadlem1  26433  lgsquad2lem1  26437  lgsquad3  26440  m1lgs  26441  2sqlem7  26477  2sq2  26486  2sqmod  26489  chebbnd1lem2  26523  chebbnd1lem3  26524  rplogsumlem1  26537  rpvmasumlem  26540  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasumlema  26553  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0re  26566  logdivsum  26586  pntrsumbnd2  26620  pntpbnd1a  26638  pntpbnd1  26639  pntibndlem2  26644  pntlemr  26655  pntlemj  26656  pntlemf  26658  pnt2  26666  padicabv  26683  ostth2lem2  26687  f1otrg  27136  brbtwn2  27176  colinearalglem2  27178  axcgrtr  27186  axcgrid  27187  axsegconlem7  27194  axsegcon  27198  ax5seglem3  27202  ax5seglem6  27205  ax5seg  27209  axpaschlem  27211  axlowdimlem17  27229  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  ecgrtg  27254  usgredg2v  27497  vtxdgoddnumeven  27823  2trlond  28205  eupthp1  28481  nmobndi  29038  ubthlem2  29134  ubthlem3  29135  minvecolem2  29138  shuni  29563  pjhthlem1  29654  chscllem2  29901  pjcompi  29935  mayete3i  29991  unoplin  30183  hmoplin  30205  nmophmi  30294  mdslmd4i  30596  isoun  30936  xrge0addcld  30987  xrofsup  30992  eliccelico  31000  elicoelioo  31001  difioo  31005  rexdiv  31102  mgcmnt1d  31177  mgcmnt2d  31178  xrge0addgt0  31202  omndadd2d  31236  omndadd2rd  31237  omndmul2  31240  cycpmcl  31285  cycpm2tr  31288  cyc3evpm  31319  cycpmconjslem2  31324  freshmansdream  31386  ofldchr  31415  qusker  31451  eqgvscpbl  31452  ringlsmss1  31486  ringlsmss2  31487  intlidl  31504  rhmpreimaidl  31505  elrspunidl  31508  idlinsubrg  31510  isprmidlc  31525  rhmpreimaprmidl  31529  qsidomlem1  31530  mxidlprm  31542  ssmxidllem  31543  lindsunlem  31607  finexttrb  31639  mdetpmtr2  31676  mdetpmtr12  31677  madjusmdetlem1  31679  madjusmdetlem4  31682  rhmpreimacn  31737  unitdivcld  31753  xrge0mulc1cn  31793  qqhnm  31840  esumcst  31931  esumfsup  31938  esumpmono  31947  esumcvg  31954  difelsiga  32001  sigapisys  32023  sigapildsys  32030  ldgenpisyslem1  32031  1stmbfm  32127  2ndmbfm  32128  dya2icoseg  32144  sibfinima  32206  probmeasb  32297  orvcgteel  32334  orvclteel  32339  ballotlemsima  32382  ballotlemfrceq  32395  sgnmul  32409  ccatmulgnn0dir  32421  fct2relem  32477  ftc2re  32478  chtvalz  32509  subfacp1lem2a  33042  subfaclim  33050  erdsze2lem2  33066  cvmliftlem2  33148  cvmliftlem10  33156  cvmliftlem13  33158  cvmliftiota  33163  cvmlift2lem9  33173  cvmlift2lem11  33175  cvmlift2lem12  33176  cvmliftphtlem  33179  cvmlift3lem6  33186  cvmlift3lem7  33187  cvmlift3lem9  33189  snmlff  33191  mrsubfval  33370  wzel  33745  wsuclem  33746  sltrec  33941  madebday  34007  sltn0  34012  brsegle  34337  opnregcld  34446  fin2so  35691  poimirlem17  35721  poimirlem23  35727  opnmbllem0  35740  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem  35755  itg2addnc  35758  itg2gt0cn  35759  ftc1cnnclem  35775  ftc1cnnc  35776  areacirclem5  35796  indexdom  35819  sstotbnd2  35859  isbnd3  35869  isbnd3b  35870  cntotbnd  35881  ismtyima  35888  heibor1lem  35894  heiborlem8  35903  rrncmslem  35917  reheibor  35924  lkrlsp  37043  lshpkrlem5  37055  ldualssvscl  37099  ldualssvsubcl  37100  llnmlplnN  37480  llncvrlpln  37499  pmapjat1  37794  pclfinN  37841  lautlt  38032  lauteq  38036  lautco  38038  ltrn11  38067  ltrnle  38070  ltrneq2  38089  cdlemednuN  38241  cdleme20k  38260  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21c  38268  cdleme22e  38285  cdleme22eALTN  38286  cdlemefrs32fva  38341  cdlemg4g  38557  cdlemg18b  38620  cdlemg18c  38621  cdlemj3  38764  dia2dimlem5  39009  dvhopN  39057  cdlemm10N  39059  dihjatcclem4  39362  dochexmidlem2  39402  lclkrlem2o  39462  lcfrlem5  39487  lcfrlem6  39488  lcdlssvscl  39547  mapdpglem6  39619  mapdpglem9  39621  mapdpglem12  39624  mapdpglem14  39626  mapdindp0  39660  hdmaprnlem7N  39796  hdmaprnlem8N  39797  hdmaprnlem3eN  39799  hgmapvvlem3  39866  evlsaddval  40200  evlsmulval  40201  addinvcom  40334  mzpsubst  40486  eldioph2lem1  40498  eldioph2lem2  40499  eldioph2b  40501  diophin  40510  irrapxlem2  40561  irrapxlem4  40563  irrapxlem5  40564  pellexlem1  40567  pellexlem2  40568  pellexlem6  40572  elpell1qr2  40610  pell1qrgaplem  40611  pell1qrgap  40612  pellqrex  40617  pellfundex  40624  pellfund14  40636  rmspecsqrtnq  40644  rmxyadd  40659  congsub  40708  mzpcong  40710  congrep  40711  acongtr  40716  acongrep  40718  jm2.19lem1  40727  jm2.22  40733  jm2.23  40734  jm2.26lem3  40739  jm2.26  40740  jm2.27a  40743  fnwe2lem2  40792  aomclem6  40800  hbtlem2  40865  hbtlem4  40867  hbtlem5  40869  dgraa0p  40890  rngunsnply  40914  proot1hash  40941  expgrowth  41842  fpmd  42700  abslt2sqd  42789  ioondisj2  42921  ioondisj1  42922  eliocre  42937  ioossioobi  42945  iooiinicc  42970  iooiinioc  42984  icossico2  42992  lptioo2  43062  limcresiooub  43073  limsupequzlem  43153  xlimmnfvlem2  43264  xlimpnfvlem2  43268  cncfuni  43317  cncfiooicclem1  43324  cxpcncf2  43330  dvcnre  43347  dvresntr  43349  dvresioo  43352  dvbdfbdioolem1  43359  dvnmptdivc  43369  dvnxpaek  43373  itgsinexplem1  43385  itgcoscmulx  43400  itgiccshift  43411  itgperiod  43412  ovolsplit  43419  stoweidlem11  43442  stoweidlem26  43457  stoweidlem34  43465  stoweidlem36  43467  stoweidlem38  43469  stirlinglem5  43509  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem20  43558  fourierdlem58  43595  fourierdlem72  43609  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem79  43616  fourierdlem80  43617  fourierdlem87  43624  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem113  43650  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  etransclem46  43711  etransclem47  43712  rrndistlt  43721  rrnprjdstle  43732  ioorrnopnxrlem  43737  sge0ssre  43825  sge0seq  43874  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidifhspdmvle  44048  hoiqssbllem2  44051  ovolval5lem2  44081  iinhoiicc  44102  iunhoiioo  44104  vonioolem2  44109  vonicclem2  44112  issmflem  44150  iccpartdisj  44777  m1expevenALTV  44987  fpprel2  45081  tgoldbach  45157  strisomgrop  45180  nn0eo  45762  fdivpm  45777  refdivpm  45778  elbigolo1  45791  logbpw2m1  45801  fllog2  45802  dignn0flhalflem1  45849  dignn0flhalflem2  45850  itsclinecirc0in  46009  2itscplem2  46013  itscnhlinecirc02plem1  46016  iccdisj2  46079