Theorem syl22anc 837

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  preqsnd  4814  fr2nr  5609  soltmin  6088  f1oprg  6826  f1prex  7226  fveqf1o  7245  weniso  7295  fr3nr  7702  suppofssd  8130  smogt  8309  smocdmdom  8310  oacomf1o  8508  en2prd  8988  enpr2dOLD  8990  difsnen  8993  undomOLD  9000  enfixsn  9021  domss2  9076  ssenen  9091  marypha1lem  9365  fisupcl  9401  ordtypelem3  9452  ordtypelem8  9457  oieu  9471  oismo  9472  wofib  9477  wemaplem2  9479  wemapso  9483  wemapso2lem  9484  unxpwdom2  9520  infdifsn  9589  oemapvali  9616  cantnflem1c  9619  cantnflem1  9621  cantnf  9625  cnfcom3  9636  r1ordg  9710  dif1card  9942  infxpenlem  9945  dfac8clem  9964  infxp  10147  infmap2  10150  cflim2  10195  coftr  10205  fin2i2  10250  enfin2i  10253  fin23lem26  10257  fin23lem27  10260  fin23lem40  10283  isf32lem2  10286  isf32lem3  10287  isf32lem4  10288  isf32lem7  10291  isf32lem9  10293  fin1a2lem13  10344  fin12  10345  alephexp1  10511  gchdomtri  10561  fpwwe2lem11  10573  fpwwe2lem12  10574  gchpwdom  10602  gchhar  10611  adderpqlem  10886  mulerpqlem  10887  addassnq  10890  mulassnq  10891  distrnq  10893  mulidnq  10895  recmulnq  10896  ltexnq  10907  distrlem1pr  10957  distrlem4pr  10958  prlem936  10979  reclem3pr  10981  mulcmpblnr  11003  mulgt0d  11306  mul4d  11363  add4d  11379  add42d  11380  subcan  11452  addsub4d  11555  subadd4d  11556  sub4d  11557  2addsubd  11558  addsubeq4d  11559  muladdd  11609  mulsubd  11610  addgegt0d  11724  addgtge0d  11725  addge0d  11727  mulge0d  11728  le2addd  11770  le2subd  11771  ltleaddd  11772  leltaddd  11773  lt2subd  11775  divdivdiv  11852  divcan5  11853  divne0d  11943  recdivd  11944  recdiv2d  11945  divcan6d  11946  ddcand  11947  rec11d  11948  divmuldivd  11968  divmul13d  11969  divmul24d  11970  divadddivd  11971  divsubdivd  11972  divmuleqd  11973  divdivdivd  11974  subrecd  11982  mulge0b  12021  recreclt  12050  divgt0d  12086  mulgt1d  12087  lemulge11d  12088  lemulge12d  12089  ltmul12ad  12092  lemul12ad  12093  lemul12bd  12094  supmul1  12120  nndivtr  12196  qreccl  12886  ledivdivd  12974  lediv12ad  13008  lt2mul2divd  13018  xlt2add  13171  supxrun  13227  supxrre  13238  infxrre  13247  elicore  13308  iccss2  13327  iccssico2  13330  lincmb01cmp  13404  iccf1o  13405  fzrev2i  13498  2tnp1ge0ge0  13726  m1modnnsub1  13814  modaddmodup  13831  modaddmodlo  13832  modsubdir  13837  fzennn  13865  sermono  13932  mulexpz  14000  expaddz  14004  sqdiv  14018  expsubd  14054  ltexp2a  14063  expmordi  14064  leexp2a  14069  expmulnbnd  14130  digit1  14132  lt2sqd  14151  le2sqd  14152  sq11d  14153  bcm1k  14207  bcp1n  14208  bcp1nk  14209  hashf1lem1  14345  hashf1lem1OLD  14346  cshw1  14702  2swrd2eqwrdeq  14834  ofccat  14846  absrele  15185  sqreulem  15236  sqrtmuld  15301  sqrtsq2d  15302  sqrtled  15303  sqrtltd  15304  sqr11d  15305  abs3lemd  15338  rlimuni  15424  climuni  15426  lo1resb  15438  o1resb  15440  2clim  15446  addcn2  15468  mulcn2  15470  o1of2  15487  o1rlimmul  15493  lo1add  15501  lo1mul  15502  isercolllem1  15541  caucvgrlem  15549  iseraltlem2  15559  iseraltlem3  15560  mptfzshft  15655  fsumrev  15656  fsum0diag2  15660  binomlem  15706  climcndslem1  15726  climcndslem2  15727  harmonic  15736  mertenslem1  15761  fprodser  15824  fprodrev  15852  efcllem  15952  moddvds  16139  dvds1  16193  dvdsext  16195  evennn2n  16225  bitsinv1  16314  sadaddlem  16338  sadasslem  16342  sadeq  16344  mulgcd  16421  dvdssqlem  16434  lcmftp  16504  rpmulgcd2  16524  coprmproddvdslem  16530  isprm5  16575  isprm6  16582  crth  16642  eulerthlem2  16646  prmdiveq  16650  pythagtriplem11  16689  pythagtriplem13  16691  pcgcd1  16741  pcprmpw2  16746  pcaddlem  16752  fldivp1  16761  4sqlem12  16820  4sqlem14  16822  4sqlem15  16823  4sqlem16  16824  vdwapun  16838  mreexexlem4d  17519  acsfn1  17533  acsfn2  17535  sscpwex  17690  rescabs  17710  rescabsOLD  17711  yonedainv  18162  subm0  18618  pmtrfb  19238  psgnunilem1  19266  odmodnn0  19313  odeq  19323  dfod2  19337  sylow1lem1  19371  lsmsubg  19427  lsmmod  19448  lsmdisj2  19455  ghmplusg  19615  odadd  19619  gexexlem  19621  lt6abl  19663  cyggex2  19665  dprdfinv  19789  dmdprdsplitlem  19807  dpjidcl  19828  ablfacrp  19836  ablfacrp2  19837  ablfac1c  19841  ablfac1eu  19843  acsfn1p  20251  lcomfsupp  20347  lssvancl1  20390  lssvnegcl  20402  lspprvacl  20445  lspsneli  20447  lspsn  20448  lmhmplusg  20490  lmhmima  20493  lmhmpreima  20494  reslmhm  20498  lbsind2  20527  lsmcl  20529  lsmelval2  20531  lsppreli  20536  lspprabs  20541  pj1lmhm  20546  lssvs0or  20556  lspabs3  20567  lspfixed  20574  lspexch  20575  lsmcv  20587  lspsolv  20589  lidlmcl  20672  drngnidl  20684  2idlcpbl  20689  gzrngunit  20848  zringlpirlem3  20870  prmirredlem  20878  znf1o  20943  znunithash  20956  frlmsubgval  21156  frlmvplusgvalc  21158  frlmvscaval  21159  frlmphllem  21171  frlmphl  21172  frlmssuvc1  21185  frlmsslsp  21187  frlmup1  21189  frlmup2  21190  lindfind2  21209  lindfrn  21212  f1lindf  21213  islindf4  21229  mplbas2  21427  evlslem3  21474  evlslem1  21476  coe1addfv  21620  lply1binom  21661  evl1addd  21691  evl1subd  21692  evl1muld  21693  mamudi  21734  mamudir  21735  1marepvmarrepid  21908  mdetrlin  21935  smadiadetglem1  22004  smadiadetg  22006  cramerimplem1  22016  mat2pmatscmxcl  22073  m2pmfzgsumcl  22081  pmatcollpw  22114  pmatcollpwfi  22115  pmatcollpw3fi1lem1  22119  cpmidpmatlem2  22204  cpmadugsumlemF  22209  chcoeffeqlem  22218  ntrin  22396  topssnei  22459  restbas  22493  restntr  22517  cnntri  22606  fiuncmp  22739  nllyrest  22821  nllyidm  22824  hausllycmp  22829  cldllycmp  22830  hauspwdom  22836  txcld  22938  txcn  22961  txlly  22971  txnlly  22972  txhaus  22982  txlm  22983  txkgen  22987  xkococnlem  22994  cnmpt2res  23012  xkoinjcn  23022  basqtop  23046  qtopeu  23051  trfbas2  23178  neifil  23215  hausflim  23316  alexsubALTlem2  23383  cnextfval  23397  cnextfvval  23400  cnextf  23401  cnextfres  23404  clssubg  23444  utop2nei  23586  utop3cls  23587  utopreg  23588  psmetlecl  23652  xmetlecl  23683  prdsxmetlem  23705  bldisj  23735  imasf1obl  23828  prdsbl  23831  stdbdmet  23856  stdbdmopn  23858  met2ndci  23862  metcnp  23881  metustto  23893  metustexhalf  23896  cfilucfil  23899  metucn  23911  lssnlm  24049  nmotri  24087  nmoid  24090  tgioo  24143  blcvx  24145  xrsmopn  24159  reperflem  24165  reconnlem2  24174  opnreen  24178  metdsge  24196  metdsre  24200  metdscnlem  24202  metnrmlem1a  24205  metnrmlem1  24206  metnrmlem3  24208  cncfmet  24256  cnmpopc  24275  icopnfcnv  24289  icopnfhmeo  24290  cnllycmp  24303  evth  24306  lebnumii  24313  nmoleub2lem3  24462  iscfil2  24614  cfil3i  24617  iscfil3  24621  cfilfcls  24622  iscau3  24626  iscmet3lem2  24640  caubl  24656  lmcau  24661  cssbn  24723  rrxcph  24740  minveclem2  24774  pjthlem1  24785  pjthlem2  24786  ivthicc  24806  ovollecl  24831  ovolunlem1a  24844  ovolunnul  24848  ovoliunlem1  24850  ismbl2  24875  nulmbl2  24884  unmbl  24885  volun  24893  voliunlem2  24899  ioombl1lem2  24907  uniioombllem2a  24930  uniioombllem3  24933  uniioombllem4  24934  dyaddisjlem  24943  dyadmaxlem  24945  opnmbllem  24949  volsup2  24953  volcn  24954  ismbfd  24987  mbfi1fseqlem1  25064  mbfi1fseqlem5  25068  itg2lecl  25087  itg2monolem2  25100  itg2gt0  25109  itgspliticc  25185  ellimc3  25227  limcres  25234  dvfval  25245  dvres3  25261  dvres3a  25262  dvmptresicc  25264  dvnff  25271  dvnadd  25277  dvn2bss  25278  dvnres  25279  dvcmul  25292  dvcmulf  25293  dvmptres3  25304  dvmptres2  25310  dvmptntr  25319  dvexp3  25326  dvferm1lem  25332  dvlip  25341  dvlipcn  25342  dvlip2  25343  c1liplem1  25344  dvgt0lem1  25350  dvgt0lem2  25351  dvne0  25359  lhop1lem  25361  lhop2  25363  lhop  25364  dvcnvrelem1  25365  dvcnvrelem2  25366  dvcvx  25368  dvfsumle  25369  dvfsumabs  25371  dvfsumlem2  25375  ftc1lem6  25389  ftc1  25390  ftc2ditglem  25393  itgsubstlem  25396  itgpowd  25398  tdeglem4  25408  tdeglem4OLD  25409  mdegaddle  25423  mdegmullem  25427  ply1rem  25512  fta1glem2  25515  fta1blem  25517  ig1peu  25520  ig1pdvds  25525  dgrmulc  25616  dgrcolem1  25618  plydivlem4  25640  plydiveu  25642  fta1lem  25651  vieta1lem1  25654  vieta1lem2  25655  plyexmo  25657  taylfvallem1  25700  taylfval  25702  tayl0  25705  taylplem1  25706  taylply2  25711  taylply  25712  dvtaylp  25713  dvntaylp  25714  dvntaylp0  25715  taylthlem1  25716  taylthlem2  25717  ulmcaulem  25737  ulmcau  25738  ulmcn  25742  ulmdvlem1  25743  radcnvlem1  25756  radcnvle  25763  psercn  25769  pserdvlem2  25771  pserdv  25772  abelth  25784  tanregt0  25879  dvlog2lem  25991  efopn  25997  logtayllem  25998  logccv  26002  cxplt3  26039  cxpmul2zd  26055  cxpltd  26058  cxpled  26059  cxplt3d  26073  cxple3d  26074  dvsqrt  26079  cxpcn3  26085  cxpaddle  26089  cxpeq  26094  angcan  26136  angvald  26138  ang180lem2  26144  ang180  26148  isosctrlem3  26154  dquartlem1  26185  atantayl2  26272  leibpi  26276  log2tlbnd  26279  birthdaylem3  26287  xrlimcnp  26302  efrlim  26303  o1cxp  26308  jensenlem2  26321  jensen  26322  fsumharmonic  26345  lgamucov  26371  lgamcvg2  26388  wilthlem1  26401  basellem3  26416  basellem6  26419  basellem8  26421  ppisval  26437  chtwordi  26489  ppiwordi  26495  mumullem2  26513  dvdsmulf1o  26527  fsumvma  26545  fsumvma2  26546  chpchtsum  26551  chpub  26552  logfacubnd  26553  dchrmulcl  26581  dchrinv  26593  dchrptlem1  26596  dchrptlem2  26597  sumdchr2  26602  dchr2sum  26605  bposlem7  26622  lgslem1  26629  lgslem3  26631  lgsdirprm  26663  lgsqrlem2  26679  lgseisenlem1  26707  lgseisenlem2  26708  lgseisenlem4  26710  lgseisen  26711  lgsquadlem1  26712  lgsquad2lem1  26716  lgsquad3  26719  m1lgs  26720  2sqlem7  26756  2sq2  26765  2sqmod  26768  chebbnd1lem2  26802  chebbnd1lem3  26803  rplogsumlem1  26816  rpvmasumlem  26819  dchrvmasumlem1  26827  dchrvmasum2lem  26828  dchrvmasumlema  26832  dchrisum0flblem2  26841  dchrisum0fno1  26843  dchrisum0re  26845  logdivsum  26865  pntrsumbnd2  26899  pntpbnd1a  26917  pntpbnd1  26918  pntibndlem2  26923  pntlemr  26934  pntlemj  26935  pntlemf  26937  pnt2  26945  padicabv  26962  ostth2lem2  26966  sltrec  27143  madebday  27213  sltn0  27218  f1otrg  27699  brbtwn2  27740  colinearalglem2  27742  axcgrtr  27750  axcgrid  27751  axsegconlem7  27758  axsegcon  27762  ax5seglem3  27766  ax5seglem6  27769  ax5seg  27773  axpaschlem  27775  axlowdimlem17  27793  axcontlem2  27800  axcontlem4  27802  axcontlem7  27805  axcontlem8  27806  ecgrtg  27818  usgredg2v  28061  vtxdgoddnumeven  28387  2trlond  28770  eupthp1  29046  nmobndi  29603  ubthlem2  29699  ubthlem3  29700  minvecolem2  29703  shuni  30128  pjhthlem1  30219  chscllem2  30466  pjcompi  30500  mayete3i  30556  unoplin  30748  hmoplin  30770  nmophmi  30859  mdslmd4i  31161  isoun  31499  xrge0addcld  31550  xrofsup  31555  eliccelico  31563  elicoelioo  31564  difioo  31568  rexdiv  31665  mgcmnt1d  31740  mgcmnt2d  31741  xrge0addgt0  31765  omndadd2d  31799  omndadd2rd  31800  omndmul2  31803  cycpmcl  31848  cycpm2tr  31851  cyc3evpm  31882  cycpmconjslem2  31887  freshmansdream  31950  fldgensdrg  31966  ofldchr  31992  qusker  32024  eqgvscpbl  32025  ringlsmss1  32060  ringlsmss2  32061  intlidl  32078  rhmpreimaidl  32079  elrspunidl  32082  idlinsubrg  32084  isprmidlc  32099  rhmpreimaprmidl  32103  qsidomlem1  32104  mxidlprm  32116  ssmxidllem  32117  lindsunlem  32196  finexttrb  32228  mdetpmtr2  32274  mdetpmtr12  32275  madjusmdetlem1  32277  madjusmdetlem4  32280  rhmpreimacn  32335  unitdivcld  32351  xrge0mulc1cn  32391  qqhnm  32440  esumcst  32531  esumfsup  32538  esumpmono  32547  esumcvg  32554  difelsiga  32601  sigapisys  32623  sigapildsys  32630  ldgenpisyslem1  32631  1stmbfm  32729  2ndmbfm  32730  dya2icoseg  32746  sibfinima  32808  probmeasb  32899  orvcgteel  32936  orvclteel  32941  ballotlemsima  32984  ballotlemfrceq  32997  sgnmul  33011  ccatmulgnn0dir  33023  fct2relem  33079  ftc2re  33080  chtvalz  33111  subfacp1lem2a  33643  subfaclim  33651  erdsze2lem2  33667  cvmliftlem2  33749  cvmliftlem10  33757  cvmliftlem13  33759  cvmliftiota  33764  cvmlift2lem9  33774  cvmlift2lem11  33776  cvmlift2lem12  33777  cvmliftphtlem  33780  cvmlift3lem6  33787  cvmlift3lem7  33788  cvmlift3lem9  33790  snmlff  33792  mrsubfval  33971  wzel  34269  wsuclem  34270  addsproplem6  34290  sleadd1  34302  negsproplem6  34335  brsegle  34660  opnregcld  34769  fin2so  36032  poimirlem17  36062  poimirlem23  36068  opnmbllem0  36081  mblfinlem3  36084  mblfinlem4  36085  itg2addnclem  36096  itg2addnc  36099  itg2gt0cn  36100  ftc1cnnclem  36116  ftc1cnnc  36117  areacirclem5  36137  indexdom  36160  sstotbnd2  36200  isbnd3  36210  isbnd3b  36211  cntotbnd  36222  ismtyima  36229  heibor1lem  36235  heiborlem8  36244  rrncmslem  36258  reheibor  36265  lkrlsp  37531  lshpkrlem5  37543  ldualssvscl  37587  ldualssvsubcl  37588  llnmlplnN  37969  llncvrlpln  37988  pmapjat1  38283  pclfinN  38330  lautlt  38521  lauteq  38525  lautco  38527  ltrn11  38556  ltrnle  38559  ltrneq2  38578  cdlemednuN  38730  cdleme20k  38749  cdleme20l2  38751  cdleme20l  38752  cdleme20m  38753  cdleme21c  38757  cdleme22e  38774  cdleme22eALTN  38775  cdlemefrs32fva  38830  cdlemg4g  39046  cdlemg18b  39109  cdlemg18c  39110  cdlemj3  39253  dia2dimlem5  39498  dvhopN  39546  cdlemm10N  39548  dihjatcclem4  39851  dochexmidlem2  39891  lclkrlem2o  39951  lcfrlem5  39976  lcfrlem6  39977  lcdlssvscl  40036  mapdpglem6  40108  mapdpglem9  40110  mapdpglem12  40113  mapdpglem14  40115  mapdindp0  40149  hdmaprnlem7N  40285  hdmaprnlem8N  40286  hdmaprnlem3eN  40288  hgmapvvlem3  40355  evlsaddval  40701  evlsmulval  40702  addinvcom  40838  mzpsubst  41009  eldioph2lem1  41021  eldioph2lem2  41022  eldioph2b  41024  diophin  41033  irrapxlem2  41084  irrapxlem4  41086  irrapxlem5  41087  pellexlem1  41090  pellexlem2  41091  pellexlem6  41095  elpell1qr2  41133  pell1qrgaplem  41134  pell1qrgap  41135  pellqrex  41140  pellfundex  41147  pellfund14  41159  rmspecsqrtnq  41167  rmxyadd  41183  congsub  41232  mzpcong  41234  congrep  41235  acongtr  41240  acongrep  41242  jm2.19lem1  41251  jm2.22  41257  jm2.23  41258  jm2.26lem3  41263  jm2.26  41264  jm2.27a  41267  fnwe2lem2  41316  aomclem6  41324  hbtlem2  41389  hbtlem4  41391  hbtlem5  41393  dgraa0p  41414  rngunsnply  41438  proot1hash  41465  nnoeomeqom  41584  cantnf2  41597  omabs2  41603  naddcnff  41614  naddcnffo  41616  naddcnfcom  41618  naddcnfid1  41619  expgrowth  42557  fpmd  43429  abslt2sqd  43530  ioondisj2  43663  ioondisj1  43664  eliocre  43679  ioossioobi  43687  iooiinicc  43712  iooiinioc  43726  icossico2  43734  lptioo2  43804  limcresiooub  43815  limsupequzlem  43895  xlimmnfvlem2  44006  xlimpnfvlem2  44010  cncfuni  44059  cncfiooicclem1  44066  cxpcncf2  44072  dvcnre  44089  dvresntr  44091  dvresioo  44094  dvbdfbdioolem1  44101  dvnmptdivc  44111  dvnxpaek  44115  itgsinexplem1  44127  itgcoscmulx  44142  itgiccshift  44153  itgperiod  44154  ovolsplit  44161  stoweidlem11  44184  stoweidlem26  44199  stoweidlem34  44207  stoweidlem36  44209  stoweidlem38  44211  stirlinglem5  44251  dirkercncflem2  44277  dirkercncflem4  44279  fourierdlem20  44300  fourierdlem58  44337  fourierdlem72  44351  fourierdlem73  44352  fourierdlem74  44353  fourierdlem75  44354  fourierdlem76  44355  fourierdlem79  44358  fourierdlem80  44359  fourierdlem87  44366  fourierdlem94  44373  fourierdlem103  44382  fourierdlem104  44383  fourierdlem107  44386  fourierdlem113  44392  sqwvfoura  44401  sqwvfourb  44402  fourierswlem  44403  fouriersw  44404  etransclem46  44453  etransclem47  44454  rrndistlt  44463  rrnprjdstle  44474  ioorrnopnxrlem  44479  sge0ssre  44570  sge0seq  44619  hsphoidmvle2  44758  hsphoidmvle  44759  hoidmv1lelem1  44764  hoidmv1lelem2  44765  hoidmv1lelem3  44766  hoidmvlelem1  44768  hoidifhspdmvle  44793  hoiqssbllem2  44796  ovolval5lem2  44826  iinhoiicc  44847  iunhoiioo  44849  vonioolem2  44854  vonicclem2  44857  issmflem  44900  iccpartdisj  45561  m1expevenALTV  45771  fpprel2  45865  tgoldbach  45941  strisomgrop  45964  nn0eo  46546  fdivpm  46561  refdivpm  46562  elbigolo1  46575  logbpw2m1  46585  fllog2  46586  dignn0flhalflem1  46633  dignn0flhalflem2  46634  itsclinecirc0in  46793  2itscplem2  46797  itscnhlinecirc02plem1  46800  iccdisj2  46862