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

Theorem syl22anc 1318
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 552 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 1315 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  preqsnd  4325  fr2nr  5006  soltmin  5438  f1oprg  6078  f1prex  6417  fveqf1o  6435  weniso  6482  fr3nr  6848  smogt  7328  smorndom  7329  oacomf1o  7509  difsnen  7904  undom  7910  enfixsn  7931  domss2  7981  ssenen  7996  marypha1lem  8199  fisupcl  8235  ordtypelem3  8285  ordtypelem8  8290  oieu  8304  oismo  8305  wofib  8310  wemaplem2  8312  wemapso  8316  wemapso2lem  8317  unxpwdom2  8353  infdifsn  8414  oemapvali  8441  cantnflem1c  8444  cantnflem1  8446  cantnf  8450  cnfcom3  8461  r1ordg  8501  dif1card  8693  infxpenlem  8696  dfac8clem  8715  infxp  8897  infmap2  8900  cflim2  8945  coftr  8955  fin2i2  9000  enfin2i  9003  fin23lem26  9007  fin23lem27  9010  fin23lem40  9033  isf32lem2  9036  isf32lem3  9037  isf32lem4  9038  isf32lem7  9041  isf32lem9  9043  fin1a2lem13  9094  fin12  9095  alephexp1  9257  gchdomtri  9307  fpwwe2lem12  9319  fpwwe2lem13  9320  gchpwdom  9348  gchhar  9357  adderpqlem  9632  mulerpqlem  9633  addassnq  9636  mulassnq  9637  distrnq  9639  mulidnq  9641  recmulnq  9642  ltexnq  9653  distrlem1pr  9703  distrlem4pr  9704  prlem936  9725  reclem3pr  9727  mulcmpblnr  9748  mulgt0d  10043  mul4d  10099  add4d  10115  add42d  10116  subcan  10187  addsub4d  10290  subadd4d  10291  sub4d  10292  2addsubd  10293  addsubeq4d  10294  muladdd  10338  mulsubd  10339  addgegt0d  10450  addge0d  10452  mulge0d  10453  le2addd  10495  le2subd  10496  ltleaddd  10497  leltaddd  10498  lt2subd  10500  divdivdiv  10575  divcan5  10576  divne0d  10666  recdivd  10667  recdiv2d  10668  divcan6d  10669  ddcand  10670  rec11d  10671  divmuldivd  10691  divmul13d  10692  divmul24d  10693  divadddivd  10694  divsubdivd  10695  divmuleqd  10696  divdivdivd  10697  subrecd  10705  mulge0b  10742  recreclt  10771  divgt0d  10808  mulgt1d  10809  lemulge11d  10810  lemulge12d  10811  ltmul12ad  10814  lemul12ad  10815  lemul12bd  10816  supmul1  10839  nndivtr  10909  qreccl  11640  ledivdivd  11729  lediv12ad  11763  lt2mul2divd  11771  xlt2add  11919  supxrun  11974  supxrre  11985  infxrre  11994  elicore  12053  iccss2  12071  iccssico2  12074  lincmb01cmp  12142  iccf1o  12143  fzrev2i  12230  fz1fzo0m1  12338  2tnp1ge0ge0  12447  m1modnnsub1  12533  modaddmodup  12550  modaddmodlo  12551  modsubdir  12556  fzennn  12584  sermono  12650  mulexpz  12717  expaddz  12721  ltexp2a  12729  leexp2a  12733  sqdiv  12745  expmulnbnd  12813  digit1  12815  expsubd  12836  lt2sqd  12860  le2sqd  12861  sq11d  12862  bcm1k  12919  bcp1n  12920  bcp1nk  12921  hashf1lem1  13048  cshw1  13365  2swrd2eqwrdeq  13490  ofccat  13502  absrele  13842  sqreulem  13893  sqrtmuld  13957  sqrtsq2d  13958  sqrtled  13959  sqrtltd  13960  sqr11d  13961  abs3lemd  13994  rlimuni  14075  climuni  14077  lo1resb  14089  o1resb  14091  2clim  14097  addcn2  14118  mulcn2  14120  o1of2  14137  o1rlimmul  14143  lo1add  14151  lo1mul  14152  isercolllem1  14189  caucvgrlem  14197  iseraltlem2  14207  iseraltlem3  14208  iseralt  14209  mptfzshft  14298  fsumrev  14299  fsum0diag2  14303  binomlem  14346  climcndslem1  14366  climcndslem2  14367  harmonic  14376  mertenslem1  14401  fprodser  14464  fprodrev  14492  rprisefaccl  14539  efcllem  14593  moddvds  14775  dvds1  14825  dvdsext  14827  oexpneg  14853  evennn02n  14858  evennn2n  14859  bitsinv1  14948  sadaddlem  14972  sadasslem  14976  sadeq  14978  mulgcd  15049  dvdssqlem  15063  lcmftp  15133  rpmulgcd2  15154  coprmproddvdslem  15160  isprm5  15203  isprm6  15210  crth  15267  eulerthlem2  15271  prmdiveq  15275  pythagtriplem11  15314  pythagtriplem13  15316  iserodd  15324  pcgcd1  15365  pcprmpw2  15370  pcaddlem  15376  fldivp1  15385  4sqlem12  15444  4sqlem14  15446  4sqlem15  15447  4sqlem16  15448  vdwapun  15462  mreexexlem4d  16076  acsfn1  16091  acsfn2  16093  sscpwex  16244  rescabs  16262  yonedainv  16690  subm0  17125  pmtrfb  17654  psgnunilem1  17682  odmodnn0  17728  odeq  17738  dfod2  17750  sylow1lem1  17782  lsmsubg  17838  lsmmod  17857  lsmdisj2  17864  ghmplusg  18018  odadd  18022  gexexlem  18024  lt6abl  18065  cyggex2  18067  dprdfinv  18187  dmdprdsplitlem  18205  dpjidcl  18226  ablfacrp  18234  ablfacrp2  18235  ablfac1c  18239  ablfac1eu  18241  lcomfsupp  18672  lssvancl1  18712  lssvnegcl  18723  lspprvacl  18766  lspsneli  18768  lspsn  18769  lmhmplusg  18811  lmhmima  18814  lmhmpreima  18815  reslmhm  18819  lbsind2  18848  lsmcl  18850  lsmelval2  18852  lsppreli  18857  lspprabs  18862  pj1lmhm  18867  lssvs0or  18877  lspabs3  18888  lspfixed  18895  lspexch  18896  lsmcv  18908  lspsolv  18910  lidlmcl  18984  drngnidl  18996  2idlcpbl  19001  mplbas2  19237  evlslem3  19281  evlslem1  19282  coe1addfv  19402  lply1binom  19443  evl1addd  19472  evl1subd  19473  evl1muld  19474  gzrngunit  19577  zringlpirlem3  19599  prmirredlem  19605  znf1o  19664  znunithash  19677  frlmsubgval  19869  frlmvscaval  19871  frlmphllem  19880  frlmphl  19881  frlmssuvc1  19894  frlmsslsp  19896  frlmup1  19898  frlmup2  19899  lindfind2  19918  lindfrn  19921  f1lindf  19922  islindf4  19938  mamudi  19970  mamudir  19971  1marepvmarrepid  20142  mdetrlin  20169  smadiadetglem1  20238  smadiadetg  20240  cramerimplem1  20250  mat2pmatscmxcl  20306  m2pmfzgsumcl  20314  pmatcollpw  20347  pmatcollpwfi  20348  pmatcollpw3fi1lem1  20352  cpmidpmatlem2  20437  cpmadugsumlemF  20442  chcoeffeqlem  20451  ntrin  20617  topssnei  20680  restbas  20714  restntr  20738  cnntri  20827  fiuncmp  20959  nllyrest  21041  nllyidm  21044  hausllycmp  21049  cldllycmp  21050  hauspwdom  21056  txcld  21158  txcn  21181  txlly  21191  txnlly  21192  txhaus  21202  txlm  21203  txkgen  21207  xkococnlem  21214  cnmpt2res  21232  xkoinjcn  21242  basqtop  21266  qtopeu  21271  trfbas2  21399  neifil  21436  hausflim  21537  alexsubALTlem2  21604  cnextfval  21618  cnextfvval  21621  cnextf  21622  cnextfres  21625  clssubg  21664  utop2nei  21806  utop3cls  21807  utopreg  21808  psmetlecl  21872  xmetlecl  21902  prdsxmetlem  21924  bldisj  21954  imasf1obl  22044  prdsbl  22047  stdbdmet  22072  stdbdmopn  22074  met2ndci  22078  metcnp  22097  metustto  22109  metustexhalf  22112  cfilucfil  22115  metucn  22127  lssnlm  22248  nmotri  22285  nmoid  22288  tgioo  22339  blcvx  22341  xrsmopn  22355  reperflem  22361  reconnlem2  22370  opnreen  22374  metdsge  22391  metdsre  22395  metdscnlem  22397  metnrmlem1a  22400  metnrmlem1  22401  metnrmlem3  22403  cncfmet  22450  cnmpt2pc  22466  icopnfcnv  22480  icopnfhmeo  22481  cnllycmp  22494  evth  22497  lebnumii  22504  nmoleub2lem3  22654  iscfil2  22790  cfil3i  22793  iscfil3  22797  cfilfcls  22798  iscau3  22802  iscmet3lem2  22816  caubl  22831  lmcau  22836  rrxcph  22905  minveclem2  22922  pjthlem1  22933  pjthlem2  22934  ivthicc  22951  ovollecl  22975  ovolunlem1a  22988  ovolunnul  22992  ovoliunlem1  22994  ismbl2  23019  nulmbl2  23028  unmbl  23029  volun  23037  voliunlem2  23043  ioombl1lem2  23051  uniioombllem2a  23073  uniioombllem3  23076  uniioombllem4  23077  dyaddisjlem  23086  dyadmaxlem  23088  opnmbllem  23092  volsup2  23096  volcn  23097  ismbfd  23130  mbfi1fseqlem1  23205  mbfi1fseqlem5  23209  itg2lecl  23228  itg2monolem2  23241  itg2gt0  23250  itgspliticc  23326  ellimc3  23366  limcres  23373  dvfval  23384  dvres3  23400  dvres3a  23401  dvnff  23409  dvnadd  23415  dvn2bss  23416  dvnres  23417  dvcmul  23430  dvcmulf  23431  dvmptres3  23442  dvmptres2  23448  dvmptntr  23457  dvexp3  23462  dvferm1lem  23468  dvlip  23477  dvlipcn  23478  dvlip2  23479  c1liplem1  23480  dvgt0lem1  23486  dvgt0lem2  23487  dvne0  23495  lhop1lem  23497  lhop2  23499  lhop  23500  dvcnvrelem1  23501  dvcnvrelem2  23502  dvcvx  23504  dvfsumle  23505  dvfsumabs  23507  dvfsumlem2  23511  ftc1lem6  23525  ftc1  23526  ftc2ditglem  23529  itgsubstlem  23532  tdeglem4  23541  mdegaddle  23555  mdegmullem  23559  ply1rem  23644  fta1glem2  23647  fta1blem  23649  ig1peu  23652  ig1pdvds  23657  dgrmulc  23748  dgrcolem1  23750  plydivlem4  23772  plydiveu  23774  fta1lem  23783  vieta1lem1  23786  vieta1lem2  23787  plyexmo  23789  taylfvallem1  23832  taylfval  23834  tayl0  23837  taylplem1  23838  taylply2  23843  taylply  23844  dvtaylp  23845  dvntaylp  23846  dvntaylp0  23847  taylthlem1  23848  taylthlem2  23849  ulmcaulem  23869  ulmcau  23870  ulmcn  23874  ulmdvlem1  23875  radcnvlem1  23888  radcnvle  23895  psercn  23901  pserdvlem2  23903  pserdv  23904  abelth  23916  cosordlem  23998  tanregt0  24006  dvlog2lem  24115  efopn  24121  logtayllem  24122  logccv  24126  cxplt3  24163  cxpmul2zd  24179  cxpltd  24182  cxpled  24183  cxplt3d  24195  cxple3d  24196  dvsqrt  24200  cxpcn3  24206  cxpaddle  24210  cxpeq  24215  angcan  24249  angvald  24251  ang180lem2  24257  ang180  24261  isosctrlem3  24267  dquartlem1  24295  atantayl2  24382  leibpilem1  24384  leibpi  24386  log2tlbnd  24389  birthdaylem3  24397  xrlimcnp  24412  efrlim  24413  o1cxp  24418  jensenlem2  24431  jensen  24432  fsumharmonic  24455  lgamucov  24481  lgamcvg2  24498  wilthlem1  24511  basellem3  24526  basellem6  24529  basellem8  24531  ppisval  24547  chtwordi  24599  ppiwordi  24605  mumullem2  24623  dvdsmulf1o  24637  fsumvma  24655  fsumvma2  24656  chpchtsum  24661  chpub  24662  logfacubnd  24663  dchrmulcl  24691  dchrinv  24703  dchrptlem1  24706  dchrptlem2  24707  sumdchr2  24712  dchr2sum  24715  bposlem7  24732  lgslem1  24739  lgslem3  24741  lgsdirprm  24773  lgsqrlem2  24789  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem4  24820  lgseisen  24821  lgsquadlem1  24822  lgsquad2lem1  24826  lgsquad3  24829  m1lgs  24830  2sqlem7  24866  chebbnd1lem2  24876  chebbnd1lem3  24877  rplogsumlem1  24890  rpvmasumlem  24893  dchrvmasumlem1  24901  dchrvmasum2lem  24902  dchrvmasumlema  24906  dchrisum0flblem2  24915  dchrisum0fno1  24917  dchrisum0re  24919  logdivsum  24939  pntrsumbnd2  24973  pntpbnd1a  24991  pntpbnd1  24992  pntibndlem2  24997  pntlemr  25008  pntlemj  25009  pntlemf  25011  pnt2  25019  padicabv  25036  ostth2lem2  25040  f1otrg  25469  brbtwn2  25503  colinearalglem2  25505  axcgrtr  25513  axcgrid  25514  axsegconlem7  25521  axsegcon  25525  ax5seglem3  25529  ax5seglem6  25532  ax5seg  25536  axpaschlem  25538  axlowdimlem17  25556  axcontlem2  25563  axcontlem4  25565  axcontlem7  25568  axcontlem8  25569  ecgrtg  25581  usgraidx2v  25688  iseupa  26258  eupap1  26269  eupath2lem3  26272  numclwwlkovf2ex  26379  nmobndi  26820  ubthlem2  26917  ubthlem3  26918  minvecolem2  26921  shuni  27349  pjhthlem1  27440  chscllem2  27687  pjcompi  27721  mayete3i  27777  unoplin  27969  hmoplin  27991  nmophmi  28080  mdslmd4i  28382  isoun  28668  xrge0addcld  28723  xrofsup  28729  eliccelico  28735  elicoelioo  28736  difioo  28740  rexdiv  28771  2sqmod  28785  xrge0addgt0  28828  omndadd2d  28845  omndadd2rd  28846  omndmul2  28849  ofldchr  28951  mdetpmtr2  29024  mdetpmtr12  29025  madjusmdetlem1  29027  madjusmdetlem4  29030  unitdivcld  29081  xrge0mulc1cn  29121  qqhnm  29168  esumcst  29258  esumfsup  29265  esumpmono  29274  esumcvg  29281  difelsiga  29329  sigapisys  29351  sigapildsys  29358  ldgenpisyslem1  29359  1stmbfm  29455  2ndmbfm  29456  dya2icoseg  29472  sibfinima  29534  probmeasb  29625  orvcgteel  29662  orvclteel  29667  ballotlemsima  29710  ballotlemfrceq  29723  sgnmul  29737  ccatmulgnn0dir  29751  subfacp1lem2a  30222  subfaclim  30230  erdsze2lem2  30246  cvmliftlem2  30328  cvmliftlem10  30336  cvmliftlem13  30338  cvmliftiota  30343  cvmlift2lem9  30353  cvmlift2lem11  30355  cvmlift2lem12  30356  cvmliftphtlem  30359  cvmlift3lem6  30366  cvmlift3lem7  30367  cvmlift3lem9  30369  snmlff  30371  mrsubfval  30465  trpredelss  30782  trpredpo  30785  wzel  30821  wzelOLD  30822  wsuclem  30823  wsuclemOLD  30824  nodenselem5  30890  nobndlem6  30902  brsegle  31191  opnregcld  31301  addgtge0d  31472  fin2so  32362  poimirlem17  32392  poimirlem23  32398  opnmbllem0  32411  mblfinlem3  32414  mblfinlem4  32415  itg2addnclem  32427  itg2addnc  32430  itg2gt0cn  32431  ftc1cnnclem  32449  ftc1cnnc  32450  areacirclem5  32470  indexdom  32495  sstotbnd2  32539  isbnd3  32549  isbnd3b  32550  cntotbnd  32561  ismtyima  32568  heibor1lem  32574  heiborlem8  32583  rrncmslem  32597  reheibor  32604  lkrlsp  33203  lshpkrlem5  33215  ldualssvscl  33259  ldualssvsubcl  33260  llnmlplnN  33639  llncvrlpln  33658  pmapjat1  33953  pclfinN  34000  lautlt  34191  lauteq  34195  lautco  34197  ltrn11  34226  ltrnle  34229  ltrneq2  34248  cdlemednuN  34401  cdleme20k  34421  cdleme20l2  34423  cdleme20l  34424  cdleme20m  34425  cdleme21c  34429  cdleme22e  34446  cdleme22eALTN  34447  cdlemefrs32fva  34502  cdlemg4g  34718  cdlemg18b  34781  cdlemg18c  34782  cdlemj3  34925  dia2dimlem5  35171  dvhopN  35219  cdlemm10N  35221  dihjatcclem4  35524  dochexmidlem2  35564  lclkrlem2o  35624  lcfrlem5  35649  lcfrlem6  35650  lcdlssvscl  35709  mapdpglem6  35781  mapdpglem9  35783  mapdpglem12  35786  mapdpglem14  35788  mapdindp0  35822  hdmaprnlem7N  35961  hdmaprnlem8N  35962  hdmaprnlem3eN  35964  hgmapvvlem3  36031  mzpsubst  36125  eldioph2lem1  36137  eldioph2lem2  36138  eldioph2b  36140  diophin  36150  irrapxlem2  36201  irrapxlem4  36203  irrapxlem5  36204  pellexlem1  36207  pellexlem2  36208  pellexlem6  36212  elpell1qr2  36250  pell1qrgaplem  36251  pell1qrgap  36252  pellqrex  36257  pellfundex  36264  pellfund14  36276  rmspecsqrtnq  36284  rmspecsqrtnqOLD  36285  rmxyadd  36300  expmordi  36326  rmxypos  36328  jm2.24  36344  congsub  36351  mzpcong  36353  congrep  36354  acongtr  36359  acongrep  36361  jm2.19lem1  36370  jm2.22  36376  jm2.23  36377  jm2.26lem3  36382  jm2.26  36383  jm2.27a  36386  fnwe2lem2  36435  aomclem6  36443  hbtlem2  36509  hbtlem4  36511  hbtlem5  36513  dgraa0p  36534  rngunsnply  36558  acsfn1p  36584  proot1hash  36593  itgpowd  36615  expgrowth  37352  abslt2sqd  38314  ioondisj2  38358  ioondisj1  38359  eliocre  38378  ioossioobi  38387  iooiinicc  38413  iooiinioc  38427  lptioo2  38495  limcresiooub  38506  cncfuni  38569  cncfiooicclem1  38576  cxpcncf2  38583  dvcnre  38601  dvresntr  38603  dvmptresicc  38606  dvresioo  38608  dvbdfbdioolem1  38615  dvnmptdivc  38625  dvnxpaek  38629  itgsinexplem1  38642  itgcoscmulx  38658  itgiccshift  38669  itgperiod  38670  ovolsplit  38678  stoweidlem11  38701  stoweidlem26  38716  stoweidlem34  38724  stoweidlem36  38726  stoweidlem38  38728  stirlinglem5  38768  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem20  38817  fourierdlem58  38854  fourierdlem72  38868  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem76  38872  fourierdlem79  38875  fourierdlem80  38876  fourierdlem87  38883  fourierdlem94  38890  fourierdlem103  38899  fourierdlem104  38900  fourierdlem107  38903  fourierdlem113  38909  sqwvfoura  38918  sqwvfourb  38919  fourierswlem  38920  fouriersw  38921  etransclem46  38970  etransclem47  38971  rrndistlt  38983  rrnprjdstle  38994  ioorrnopnxrlem  38999  sge0ssre  39087  sge0seq  39136  hsphoidmvle2  39272  hsphoidmvle  39273  hoidmv1lelem1  39278  hoidmv1lelem2  39279  hoidmv1lelem3  39280  hoidmvlelem1  39282  hoidifhspdmvle  39307  hoiqssbllem2  39310  ovolval5lem2  39340  iinhoiicc  39362  iunhoiioo  39364  vonioolem2  39369  vonicclem2  39372  issmflem  39410  iccpartdisj  39773  m1expevenALTV  39896  oexpnegALTV  39924  tgoldbach  40030  tgoldbachOLD  40037  usgredg2v  40449  2trlond  41141  eupthp1  41379  av-numclwwlkovf2ex  41512  nn0eo  42111  fdivpm  42130  refdivpm  42131  elbigolo1  42144  logbpw2m1  42154  fllog2  42155  dignn0flhalflem1  42202  dignn0flhalflem2  42203
  Copyright terms: Public domain W3C validator