MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl22anc Structured version   Visualization version   GIF version

Theorem syl22anc 839
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
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 511 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 837 1 (𝜑𝜂)
Colors of variables: wff setvar class
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  4802  fr2nr  5608  soltmin  6099  f1oprg  6826  f1prex  7239  fveqf1o  7257  weniso  7309  fr3nr  7726  suppofssd  8153  smogt  8307  smocdmdom  8308  oacomf1o  8500  en2prd  8994  difsnen  8997  enfixsn  9024  domss2  9074  ssenen  9089  marypha1lem  9346  fisupcl  9383  ordtypelem3  9435  ordtypelem8  9440  oieu  9454  oismo  9455  wofib  9460  wemaplem2  9462  wemapso  9466  wemapso2lem  9467  unxpwdom2  9503  infdifsn  9578  oemapvali  9605  cantnflem1c  9608  cantnflem1  9610  cantnf  9614  cnfcom3  9625  r1ordg  9702  dif1card  9932  infxpenlem  9935  dfac8clem  9954  infxp  10136  infmap2  10139  cflim2  10185  coftr  10195  fin2i2  10240  enfin2i  10243  fin23lem26  10247  fin23lem27  10250  fin23lem40  10273  isf32lem2  10276  isf32lem3  10277  isf32lem4  10278  isf32lem7  10281  isf32lem9  10283  fin1a2lem13  10334  fin12  10335  alephexp1  10502  gchdomtri  10552  fpwwe2lem11  10564  fpwwe2lem12  10565  gchpwdom  10593  gchhar  10602  adderpqlem  10877  mulerpqlem  10878  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltexnq  10898  distrlem1pr  10948  distrlem4pr  10949  prlem936  10970  reclem3pr  10972  mulcmpblnr  10994  mulgt0d  11301  mul4d  11358  add4d  11375  add42d  11376  subcan  11449  addsub4d  11552  subadd4d  11553  sub4d  11554  2addsubd  11555  addsubeq4d  11556  muladdd  11608  mulsubd  11609  addgegt0d  11723  addgtge0d  11724  addge0d  11726  mulge0d  11727  le2subd  11770  ltleaddd  11771  leltaddd  11772  lt2subd  11774  divdivdiv  11856  divcan5  11857  divne0d  11947  recdivd  11948  recdiv2d  11949  divcan6d  11950  ddcand  11951  rec11d  11952  divmuldivd  11972  divmul13d  11973  divmul24d  11974  divadddivd  11975  divsubdivd  11976  divmuleqd  11977  divdivdivd  11978  mulge0b  12026  recreclt  12055  divgt0d  12091  mulgt1d  12092  lemulge11d  12093  lemulge12d  12094  ltmul12ad  12097  lemul12ad  12098  lemul12bd  12099  supmul1  12125  nndivtr  12224  qreccl  12919  ledivdivd  13011  lediv12ad  13045  lt2mul2divd  13055  xlt2add  13212  supxrun  13268  supxrre  13279  infxrre  13289  elicore  13351  iccss2  13370  iccssico2  13373  icossico2d  13374  lincmb01cmp  13448  iccf1o  13449  nnge2recico01  13460  fzrev2i  13543  2tnp1ge0ge0  13788  m1modnnsub1  13879  modaddmodup  13896  modaddmodlo  13897  modsubdir  13902  fzennn  13930  sermono  13996  mulexpz  14064  expaddz  14068  sqdiv  14083  expsubd  14119  ltexp2a  14128  expmordi  14129  leexp2a  14134  expmulnbnd  14197  digit1  14199  lt2sqd  14218  le2sqd  14219  sq11d  14220  bcm1k  14277  bcp1n  14278  bcp1nk  14279  hashf1lem1  14417  cshw1  14784  2swrd2eqwrdeq  14915  ofccat  14931  absrele  15270  sqreulem  15322  sqrtmuld  15387  sqrtsq2d  15388  sqrtled  15389  sqrtltd  15390  sqr11d  15391  abs3lemd  15426  rlimuni  15512  climuni  15514  lo1resb  15526  o1resb  15528  2clim  15534  addcn2  15556  mulcn2  15558  o1of2  15575  o1rlimmul  15581  lo1add  15589  lo1mul  15590  isercolllem1  15627  caucvgrlem  15635  iseraltlem2  15645  iseraltlem3  15646  mptfzshft  15740  fsumrev  15741  fsum0diag2  15745  binomlem  15794  climcndslem1  15814  climcndslem2  15815  harmonic  15824  mertenslem1  15849  fprodser  15914  fprodrev  15942  efcllem  16042  moddvds  16232  dvds1  16288  dvdsext  16290  evennn2n  16320  bitsinv1  16411  sadaddlem  16435  sadasslem  16439  sadeq  16441  mulgcd  16517  dvdssqlem  16535  lcmftp  16605  rpmulgcd2  16625  coprmproddvdslem  16631  isprm5  16677  isprm6  16684  crth  16748  eulerthlem2  16752  prmdiveq  16756  pythagtriplem11  16796  pythagtriplem13  16798  pcgcd1  16848  pcprmpw2  16853  pcaddlem  16859  fldivp1  16868  4sqlem12  16927  4sqlem14  16929  4sqlem15  16930  4sqlem16  16931  vdwapun  16945  mreexexlem4d  17613  acsfn1  17627  acsfn2  17629  sscpwex  17782  rescabs  17800  yonedainv  18247  chnub  18588  subm0  18783  pmtrfb  19440  psgnunilem1  19468  odmodnn0  19515  odeq  19525  dfod2  19539  sylow1lem1  19573  lsmsubg  19629  lsmmod  19650  lsmdisj2  19657  ghmplusg  19821  odadd  19825  gexexlem  19827  lt6abl  19870  cyggex2  19872  dprdfinv  19996  dmdprdsplitlem  20014  dpjidcl  20035  ablfacrp  20043  ablfacrp2  20044  ablfac1c  20048  ablfac1eu  20050  omndadd2d  20105  omndadd2rd  20106  omndmul2  20108  acsfn1p  20776  lcomfsupp  20897  lssvancl1  20940  lssvnegcl  20951  lspprvacl  20994  ellspsni  20996  lspsn  20997  lmhmplusg  21039  lmhmima  21042  lmhmpreima  21043  reslmhm  21047  lbsind2  21076  lsmcl  21078  lsmelval2  21080  lsppreli  21085  lspprabs  21090  pj1lmhm  21095  lssvs0or  21108  lspabs3  21119  lspfixed  21126  lspexch  21127  lsmcv  21139  lspsolv  21141  drngnidl  21241  rhmpreimaidl  21275  rngqiprngimfo  21299  rngqiprngfulem4  21312  gzrngunit  21413  zringlpirlem3  21444  prmirredlem  21452  znf1o  21531  znunithash  21544  freshmansdream  21554  ofldchr  21556  frlmsubgval  21745  frlmvplusgvalc  21747  frlmvscaval  21748  frlmphllem  21760  frlmphl  21761  frlmssuvc1  21774  frlmsslsp  21776  frlmup1  21778  frlmup2  21779  lindfind2  21798  lindfrn  21801  f1lindf  21802  islindf4  21818  mplbas2  22020  evlslem3  22058  evlslem1  22060  evladdval  22081  evlmulval  22082  coe1addfv  22230  lply1binom  22275  evl1addd  22306  evl1subd  22307  evl1muld  22308  mamudi  22368  mamudir  22369  1marepvmarrepid  22540  mdetrlin  22567  smadiadetglem1  22636  smadiadetg  22638  cramerimplem1  22648  mat2pmatscmxcl  22705  m2pmfzgsumcl  22713  pmatcollpw  22746  pmatcollpwfi  22747  pmatcollpw3fi1lem1  22751  cpmidpmatlem2  22836  cpmadugsumlemF  22841  chcoeffeqlem  22850  ntrin  23026  topssnei  23089  restbas  23123  restntr  23147  cnntri  23236  fiuncmp  23369  nllyrest  23451  nllyidm  23454  hausllycmp  23459  cldllycmp  23460  hauspwdom  23466  txcld  23568  txcn  23591  txlly  23601  txnlly  23602  txhaus  23612  txlm  23613  txkgen  23617  xkococnlem  23624  cnmpt2res  23642  xkoinjcn  23652  basqtop  23676  qtopeu  23681  trfbas2  23808  neifil  23845  hausflim  23946  alexsubALTlem2  24013  cnextfval  24027  cnextfvval  24030  cnextf  24031  cnextfres  24034  clssubg  24074  utop2nei  24215  utop3cls  24216  utopreg  24217  psmetlecl  24280  xmetlecl  24311  prdsxmetlem  24333  bldisj  24363  imasf1obl  24453  prdsbl  24456  stdbdmet  24481  stdbdmopn  24483  met2ndci  24487  metcnp  24506  metustto  24518  metustexhalf  24521  cfilucfil  24524  metucn  24536  lssnlm  24666  nmotri  24704  nmoid  24707  tgioo  24761  blcvx  24763  xrsmopn  24778  reperflem  24784  reconnlem2  24793  opnreen  24797  metdsge  24815  metdsre  24819  metdscnlem  24821  metnrmlem1a  24824  metnrmlem1  24825  metnrmlem3  24827  cncfmet  24876  cnmpopc  24895  icopnfcnv  24909  icopnfhmeo  24910  cnllycmp  24923  evth  24926  lebnumii  24933  nmoleub2lem3  25082  iscfil2  25233  cfil3i  25236  iscfil3  25240  cfilfcls  25241  iscau3  25245  iscmet3lem2  25259  caubl  25275  lmcau  25280  cssbn  25342  rrxcph  25359  minveclem2  25393  pjthlem1  25404  pjthlem2  25405  ivthicc  25425  ovollecl  25450  ovolunlem1a  25463  ovolunnul  25467  ovoliunlem1  25469  ismbl2  25494  nulmbl2  25503  unmbl  25504  volun  25512  voliunlem2  25518  ioombl1lem2  25526  uniioombllem2a  25549  uniioombllem3  25552  uniioombllem4  25553  dyaddisjlem  25562  dyadmaxlem  25564  opnmbllem  25568  volsup2  25572  volcn  25573  ismbfd  25606  mbfi1fseqlem1  25682  mbfi1fseqlem5  25686  itg2lecl  25705  itg2monolem2  25718  itg2gt0  25727  itgspliticc  25804  ellimc3  25846  limcres  25853  dvfval  25864  dvres3  25880  dvres3a  25881  dvmptresicc  25883  dvnff  25890  dvnadd  25896  dvn2bss  25897  dvnres  25898  dvcmul  25911  dvcmulf  25912  dvmptres3  25923  dvmptres2  25929  dvmptntr  25938  dvexp3  25945  dvferm1lem  25951  dvlip  25960  dvlipcn  25961  dvlip2  25962  c1liplem1  25963  dvgt0lem1  25969  dvgt0lem2  25970  dvne0  25978  lhop1lem  25980  lhop2  25982  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcvx  25987  dvfsumle  25988  dvfsumabs  25990  dvfsumlem2  25994  ftc1lem6  26008  ftc1  26009  ftc2ditglem  26012  itgsubstlem  26015  itgpowd  26017  tdeglem4  26025  mdegaddle  26039  mdegmullem  26043  ply1rem  26131  fta1glem2  26134  fta1blem  26136  ig1peu  26140  ig1pdvds  26145  dgrmulc  26236  dgrcolem1  26238  plydivlem4  26262  plydiveu  26264  fta1lem  26273  vieta1lem1  26276  vieta1lem2  26277  plyexmo  26279  taylfvallem1  26322  taylfval  26324  tayl0  26327  taylplem1  26328  taylply2  26333  taylply  26334  dvtaylp  26335  dvntaylp  26336  dvntaylp0  26337  taylthlem1  26338  taylthlem2  26339  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  ulmdvlem1  26365  radcnvlem1  26378  radcnvle  26385  psercn  26391  pserdvlem2  26393  pserdv  26394  abelth  26406  tanregt0  26503  dvlog2lem  26616  efopn  26622  logtayllem  26623  logccv  26627  cxplt3  26664  cxpmul2zd  26680  cxpltd  26683  cxpled  26684  cxplt3d  26699  cxple3d  26700  dvsqrt  26706  cxpcn3  26712  cxpaddle  26716  cxpeq  26721  angcan  26766  angvald  26768  ang180lem2  26774  ang180  26778  isosctrlem3  26784  dquartlem1  26815  atantayl2  26902  leibpi  26906  log2tlbnd  26909  birthdaylem3  26917  xrlimcnp  26932  efrlim  26933  o1cxp  26938  jensenlem2  26951  jensen  26952  fsumharmonic  26975  lgamucov  27001  lgamcvg2  27018  wilthlem1  27031  basellem3  27046  basellem6  27049  basellem8  27051  ppisval  27067  chtwordi  27119  ppiwordi  27125  mumullem2  27143  mpodvdsmulf1o  27157  dvdsmulf1o  27159  fsumvma  27176  fsumvma2  27177  chpchtsum  27182  chpub  27183  logfacubnd  27184  dchrmulcl  27212  dchrinv  27224  dchrptlem1  27227  dchrptlem2  27228  sumdchr2  27233  dchr2sum  27236  bposlem7  27253  lgslem1  27260  lgslem3  27262  lgsdirprm  27294  lgsqrlem2  27310  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem4  27341  lgseisen  27342  lgsquadlem1  27343  lgsquad2lem1  27347  lgsquad3  27350  m1lgs  27351  2sqlem7  27387  2sq2  27396  2sqmod  27399  chebbnd1lem2  27433  chebbnd1lem3  27434  rplogsumlem1  27447  rpvmasumlem  27450  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasumlema  27463  dchrisum0flblem2  27472  dchrisum0fno1  27474  dchrisum0re  27476  logdivsum  27496  pntrsumbnd2  27530  pntpbnd1a  27548  pntpbnd1  27549  pntibndlem2  27554  pntlemr  27565  pntlemj  27566  pntlemf  27568  pnt2  27576  padicabv  27593  ostth2lem2  27597  lesrecd  27792  ltsrecd  27794  madebday  27892  addsproplem6  27966  negsproplem6  28025  mulsproplem13  28120  mulsproplem14  28121  ltmulsd  28129  mulsgt0d  28137  f1otrg  28939  brbtwn2  28974  colinearalglem2  28976  axcgrtr  28984  axcgrid  28985  axsegconlem7  28992  axsegcon  28996  ax5seglem3  29000  ax5seglem6  29003  ax5seg  29007  axpaschlem  29009  axlowdimlem17  29027  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  ecgrtg  29052  usgredg2v  29296  vtxdgoddnumeven  29622  2trlond  30007  eupthp1  30286  nmobndi  30846  ubthlem2  30942  ubthlem3  30943  minvecolem2  30946  shuni  31371  pjhthlem1  31462  chscllem2  31709  pjcompi  31743  mayete3i  31799  unoplin  31991  hmoplin  32013  nmophmi  32102  mdslmd4i  32404  isoun  32775  submuladdd  32813  receqid  32817  xrge0addcld  32835  xrofsup  32840  eliccelico  32850  elicoelioo  32851  difioo  32855  hashpss  32882  sgnmul  32908  rexdiv  32985  mgcmnt1d  33057  mgcmnt2d  33058  xrge0addgt0  33077  cycpmcl  33177  cycpm2tr  33180  cyc3evpm  33211  cycpmconjslem2  33216  fldgensdrg  33375  qusker  33409  eqgvscpbl  33410  ringlsmss1  33456  ringlsmss2  33457  lidlmcld  33479  intlidl  33480  lidlunitel  33483  elrspunidl  33488  idlinsubrg  33491  isprmidlc  33507  rhmpreimaprmidl  33511  qsidomlem1  33512  ssdifidllem  33516  mxidlmaxv  33528  mxidlprm  33530  ssmxidllem  33533  opprmxidlabs  33547  qsdrnglem2  33556  mplvrpmmhm  33690  mplvrpmrhm  33691  esplyind  33719  resssra  33731  ply1degltdimlem  33766  lindsunlem  33768  sdrgfldext  33794  fldsdrgfldext  33805  finexttrb  33809  fldgenfldext  33812  fldextrspunlem1  33819  algextdeglem4  33864  algextdeglem8  33868  constrextdg2lem  33892  mdetpmtr2  33968  mdetpmtr12  33969  madjusmdetlem1  33971  madjusmdetlem4  33974  rhmpreimacn  34029  unitdivcld  34045  xrge0mulc1cn  34085  qqhnm  34134  esumcst  34207  esumfsup  34214  esumpmono  34223  esumcvg  34230  difelsiga  34277  sigapisys  34299  sigapildsys  34306  ldgenpisyslem1  34307  1stmbfm  34404  2ndmbfm  34405  dya2icoseg  34421  sibfinima  34483  probmeasb  34574  orvcgteel  34612  orvclteel  34617  ballotlemsima  34660  ballotlemfrceq  34673  ccatmulgnn0dir  34686  fct2relem  34741  ftc2re  34742  chtvalz  34773  r1filimi  35246  subfacp1lem2a  35362  subfaclim  35370  erdsze2lem2  35386  cvmliftlem2  35468  cvmliftlem10  35476  cvmliftlem13  35478  cvmliftiota  35483  cvmlift2lem9  35493  cvmlift2lem11  35495  cvmlift2lem12  35496  cvmliftphtlem  35499  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  snmlff  35511  mrsubfval  35690  wzel  36004  wsuclem  36005  brsegle  36290  opnregcld  36512  weiunfrlem  36646  fin2so  37928  poimirlem17  37958  poimirlem23  37964  opnmbllem0  37977  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem  37992  itg2addnc  37995  itg2gt0cn  37996  ftc1cnnclem  38012  ftc1cnnc  38013  areacirclem5  38033  indexdom  38055  sstotbnd2  38095  isbnd3  38105  isbnd3b  38106  cntotbnd  38117  ismtyima  38124  heibor1lem  38130  heiborlem8  38139  rrncmslem  38153  reheibor  38160  lkrlsp  39548  lshpkrlem5  39560  ldualssvscl  39604  ldualssvsubcl  39605  llnmlplnN  39985  llncvrlpln  40004  pmapjat1  40299  pclfinN  40346  lautlt  40537  lauteq  40541  lautco  40543  ltrn11  40572  ltrnle  40575  ltrneq2  40594  cdlemednuN  40746  cdleme20k  40765  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21c  40773  cdleme22e  40790  cdleme22eALTN  40791  cdlemefrs32fva  40846  cdlemg4g  41062  cdlemg18b  41125  cdlemg18c  41126  cdlemj3  41269  dia2dimlem5  41514  dvhopN  41562  cdlemm10N  41564  dihjatcclem4  41867  dochexmidlem2  41907  lclkrlem2o  41967  lcfrlem5  41992  lcfrlem6  41993  lcdlssvscl  42052  mapdpglem6  42124  mapdpglem9  42126  mapdpglem12  42129  mapdpglem14  42131  mapdindp0  42165  hdmaprnlem7N  42301  hdmaprnlem8N  42302  hdmaprnlem3eN  42304  hgmapvvlem3  42371  dvun  42791  addinvcom  42864  evlsaddval  43004  evlsmulval  43005  mzpsubst  43180  eldioph2lem1  43192  eldioph2lem2  43193  eldioph2b  43195  diophin  43204  irrapxlem2  43251  irrapxlem4  43253  irrapxlem5  43254  pellexlem1  43257  pellexlem2  43258  pellexlem6  43262  elpell1qr2  43300  pell1qrgaplem  43301  pell1qrgap  43302  pellqrex  43307  pellfundex  43314  pellfund14  43326  rmspecsqrtnq  43334  rmxyadd  43349  congsub  43398  mzpcong  43400  congrep  43401  acongtr  43406  acongrep  43408  jm2.19lem1  43417  jm2.22  43423  jm2.23  43424  jm2.26lem3  43429  jm2.26  43430  jm2.27a  43433  fnwe2lem2  43479  aomclem6  43487  hbtlem2  43552  hbtlem4  43554  hbtlem5  43556  dgraa0p  43577  rngunsnply  43597  proot1hash  43623  nnoeomeqom  43740  cantnf2  43753  omabs2  43760  naddcnff  43790  naddcnffo  43792  naddcnfcom  43794  naddcnfid1  43795  expgrowth  44762  fpmd  45692  abslt2sqd  45790  ioondisj2  45923  ioondisj1  45924  eliocre  45939  ioossioobi  45947  iooiinicc  45972  iooiinioc  45986  lptioo2  46061  limcresiooub  46070  limsupequzlem  46150  xlimmnfvlem2  46261  xlimpnfvlem2  46265  cncfuni  46314  cncfiooicclem1  46321  cxpcncf2  46327  dvcnre  46344  dvresntr  46346  dvresioo  46349  dvbdfbdioolem1  46356  dvnmptdivc  46366  dvnxpaek  46370  itgsinexplem1  46382  itgcoscmulx  46397  itgiccshift  46408  itgperiod  46409  ovolsplit  46416  stoweidlem11  46439  stoweidlem26  46454  stoweidlem34  46462  stoweidlem36  46464  stoweidlem38  46466  stirlinglem5  46506  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem20  46555  fourierdlem58  46592  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem79  46613  fourierdlem80  46614  fourierdlem87  46621  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem113  46647  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem46  46708  etransclem47  46709  rrndistlt  46718  rrnprjdstle  46729  ioorrnopnxrlem  46734  sge0ssre  46825  sge0seq  46874  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmvlelem1  47023  hoidifhspdmvle  47048  hoiqssbllem2  47051  ovolval5lem2  47081  iinhoiicc  47102  iunhoiioo  47104  vonioolem2  47109  vonicclem2  47112  issmflem  47155  submodlt  47804  iccpartdisj  47897  m1expevenALTV  48123  fpprel2  48217  tgoldbach  48293  opstrgric  48402  gpg3kgrtriex  48565  nn0eo  49004  fdivpm  49019  refdivpm  49020  elbigolo1  49033  logbpw2m1  49043  fllog2  49044  dignn0flhalflem1  49091  dignn0flhalflem2  49092  itsclinecirc0in  49251  2itscplem2  49255  itscnhlinecirc02plem1  49258  iccdisj2  49372
  Copyright terms: Public domain W3C validator