Theorem syl22anc 826

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  preqsnd  4657  fr2nr  5378  soltmin  5830  f1oprg  6482  f1prex  6859  fveqf1o  6877  weniso  6924  fr3nr  7304  suppofssd  7663  smogt  7801  smorndom  7802  oacomf1o  7984  difsnen  8387  undom  8393  enfixsn  8414  domss2  8464  ssenen  8479  marypha1lem  8684  fisupcl  8720  ordtypelem3  8771  ordtypelem8  8776  oieu  8790  oismo  8791  wofib  8796  wemaplem2  8798  wemapso  8802  wemapso2lem  8803  unxpwdom2  8839  infdifsn  8906  oemapvali  8933  cantnflem1c  8936  cantnflem1  8938  cantnf  8942  cnfcom3  8953  r1ordg  8993  dif1card  9222  infxpenlem  9225  dfac8clem  9244  cdadju  9382  infxp  9427  infmap2  9430  cflim2  9475  coftr  9485  fin2i2  9530  enfin2i  9533  fin23lem26  9537  fin23lem27  9540  fin23lem40  9563  isf32lem2  9566  isf32lem3  9567  isf32lem4  9568  isf32lem7  9571  isf32lem9  9573  fin1a2lem13  9624  fin12  9625  alephexp1  9791  gchdomtri  9841  fpwwe2lem12  9853  fpwwe2lem13  9854  gchpwdom  9882  gchhar  9891  adderpqlem  10166  mulerpqlem  10167  addassnq  10170  mulassnq  10171  distrnq  10173  mulidnq  10175  recmulnq  10176  ltexnq  10187  distrlem1pr  10237  distrlem4pr  10238  prlem936  10259  reclem3pr  10261  mulcmpblnr  10283  mulgt0d  10587  mul4d  10644  add4d  10660  add42d  10661  subcan  10734  addsub4d  10837  subadd4d  10838  sub4d  10839  2addsubd  10840  addsubeq4d  10841  muladdd  10891  mulsubd  10892  addgegt0d  11006  addgtge0d  11007  addge0d  11009  mulge0d  11010  le2addd  11052  le2subd  11053  ltleaddd  11054  leltaddd  11055  lt2subd  11057  divdivdiv  11134  divcan5  11135  divne0d  11225  recdivd  11226  recdiv2d  11227  divcan6d  11228  ddcand  11229  rec11d  11230  divmuldivd  11250  divmul13d  11251  divmul24d  11252  divadddivd  11253  divsubdivd  11254  divmuleqd  11255  divdivdivd  11256  subrecd  11264  mulge0b  11303  recreclt  11332  divgt0d  11368  mulgt1d  11369  lemulge11d  11370  lemulge12d  11371  ltmul12ad  11374  lemul12ad  11375  lemul12bd  11376  supmul1  11403  nndivtr  11480  qreccl  12176  ledivdivd  12266  lediv12ad  12300  lt2mul2divd  12310  xlt2add  12462  supxrun  12518  supxrre  12529  infxrre  12538  elicore  12598  iccss2  12616  iccssico2  12619  lincmb01cmp  12690  iccf1o  12691  fzrev2i  12781  2tnp1ge0ge0  13007  m1modnnsub1  13093  modaddmodup  13110  modaddmodlo  13111  modsubdir  13116  fzennn  13144  sermono  13210  mulexpz  13277  expaddz  13281  sqdiv  13295  expsubd  13329  ltexp2a  13338  expmordi  13339  leexp2a  13344  expmulnbnd  13404  digit1  13406  lt2sqd  13427  le2sqd  13428  sq11d  13429  bcm1k  13483  bcp1n  13484  bcp1nk  13485  hashf1lem1  13616  cshw1  14036  2swrd2eqwrdeq  14167  2swrd2eqwrdeqOLD  14168  ofccat  14180  absrele  14519  sqreulem  14570  sqrtmuld  14635  sqrtsq2d  14636  sqrtled  14637  sqrtltd  14638  sqr11d  14639  abs3lemd  14672  rlimuni  14758  climuni  14760  lo1resb  14772  o1resb  14774  2clim  14780  addcn2  14801  mulcn2  14803  o1of2  14820  o1rlimmul  14826  lo1add  14834  lo1mul  14835  isercolllem1  14872  caucvgrlem  14880  iseraltlem2  14890  iseraltlem3  14891  mptfzshft  14983  fsumrev  14984  fsum0diag2  14988  binomlem  15034  climcndslem1  15054  climcndslem2  15055  harmonic  15064  mertenslem1  15090  fprodser  15153  fprodrev  15181  efcllem  15281  moddvds  15468  dvds1  15519  dvdsext  15521  evennn2n  15550  bitsinv1  15641  sadaddlem  15665  sadasslem  15669  sadeq  15671  mulgcd  15742  dvdssqlem  15756  lcmftp  15826  rpmulgcd2  15846  coprmproddvdslem  15852  isprm5  15897  isprm6  15904  crth  15961  eulerthlem2  15965  prmdiveq  15969  pythagtriplem11  16008  pythagtriplem13  16010  pcgcd1  16059  pcprmpw2  16064  pcaddlem  16070  fldivp1  16079  4sqlem12  16138  4sqlem14  16140  4sqlem15  16141  4sqlem16  16142  vdwapun  16156  mreexexlem4d  16766  acsfn1  16780  acsfn2  16782  sscpwex  16933  rescabs  16951  yonedainv  17379  subm0  17814  pmtrfb  18344  psgnunilem1  18372  odmodnn0  18420  odeq  18430  dfod2  18442  sylow1lem1  18474  lsmsubg  18530  lsmmod  18549  lsmdisj2  18556  ghmplusg  18712  odadd  18716  gexexlem  18718  lt6abl  18759  cyggex2  18761  dprdfinv  18881  dmdprdsplitlem  18899  dpjidcl  18920  ablfacrp  18928  ablfacrp2  18929  ablfac1c  18933  ablfac1eu  18935  acsfn1p  19290  lcomfsupp  19386  lssvancl1  19428  lssvnegcl  19440  lspprvacl  19483  lspsneli  19485  lspsn  19486  lmhmplusg  19528  lmhmima  19531  lmhmpreima  19532  reslmhm  19536  lbsind2  19565  lsmcl  19567  lsmelval2  19569  lsppreli  19574  lspprabs  19579  pj1lmhm  19584  lssvs0or  19594  lspabs3  19605  lspfixed  19612  lspexch  19613  lsmcv  19625  lspsolv  19627  lidlmcl  19701  drngnidl  19713  2idlcpbl  19718  mplbas2  19954  evlslem3  19997  evlslem1  19998  coe1addfv  20126  lply1binom  20167  evl1addd  20196  evl1subd  20197  evl1muld  20198  gzrngunit  20303  zringlpirlem3  20325  prmirredlem  20332  znf1o  20390  znunithash  20403  frlmsubgval  20601  frlmvplusgvalc  20603  frlmvscaval  20604  frlmphllem  20616  frlmphl  20617  frlmssuvc1  20630  frlmsslsp  20632  frlmup1  20634  frlmup2  20635  lindfind2  20654  lindfrn  20657  f1lindf  20658  islindf4  20674  mamudi  20706  mamudir  20707  1marepvmarrepid  20878  mdetrlin  20905  smadiadetglem1  20974  smadiadetg  20976  cramerimplem1  20986  mat2pmatscmxcl  21042  m2pmfzgsumcl  21050  pmatcollpw  21083  pmatcollpwfi  21084  pmatcollpw3fi1lem1  21088  cpmidpmatlem2  21173  cpmadugsumlemF  21178  chcoeffeqlem  21187  ntrin  21363  topssnei  21426  restbas  21460  restntr  21484  cnntri  21573  fiuncmp  21706  nllyrest  21788  nllyidm  21791  hausllycmp  21796  cldllycmp  21797  hauspwdom  21803  txcld  21905  txcn  21928  txlly  21938  txnlly  21939  txhaus  21949  txlm  21950  txkgen  21954  xkococnlem  21961  cnmpt2res  21979  xkoinjcn  21989  basqtop  22013  qtopeu  22018  trfbas2  22145  neifil  22182  hausflim  22283  alexsubALTlem2  22350  cnextfval  22364  cnextfvval  22367  cnextf  22368  cnextfres  22371  clssubg  22410  utop2nei  22552  utop3cls  22553  utopreg  22554  psmetlecl  22618  xmetlecl  22649  prdsxmetlem  22671  bldisj  22701  imasf1obl  22791  prdsbl  22794  stdbdmet  22819  stdbdmopn  22821  met2ndci  22825  metcnp  22844  metustto  22856  metustexhalf  22859  cfilucfil  22862  metucn  22874  lssnlm  23003  nmotri  23041  nmoid  23044  tgioo  23097  blcvx  23099  xrsmopn  23113  reperflem  23119  reconnlem2  23128  opnreen  23132  metdsge  23150  metdsre  23154  metdscnlem  23156  metnrmlem1a  23159  metnrmlem1  23160  metnrmlem3  23162  cncfmet  23209  cnmpopc  23225  icopnfcnv  23239  icopnfhmeo  23240  cnllycmp  23253  evth  23256  lebnumii  23263  nmoleub2lem3  23412  iscfil2  23562  cfil3i  23565  iscfil3  23569  cfilfcls  23570  iscau3  23574  iscmet3lem2  23588  caubl  23604  lmcau  23609  cssbn  23671  rrxcph  23688  minveclem2  23722  pjthlem1  23733  pjthlem2  23734  ivthicc  23752  ovollecl  23777  ovolunlem1a  23790  ovolunnul  23794  ovoliunlem1  23796  ismbl2  23821  nulmbl2  23830  unmbl  23831  volun  23839  voliunlem2  23845  ioombl1lem2  23853  uniioombllem2a  23876  uniioombllem3  23879  uniioombllem4  23880  dyaddisjlem  23889  dyadmaxlem  23891  opnmbllem  23895  volsup2  23899  volcn  23900  ismbfd  23933  mbfi1fseqlem1  24009  mbfi1fseqlem5  24013  itg2lecl  24032  itg2monolem2  24045  itg2gt0  24054  itgspliticc  24130  ellimc3  24170  limcres  24177  dvfval  24188  dvres3  24204  dvres3a  24205  dvnff  24213  dvnadd  24219  dvn2bss  24220  dvnres  24221  dvcmul  24234  dvcmulf  24235  dvmptres3  24246  dvmptres2  24252  dvmptntr  24261  dvexp3  24268  dvferm1lem  24274  dvlip  24283  dvlipcn  24284  dvlip2  24285  c1liplem1  24286  dvgt0lem1  24292  dvgt0lem2  24293  dvne0  24301  lhop1lem  24303  lhop2  24305  lhop  24306  dvcnvrelem1  24307  dvcnvrelem2  24308  dvcvx  24310  dvfsumle  24311  dvfsumabs  24313  dvfsumlem2  24317  ftc1lem6  24331  ftc1  24332  ftc2ditglem  24335  itgsubstlem  24338  tdeglem4  24347  mdegaddle  24361  mdegmullem  24365  ply1rem  24450  fta1glem2  24453  fta1blem  24455  ig1peu  24458  ig1pdvds  24463  dgrmulc  24554  dgrcolem1  24556  plydivlem4  24578  plydiveu  24580  fta1lem  24589  vieta1lem1  24592  vieta1lem2  24593  plyexmo  24595  taylfvallem1  24638  taylfval  24640  tayl0  24643  taylplem1  24644  taylply2  24649  taylply  24650  dvtaylp  24651  dvntaylp  24652  dvntaylp0  24653  taylthlem1  24654  taylthlem2  24655  ulmcaulem  24675  ulmcau  24676  ulmcn  24680  ulmdvlem1  24681  radcnvlem1  24694  radcnvle  24701  psercn  24707  pserdvlem2  24709  pserdv  24710  abelth  24722  tanregt0  24814  dvlog2lem  24926  efopn  24932  logtayllem  24933  logccv  24937  cxplt3  24974  cxpmul2zd  24990  cxpltd  24993  cxpled  24994  cxplt3d  25008  cxple3d  25009  dvsqrt  25014  cxpcn3  25020  cxpaddle  25024  cxpeq  25029  angcan  25071  angvald  25073  ang180lem2  25079  ang180  25083  isosctrlem3  25089  dquartlem1  25120  atantayl2  25207  leibpilem1OLD  25210  leibpi  25212  log2tlbnd  25215  birthdaylem3  25223  xrlimcnp  25238  efrlim  25239  o1cxp  25244  jensenlem2  25257  jensen  25258  fsumharmonic  25281  lgamucov  25307  lgamcvg2  25324  wilthlem1  25337  basellem3  25352  basellem6  25355  basellem8  25357  ppisval  25373  chtwordi  25425  ppiwordi  25431  mumullem2  25449  dvdsmulf1o  25463  fsumvma  25481  fsumvma2  25482  chpchtsum  25487  chpub  25488  logfacubnd  25489  dchrmulcl  25517  dchrinv  25529  dchrptlem1  25532  dchrptlem2  25533  sumdchr2  25538  dchr2sum  25541  bposlem7  25558  lgslem1  25565  lgslem3  25567  lgsdirprm  25599  lgsqrlem2  25615  lgseisenlem1  25643  lgseisenlem2  25644  lgseisenlem4  25646  lgseisen  25647  lgsquadlem1  25648  lgsquad2lem1  25652  lgsquad3  25655  m1lgs  25656  2sqlem7  25692  2sq2  25701  2sqmod  25704  chebbnd1lem2  25738  chebbnd1lem3  25739  rplogsumlem1  25752  rpvmasumlem  25755  dchrvmasumlem1  25763  dchrvmasum2lem  25764  dchrvmasumlema  25768  dchrisum0flblem2  25777  dchrisum0fno1  25779  dchrisum0re  25781  logdivsum  25801  pntrsumbnd2  25835  pntpbnd1a  25853  pntpbnd1  25854  pntibndlem2  25859  pntlemr  25870  pntlemj  25871  pntlemf  25873  pnt2  25881  padicabv  25898  ostth2lem2  25902  f1otrg  26350  brbtwn2  26384  colinearalglem2  26386  axcgrtr  26394  axcgrid  26395  axsegconlem7  26402  axsegcon  26406  ax5seglem3  26410  ax5seglem6  26413  ax5seg  26417  axpaschlem  26419  axlowdimlem17  26437  axcontlem2  26444  axcontlem4  26446  axcontlem7  26449  axcontlem8  26450  ecgrtg  26462  usgredg2v  26702  vtxdgoddnumeven  27028  2trlond  27435  clwwlknonex2  27627  eupthp1  27736  nmobndi  28319  ubthlem2  28416  ubthlem3  28417  minvecolem2  28420  shuni  28848  pjhthlem1  28939  chscllem2  29186  pjcompi  29220  mayete3i  29276  unoplin  29468  hmoplin  29490  nmophmi  29579  mdslmd4i  29881  isoun  30178  xrge0addcld  30227  xrofsup  30233  eliccelico  30241  elicoelioo  30242  difioo  30246  rexdiv  30337  xrge0addgt0  30388  omndadd2d  30405  omndadd2rd  30406  omndmul2  30409  freshmansdream  30494  ofldchr  30522  qusker  30553  eqgvscpbl  30554  lindsunlem  30605  finexttrb  30637  mdetpmtr2  30688  mdetpmtr12  30689  madjusmdetlem1  30691  madjusmdetlem4  30694  unitdivcld  30745  xrge0mulc1cn  30785  qqhnm  30832  esumcst  30923  esumfsup  30930  esumpmono  30939  esumcvg  30946  difelsiga  30994  sigapisys  31016  sigapildsys  31023  ldgenpisyslem1  31024  1stmbfm  31120  2ndmbfm  31121  dya2icoseg  31137  sibfinima  31199  probmeasb  31291  orvcgteel  31328  orvclteel  31333  ballotlemsima  31376  ballotlemfrceq  31389  sgnmul  31403  ccatmulgnn0dir  31419  fct2relem  31477  ftc2re  31478  chtvalz  31509  subfacp1lem2a  31972  subfaclim  31980  erdsze2lem2  31996  cvmliftlem2  32078  cvmliftlem10  32086  cvmliftlem13  32088  cvmliftiota  32093  cvmlift2lem9  32103  cvmlift2lem11  32105  cvmlift2lem12  32106  cvmliftphtlem  32109  cvmlift3lem6  32116  cvmlift3lem7  32117  cvmlift3lem9  32119  snmlff  32121  mrsubfval  32215  trpredelss  32532  trpredpo  32535  wzel  32572  wsuclem  32573  sltrec  32739  brsegle  33030  opnregcld  33139  fin2so  34268  poimirlem17  34298  poimirlem23  34304  opnmbllem0  34317  mblfinlem3  34320  mblfinlem4  34321  itg2addnclem  34332  itg2addnc  34335  itg2gt0cn  34336  ftc1cnnclem  34354  ftc1cnnc  34355  areacirclem5  34375  indexdom  34399  sstotbnd2  34442  isbnd3  34452  isbnd3b  34453  cntotbnd  34464  ismtyima  34471  heibor1lem  34477  heiborlem8  34486  rrncmslem  34500  reheibor  34507  lkrlsp  35631  lshpkrlem5  35643  ldualssvscl  35687  ldualssvsubcl  35688  llnmlplnN  36068  llncvrlpln  36087  pmapjat1  36382  pclfinN  36429  lautlt  36620  lauteq  36624  lautco  36626  ltrn11  36655  ltrnle  36658  ltrneq2  36677  cdlemednuN  36829  cdleme20k  36848  cdleme20l2  36850  cdleme20l  36851  cdleme20m  36852  cdleme21c  36856  cdleme22e  36873  cdleme22eALTN  36874  cdlemefrs32fva  36929  cdlemg4g  37145  cdlemg18b  37208  cdlemg18c  37209  cdlemj3  37352  dia2dimlem5  37597  dvhopN  37645  cdlemm10N  37647  dihjatcclem4  37950  dochexmidlem2  37990  lclkrlem2o  38050  lcfrlem5  38075  lcfrlem6  38076  lcdlssvscl  38135  mapdpglem6  38207  mapdpglem9  38209  mapdpglem12  38212  mapdpglem14  38214  mapdindp0  38248  hdmaprnlem7N  38384  hdmaprnlem8N  38385  hdmaprnlem3eN  38387  hgmapvvlem3  38454  mzpsubst  38685  eldioph2lem1  38697  eldioph2lem2  38698  eldioph2b  38700  diophin  38710  irrapxlem2  38761  irrapxlem4  38763  irrapxlem5  38764  pellexlem1  38767  pellexlem2  38768  pellexlem6  38772  elpell1qr2  38810  pell1qrgaplem  38811  pell1qrgap  38812  pellqrex  38817  pellfundex  38824  pellfund14  38836  rmspecsqrtnq  38844  rmxyadd  38859  congsub  38908  mzpcong  38910  congrep  38911  acongtr  38916  acongrep  38918  jm2.19lem1  38927  jm2.22  38933  jm2.23  38934  jm2.26lem3  38939  jm2.26  38940  jm2.27a  38943  fnwe2lem2  38992  aomclem6  39000  hbtlem2  39065  hbtlem4  39067  hbtlem5  39069  dgraa0p  39090  rngunsnply  39114  proot1hash  39141  itgpowd  39162  enpr2d  39874  expgrowth  40027  fpmd  40913  abslt2sqd  41003  ioondisj2  41144  ioondisj1  41145  eliocre  41162  ioossioobi  41170  iooiinicc  41195  iooiinioc  41209  icossico2  41217  lptioo2  41289  limcresiooub  41300  limsupequzlem  41380  xlimmnfvlem2  41491  xlimpnfvlem2  41495  cncfuni  41545  cncfiooicclem1  41552  cxpcncf2  41559  dvcnre  41576  dvresntr  41578  dvmptresicc  41580  dvresioo  41582  dvbdfbdioolem1  41589  dvnmptdivc  41599  dvnxpaek  41603  itgsinexplem1  41615  itgcoscmulx  41630  itgiccshift  41641  itgperiod  41642  ovolsplit  41650  stoweidlem11  41673  stoweidlem26  41688  stoweidlem34  41696  stoweidlem36  41698  stoweidlem38  41700  stirlinglem5  41740  dirkercncflem2  41766  dirkercncflem4  41768  fourierdlem20  41789  fourierdlem58  41826  fourierdlem72  41840  fourierdlem73  41841  fourierdlem74  41842  fourierdlem75  41843  fourierdlem76  41844  fourierdlem79  41847  fourierdlem80  41848  fourierdlem87  41855  fourierdlem94  41862  fourierdlem103  41871  fourierdlem104  41872  fourierdlem107  41875  fourierdlem113  41881  sqwvfoura  41890  sqwvfourb  41891  fourierswlem  41892  fouriersw  41893  etransclem46  41942  etransclem47  41943  rrndistlt  41952  rrnprjdstle  41963  ioorrnopnxrlem  41968  sge0ssre  42056  sge0seq  42105  hsphoidmvle2  42244  hsphoidmvle  42245  hoidmv1lelem1  42250  hoidmv1lelem2  42251  hoidmv1lelem3  42252  hoidmvlelem1  42254  hoidifhspdmvle  42279  hoiqssbllem2  42282  ovolval5lem2  42312  iinhoiicc  42333  iunhoiioo  42335  vonioolem2  42340  vonicclem2  42343  issmflem  42381  iccpartdisj  42915  m1expevenALTV  43120  fpprel2  43214  tgoldbach  43290  strisomgrop  43313  nn0eo  43896  fdivpm  43911  refdivpm  43912  elbigolo1  43925  logbpw2m1  43935  fllog2  43936  dignn0flhalflem1  43983  dignn0flhalflem2  43984  itsclinecirc0in  44070  2itscplem2  44074  itscnhlinecirc02plem1  44077