Theorem syl22anc 838

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 836	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  4883  fr2nr  5677  soltmin  6168  f1oprg  6907  f1prex  7320  fveqf1o  7338  weniso  7390  fr3nr  7807  suppofssd  8244  smogt  8423  smocdmdom  8424  oacomf1o  8621  en2prd  9114  enpr2dOLD  9116  difsnen  9119  undomOLD  9126  enfixsn  9147  domss2  9202  ssenen  9217  marypha1lem  9502  fisupcl  9538  ordtypelem3  9589  ordtypelem8  9594  oieu  9608  oismo  9609  wofib  9614  wemaplem2  9616  wemapso  9620  wemapso2lem  9621  unxpwdom2  9657  infdifsn  9726  oemapvali  9753  cantnflem1c  9756  cantnflem1  9758  cantnf  9762  cnfcom3  9773  r1ordg  9847  dif1card  10079  infxpenlem  10082  dfac8clem  10101  infxp  10283  infmap2  10286  cflim2  10332  coftr  10342  fin2i2  10387  enfin2i  10390  fin23lem26  10394  fin23lem27  10397  fin23lem40  10420  isf32lem2  10423  isf32lem3  10424  isf32lem4  10425  isf32lem7  10428  isf32lem9  10430  fin1a2lem13  10481  fin12  10482  alephexp1  10648  gchdomtri  10698  fpwwe2lem11  10710  fpwwe2lem12  10711  gchpwdom  10739  gchhar  10748  adderpqlem  11023  mulerpqlem  11024  addassnq  11027  mulassnq  11028  distrnq  11030  mulidnq  11032  recmulnq  11033  ltexnq  11044  distrlem1pr  11094  distrlem4pr  11095  prlem936  11116  reclem3pr  11118  mulcmpblnr  11140  mulgt0d  11445  mul4d  11502  add4d  11518  add42d  11519  subcan  11591  addsub4d  11694  subadd4d  11695  sub4d  11696  2addsubd  11697  addsubeq4d  11698  muladdd  11748  mulsubd  11749  addgegt0d  11863  addgtge0d  11864  addge0d  11866  mulge0d  11867  le2addd  11909  le2subd  11910  ltleaddd  11911  leltaddd  11912  lt2subd  11914  divdivdiv  11995  divcan5  11996  divne0d  12086  recdivd  12087  recdiv2d  12088  divcan6d  12089  ddcand  12090  rec11d  12091  divmuldivd  12111  divmul13d  12112  divmul24d  12113  divadddivd  12114  divsubdivd  12115  divmuleqd  12116  divdivdivd  12117  subrecd  12125  mulge0b  12165  recreclt  12194  divgt0d  12230  mulgt1d  12231  lemulge11d  12232  lemulge12d  12233  ltmul12ad  12236  lemul12ad  12237  lemul12bd  12238  supmul1  12264  nndivtr  12340  qreccl  13034  ledivdivd  13124  lediv12ad  13158  lt2mul2divd  13168  xlt2add  13322  supxrun  13378  supxrre  13389  infxrre  13398  elicore  13459  iccss2  13478  iccssico2  13481  lincmb01cmp  13555  iccf1o  13556  fzrev2i  13649  2tnp1ge0ge0  13880  m1modnnsub1  13968  modaddmodup  13985  modaddmodlo  13986  modsubdir  13991  fzennn  14019  sermono  14085  mulexpz  14153  expaddz  14157  sqdiv  14171  expsubd  14207  ltexp2a  14216  expmordi  14217  leexp2a  14222  expmulnbnd  14284  digit1  14286  lt2sqd  14305  le2sqd  14306  sq11d  14307  bcm1k  14364  bcp1n  14365  bcp1nk  14366  hashf1lem1  14504  cshw1  14870  2swrd2eqwrdeq  15002  ofccat  15018  absrele  15357  sqreulem  15408  sqrtmuld  15473  sqrtsq2d  15474  sqrtled  15475  sqrtltd  15476  sqr11d  15477  abs3lemd  15510  rlimuni  15596  climuni  15598  lo1resb  15610  o1resb  15612  2clim  15618  addcn2  15640  mulcn2  15642  o1of2  15659  o1rlimmul  15665  lo1add  15673  lo1mul  15674  isercolllem1  15713  caucvgrlem  15721  iseraltlem2  15731  iseraltlem3  15732  mptfzshft  15826  fsumrev  15827  fsum0diag2  15831  binomlem  15877  climcndslem1  15897  climcndslem2  15898  harmonic  15907  mertenslem1  15932  fprodser  15997  fprodrev  16025  efcllem  16125  moddvds  16313  dvds1  16367  dvdsext  16369  evennn2n  16399  bitsinv1  16488  sadaddlem  16512  sadasslem  16516  sadeq  16518  mulgcd  16595  dvdssqlem  16613  lcmftp  16683  rpmulgcd2  16703  coprmproddvdslem  16709  isprm5  16754  isprm6  16761  crth  16825  eulerthlem2  16829  prmdiveq  16833  pythagtriplem11  16872  pythagtriplem13  16874  pcgcd1  16924  pcprmpw2  16929  pcaddlem  16935  fldivp1  16944  4sqlem12  17003  4sqlem14  17005  4sqlem15  17006  4sqlem16  17007  vdwapun  17021  mreexexlem4d  17705  acsfn1  17719  acsfn2  17721  sscpwex  17876  rescabs  17896  rescabsOLD  17897  yonedainv  18351  subm0  18850  pmtrfb  19507  psgnunilem1  19535  odmodnn0  19582  odeq  19592  dfod2  19606  sylow1lem1  19640  lsmsubg  19696  lsmmod  19717  lsmdisj2  19724  ghmplusg  19888  odadd  19892  gexexlem  19894  lt6abl  19937  cyggex2  19939  dprdfinv  20063  dmdprdsplitlem  20081  dpjidcl  20102  ablfacrp  20110  ablfacrp2  20111  ablfac1c  20115  ablfac1eu  20117  acsfn1p  20822  lcomfsupp  20922  lssvancl1  20966  lssvnegcl  20977  lspprvacl  21020  ellspsni  21022  lspsn  21023  lmhmplusg  21066  lmhmima  21069  lmhmpreima  21070  reslmhm  21074  lbsind2  21103  lsmcl  21105  lsmelval2  21107  lsppreli  21112  lspprabs  21117  pj1lmhm  21122  lssvs0or  21135  lspabs3  21146  lspfixed  21153  lspexch  21154  lsmcv  21166  lspsolv  21168  drngnidl  21276  rhmpreimaidl  21310  rngqiprngimfo  21334  rngqiprngfulem4  21347  gzrngunit  21474  zringlpirlem3  21498  prmirredlem  21506  znf1o  21593  znunithash  21606  freshmansdream  21616  frlmsubgval  21808  frlmvplusgvalc  21810  frlmvscaval  21811  frlmphllem  21823  frlmphl  21824  frlmssuvc1  21837  frlmsslsp  21839  frlmup1  21841  frlmup2  21842  lindfind2  21861  lindfrn  21864  f1lindf  21865  islindf4  21881  mplbas2  22083  evlslem3  22127  evlslem1  22129  coe1addfv  22289  lply1binom  22335  evl1addd  22366  evl1subd  22367  evl1muld  22368  mamudi  22428  mamudir  22429  1marepvmarrepid  22602  mdetrlin  22629  smadiadetglem1  22698  smadiadetg  22700  cramerimplem1  22710  mat2pmatscmxcl  22767  m2pmfzgsumcl  22775  pmatcollpw  22808  pmatcollpwfi  22809  pmatcollpw3fi1lem1  22813  cpmidpmatlem2  22898  cpmadugsumlemF  22903  chcoeffeqlem  22912  ntrin  23090  topssnei  23153  restbas  23187  restntr  23211  cnntri  23300  fiuncmp  23433  nllyrest  23515  nllyidm  23518  hausllycmp  23523  cldllycmp  23524  hauspwdom  23530  txcld  23632  txcn  23655  txlly  23665  txnlly  23666  txhaus  23676  txlm  23677  txkgen  23681  xkococnlem  23688  cnmpt2res  23706  xkoinjcn  23716  basqtop  23740  qtopeu  23745  trfbas2  23872  neifil  23909  hausflim  24010  alexsubALTlem2  24077  cnextfval  24091  cnextfvval  24094  cnextf  24095  cnextfres  24098  clssubg  24138  utop2nei  24280  utop3cls  24281  utopreg  24282  psmetlecl  24346  xmetlecl  24377  prdsxmetlem  24399  bldisj  24429  imasf1obl  24522  prdsbl  24525  stdbdmet  24550  stdbdmopn  24552  met2ndci  24556  metcnp  24575  metustto  24587  metustexhalf  24590  cfilucfil  24593  metucn  24605  lssnlm  24743  nmotri  24781  nmoid  24784  tgioo  24837  blcvx  24839  xrsmopn  24853  reperflem  24859  reconnlem2  24868  opnreen  24872  metdsge  24890  metdsre  24894  metdscnlem  24896  metnrmlem1a  24899  metnrmlem1  24900  metnrmlem3  24902  cncfmet  24954  cnmpopc  24974  icopnfcnv  24992  icopnfhmeo  24993  cnllycmp  25007  evth  25010  lebnumii  25017  nmoleub2lem3  25167  iscfil2  25319  cfil3i  25322  iscfil3  25326  cfilfcls  25327  iscau3  25331  iscmet3lem2  25345  caubl  25361  lmcau  25366  cssbn  25428  rrxcph  25445  minveclem2  25479  pjthlem1  25490  pjthlem2  25491  ivthicc  25512  ovollecl  25537  ovolunlem1a  25550  ovolunnul  25554  ovoliunlem1  25556  ismbl2  25581  nulmbl2  25590  unmbl  25591  volun  25599  voliunlem2  25605  ioombl1lem2  25613  uniioombllem2a  25636  uniioombllem3  25639  uniioombllem4  25640  dyaddisjlem  25649  dyadmaxlem  25651  opnmbllem  25655  volsup2  25659  volcn  25660  ismbfd  25693  mbfi1fseqlem1  25770  mbfi1fseqlem5  25774  itg2lecl  25793  itg2monolem2  25806  itg2gt0  25815  itgspliticc  25892  ellimc3  25934  limcres  25941  dvfval  25952  dvres3  25968  dvres3a  25969  dvmptresicc  25971  dvnff  25979  dvnadd  25985  dvn2bss  25986  dvnres  25987  dvcmul  26001  dvcmulf  26002  dvmptres3  26014  dvmptres2  26020  dvmptntr  26029  dvexp3  26036  dvferm1lem  26042  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  dvgt0lem2  26062  dvne0  26070  lhop1lem  26072  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1lem6  26102  ftc1  26103  ftc2ditglem  26106  itgsubstlem  26109  itgpowd  26111  tdeglem4  26119  mdegaddle  26133  mdegmullem  26137  ply1rem  26225  fta1glem2  26228  fta1blem  26230  ig1peu  26234  ig1pdvds  26239  dgrmulc  26331  dgrcolem1  26333  plydivlem4  26356  plydiveu  26358  fta1lem  26367  vieta1lem1  26370  vieta1lem2  26371  plyexmo  26373  taylfvallem1  26416  taylfval  26418  tayl0  26421  taylplem1  26422  taylply2  26427  taylply2OLD  26428  taylply  26429  dvtaylp  26430  dvntaylp  26431  dvntaylp0  26432  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmcaulem  26455  ulmcau  26456  ulmcn  26460  ulmdvlem1  26461  radcnvlem1  26474  radcnvle  26481  psercn  26488  pserdvlem2  26490  pserdv  26491  abelth  26503  tanregt0  26599  dvlog2lem  26712  efopn  26718  logtayllem  26719  logccv  26723  cxplt3  26760  cxpmul2zd  26776  cxpltd  26779  cxpled  26780  cxplt3d  26795  cxple3d  26796  dvsqrt  26802  cxpcn3  26809  cxpaddle  26813  cxpeq  26818  angcan  26863  angvald  26865  ang180lem2  26871  ang180  26875  isosctrlem3  26881  dquartlem1  26912  atantayl2  26999  leibpi  27003  log2tlbnd  27006  birthdaylem3  27014  xrlimcnp  27029  efrlim  27030  efrlimOLD  27031  o1cxp  27036  jensenlem2  27049  jensen  27050  fsumharmonic  27073  lgamucov  27099  lgamcvg2  27116  wilthlem1  27129  basellem3  27144  basellem6  27147  basellem8  27149  ppisval  27165  chtwordi  27217  ppiwordi  27223  mumullem2  27241  mpodvdsmulf1o  27255  dvdsmulf1o  27257  fsumvma  27275  fsumvma2  27276  chpchtsum  27281  chpub  27282  logfacubnd  27283  dchrmulcl  27311  dchrinv  27323  dchrptlem1  27326  dchrptlem2  27327  sumdchr2  27332  dchr2sum  27335  bposlem7  27352  lgslem1  27359  lgslem3  27361  lgsdirprm  27393  lgsqrlem2  27409  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem4  27440  lgseisen  27441  lgsquadlem1  27442  lgsquad2lem1  27446  lgsquad3  27449  m1lgs  27450  2sqlem7  27486  2sq2  27495  2sqmod  27498  chebbnd1lem2  27532  chebbnd1lem3  27533  rplogsumlem1  27546  rpvmasumlem  27549  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasumlema  27562  dchrisum0flblem2  27571  dchrisum0fno1  27573  dchrisum0re  27575  logdivsum  27595  pntrsumbnd2  27629  pntpbnd1a  27647  pntpbnd1  27648  pntibndlem2  27653  pntlemr  27664  pntlemj  27665  pntlemf  27667  pnt2  27675  padicabv  27692  ostth2lem2  27696  sltrec  27883  madebday  27956  sltn0  27961  addsproplem6  28025  sleadd1  28040  negsproplem6  28083  mulsproplem13  28172  mulsproplem14  28173  sltmuld  28181  mulsgt0d  28189  halfcut  28434  f1otrg  28897  brbtwn2  28938  colinearalglem2  28940  axcgrtr  28948  axcgrid  28949  axsegconlem7  28956  axsegcon  28960  ax5seglem3  28964  ax5seglem6  28967  ax5seg  28971  axpaschlem  28973  axlowdimlem17  28991  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  ecgrtg  29016  usgredg2v  29262  vtxdgoddnumeven  29589  2trlond  29972  eupthp1  30248  nmobndi  30807  ubthlem2  30903  ubthlem3  30904  minvecolem2  30907  shuni  31332  pjhthlem1  31423  chscllem2  31670  pjcompi  31704  mayete3i  31760  unoplin  31952  hmoplin  31974  nmophmi  32063  mdslmd4i  32365  isoun  32713  submuladdd  32753  xrge0addcld  32769  xrofsup  32774  eliccelico  32782  elicoelioo  32783  difioo  32787  rexdiv  32890  mgcmnt1d  32970  mgcmnt2d  32971  chnub  32984  xrge0addgt0  33003  omndadd2d  33058  omndadd2rd  33059  omndmul2  33062  cycpmcl  33109  cycpm2tr  33112  cyc3evpm  33143  cycpmconjslem2  33148  fldgensdrg  33281  ofldchr  33309  qusker  33342  eqgvscpbl  33343  ringlsmss1  33389  ringlsmss2  33390  lidlmcld  33412  intlidl  33413  lidlunitel  33416  elrspunidl  33421  idlinsubrg  33424  isprmidlc  33440  rhmpreimaprmidl  33444  qsidomlem1  33445  ssdifidllem  33449  mxidlmaxv  33461  mxidlprm  33463  ssmxidllem  33466  opprmxidlabs  33480  qsdrnglem2  33489  resssra  33602  ply1degltdimlem  33635  lindsunlem  33637  finexttrb  33675  fldgenfldext  33678  algextdeglem4  33711  algextdeglem8  33715  mdetpmtr2  33770  mdetpmtr12  33771  madjusmdetlem1  33773  madjusmdetlem4  33776  rhmpreimacn  33831  unitdivcld  33847  xrge0mulc1cn  33887  qqhnm  33936  esumcst  34027  esumfsup  34034  esumpmono  34043  esumcvg  34050  difelsiga  34097  sigapisys  34119  sigapildsys  34126  ldgenpisyslem1  34127  1stmbfm  34225  2ndmbfm  34226  dya2icoseg  34242  sibfinima  34304  probmeasb  34395  orvcgteel  34432  orvclteel  34437  ballotlemsima  34480  ballotlemfrceq  34493  sgnmul  34507  ccatmulgnn0dir  34519  fct2relem  34574  ftc2re  34575  chtvalz  34606  subfacp1lem2a  35148  subfaclim  35156  erdsze2lem2  35172  cvmliftlem2  35254  cvmliftlem10  35262  cvmliftlem13  35264  cvmliftiota  35269  cvmlift2lem9  35279  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmliftphtlem  35285  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  snmlff  35297  mrsubfval  35476  wzel  35788  wsuclem  35789  brsegle  36072  opnregcld  36296  weiunfrlem  36430  fin2so  37567  poimirlem17  37597  poimirlem23  37603  opnmbllem0  37616  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  itg2addnc  37634  itg2gt0cn  37635  ftc1cnnclem  37651  ftc1cnnc  37652  areacirclem5  37672  indexdom  37694  sstotbnd2  37734  isbnd3  37744  isbnd3b  37745  cntotbnd  37756  ismtyima  37763  heibor1lem  37769  heiborlem8  37778  rrncmslem  37792  reheibor  37799  lkrlsp  39058  lshpkrlem5  39070  ldualssvscl  39114  ldualssvsubcl  39115  llnmlplnN  39496  llncvrlpln  39515  pmapjat1  39810  pclfinN  39857  lautlt  40048  lauteq  40052  lautco  40054  ltrn11  40083  ltrnle  40086  ltrneq2  40105  cdlemednuN  40257  cdleme20k  40276  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21c  40284  cdleme22e  40301  cdleme22eALTN  40302  cdlemefrs32fva  40357  cdlemg4g  40573  cdlemg18b  40636  cdlemg18c  40637  cdlemj3  40780  dia2dimlem5  41025  dvhopN  41073  cdlemm10N  41075  dihjatcclem4  41378  dochexmidlem2  41418  lclkrlem2o  41478  lcfrlem5  41503  lcfrlem6  41504  lcdlssvscl  41563  mapdpglem6  41635  mapdpglem9  41637  mapdpglem12  41640  mapdpglem14  41642  mapdindp0  41676  hdmaprnlem7N  41812  hdmaprnlem8N  41813  hdmaprnlem3eN  41815  hgmapvvlem3  41882  addinvcom  42407  evlsaddval  42523  evlsmulval  42524  evladdval  42530  evlmulval  42531  mzpsubst  42704  eldioph2lem1  42716  eldioph2lem2  42717  eldioph2b  42719  diophin  42728  irrapxlem2  42779  irrapxlem4  42781  irrapxlem5  42782  pellexlem1  42785  pellexlem2  42786  pellexlem6  42790  elpell1qr2  42828  pell1qrgaplem  42829  pell1qrgap  42830  pellqrex  42835  pellfundex  42842  pellfund14  42854  rmspecsqrtnq  42862  rmxyadd  42878  congsub  42927  mzpcong  42929  congrep  42930  acongtr  42935  acongrep  42937  jm2.19lem1  42946  jm2.22  42952  jm2.23  42953  jm2.26lem3  42958  jm2.26  42959  jm2.27a  42962  fnwe2lem2  43008  aomclem6  43016  hbtlem2  43081  hbtlem4  43083  hbtlem5  43085  dgraa0p  43106  rngunsnply  43130  proot1hash  43156  nnoeomeqom  43274  cantnf2  43287  omabs2  43294  naddcnff  43324  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  expgrowth  44304  fpmd  45173  abslt2sqd  45275  ioondisj2  45411  ioondisj1  45412  eliocre  45427  ioossioobi  45435  iooiinicc  45460  iooiinioc  45474  icossico2  45482  lptioo2  45552  limcresiooub  45563  limsupequzlem  45643  xlimmnfvlem2  45754  xlimpnfvlem2  45758  cncfuni  45807  cncfiooicclem1  45814  cxpcncf2  45820  dvcnre  45837  dvresntr  45839  dvresioo  45842  dvbdfbdioolem1  45849  dvnmptdivc  45859  dvnxpaek  45863  itgsinexplem1  45875  itgcoscmulx  45890  itgiccshift  45901  itgperiod  45902  ovolsplit  45909  stoweidlem11  45932  stoweidlem26  45947  stoweidlem34  45955  stoweidlem36  45957  stoweidlem38  45959  stirlinglem5  45999  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem20  46048  fourierdlem58  46085  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem79  46106  fourierdlem80  46107  fourierdlem87  46114  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem113  46140  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem46  46201  etransclem47  46202  rrndistlt  46211  rrnprjdstle  46222  ioorrnopnxrlem  46227  sge0ssre  46318  sge0seq  46367  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidifhspdmvle  46541  hoiqssbllem2  46544  ovolval5lem2  46574  iinhoiicc  46595  iunhoiioo  46597  vonioolem2  46602  vonicclem2  46605  issmflem  46648  iccpartdisj  47311  m1expevenALTV  47521  fpprel2  47615  tgoldbach  47691  opstrgric  47779  nn0eo  48262  fdivpm  48277  refdivpm  48278  elbigolo1  48291  logbpw2m1  48301  fllog2  48302  dignn0flhalflem1  48349  dignn0flhalflem2  48350  itsclinecirc0in  48509  2itscplem2  48513  itscnhlinecirc02plem1  48516  iccdisj2  48577