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

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
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 836 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  4813  fr2nr  5600  soltmin  6089  f1oprg  6813  f1prex  7225  fveqf1o  7243  weniso  7295  fr3nr  7712  suppofssd  8143  smogt  8297  smocdmdom  8298  oacomf1o  8490  en2prd  8980  difsnen  8983  enfixsn  9010  domss2  9060  ssenen  9075  marypha1lem  9342  fisupcl  9379  ordtypelem3  9431  ordtypelem8  9436  oieu  9450  oismo  9451  wofib  9456  wemaplem2  9458  wemapso  9462  wemapso2lem  9463  unxpwdom2  9499  infdifsn  9572  oemapvali  9599  cantnflem1c  9602  cantnflem1  9604  cantnf  9608  cnfcom3  9619  r1ordg  9693  dif1card  9923  infxpenlem  9926  dfac8clem  9945  infxp  10127  infmap2  10130  cflim2  10176  coftr  10186  fin2i2  10231  enfin2i  10234  fin23lem26  10238  fin23lem27  10241  fin23lem40  10264  isf32lem2  10267  isf32lem3  10268  isf32lem4  10269  isf32lem7  10272  isf32lem9  10274  fin1a2lem13  10325  fin12  10326  alephexp1  10492  gchdomtri  10542  fpwwe2lem11  10554  fpwwe2lem12  10555  gchpwdom  10583  gchhar  10592  adderpqlem  10867  mulerpqlem  10868  addassnq  10871  mulassnq  10872  distrnq  10874  mulidnq  10876  recmulnq  10877  ltexnq  10888  distrlem1pr  10938  distrlem4pr  10939  prlem936  10960  reclem3pr  10962  mulcmpblnr  10984  mulgt0d  11289  mul4d  11346  add4d  11363  add42d  11364  subcan  11437  addsub4d  11540  subadd4d  11541  sub4d  11542  2addsubd  11543  addsubeq4d  11544  muladdd  11596  mulsubd  11597  addgegt0d  11711  addgtge0d  11712  addge0d  11714  mulge0d  11715  le2subd  11758  ltleaddd  11759  leltaddd  11760  lt2subd  11762  divdivdiv  11843  divcan5  11844  divne0d  11934  recdivd  11935  recdiv2d  11936  divcan6d  11937  ddcand  11938  rec11d  11939  divmuldivd  11959  divmul13d  11960  divmul24d  11961  divadddivd  11962  divsubdivd  11963  divmuleqd  11964  divdivdivd  11965  mulge0b  12013  recreclt  12042  divgt0d  12078  mulgt1d  12079  lemulge11d  12080  lemulge12d  12081  ltmul12ad  12084  lemul12ad  12085  lemul12bd  12086  supmul1  12112  nndivtr  12193  qreccl  12888  ledivdivd  12980  lediv12ad  13014  lt2mul2divd  13024  xlt2add  13180  supxrun  13236  supxrre  13247  infxrre  13257  elicore  13319  iccss2  13338  iccssico2  13341  icossico2d  13342  lincmb01cmp  13416  iccf1o  13417  fzrev2i  13510  2tnp1ge0ge0  13751  m1modnnsub1  13842  modaddmodup  13859  modaddmodlo  13860  modsubdir  13865  fzennn  13893  sermono  13959  mulexpz  14027  expaddz  14031  sqdiv  14046  expsubd  14082  ltexp2a  14091  expmordi  14092  leexp2a  14097  expmulnbnd  14160  digit1  14162  lt2sqd  14181  le2sqd  14182  sq11d  14183  bcm1k  14240  bcp1n  14241  bcp1nk  14242  hashf1lem1  14380  cshw1  14746  2swrd2eqwrdeq  14878  ofccat  14894  absrele  15233  sqreulem  15285  sqrtmuld  15350  sqrtsq2d  15351  sqrtled  15352  sqrtltd  15353  sqr11d  15354  abs3lemd  15389  rlimuni  15475  climuni  15477  lo1resb  15489  o1resb  15491  2clim  15497  addcn2  15519  mulcn2  15521  o1of2  15538  o1rlimmul  15544  lo1add  15552  lo1mul  15553  isercolllem1  15590  caucvgrlem  15598  iseraltlem2  15608  iseraltlem3  15609  mptfzshft  15703  fsumrev  15704  fsum0diag2  15708  binomlem  15754  climcndslem1  15774  climcndslem2  15775  harmonic  15784  mertenslem1  15809  fprodser  15874  fprodrev  15902  efcllem  16002  moddvds  16192  dvds1  16248  dvdsext  16250  evennn2n  16280  bitsinv1  16371  sadaddlem  16395  sadasslem  16399  sadeq  16401  mulgcd  16477  dvdssqlem  16495  lcmftp  16565  rpmulgcd2  16585  coprmproddvdslem  16591  isprm5  16636  isprm6  16643  crth  16707  eulerthlem2  16711  prmdiveq  16715  pythagtriplem11  16755  pythagtriplem13  16757  pcgcd1  16807  pcprmpw2  16812  pcaddlem  16818  fldivp1  16827  4sqlem12  16886  4sqlem14  16888  4sqlem15  16889  4sqlem16  16890  vdwapun  16904  mreexexlem4d  17571  acsfn1  17585  acsfn2  17587  sscpwex  17740  rescabs  17758  yonedainv  18205  subm0  18707  pmtrfb  19362  psgnunilem1  19390  odmodnn0  19437  odeq  19447  dfod2  19461  sylow1lem1  19495  lsmsubg  19551  lsmmod  19572  lsmdisj2  19579  ghmplusg  19743  odadd  19747  gexexlem  19749  lt6abl  19792  cyggex2  19794  dprdfinv  19918  dmdprdsplitlem  19936  dpjidcl  19957  ablfacrp  19965  ablfacrp2  19966  ablfac1c  19970  ablfac1eu  19972  omndadd2d  20027  omndadd2rd  20028  omndmul2  20030  acsfn1p  20702  lcomfsupp  20823  lssvancl1  20866  lssvnegcl  20877  lspprvacl  20920  ellspsni  20922  lspsn  20923  lmhmplusg  20966  lmhmima  20969  lmhmpreima  20970  reslmhm  20974  lbsind2  21003  lsmcl  21005  lsmelval2  21007  lsppreli  21012  lspprabs  21017  pj1lmhm  21022  lssvs0or  21035  lspabs3  21046  lspfixed  21053  lspexch  21054  lsmcv  21066  lspsolv  21068  drngnidl  21168  rhmpreimaidl  21202  rngqiprngimfo  21226  rngqiprngfulem4  21239  gzrngunit  21358  zringlpirlem3  21389  prmirredlem  21397  znf1o  21476  znunithash  21489  freshmansdream  21499  ofldchr  21501  frlmsubgval  21690  frlmvplusgvalc  21692  frlmvscaval  21693  frlmphllem  21705  frlmphl  21706  frlmssuvc1  21719  frlmsslsp  21721  frlmup1  21723  frlmup2  21724  lindfind2  21743  lindfrn  21746  f1lindf  21747  islindf4  21763  mplbas2  21965  evlslem3  22003  evlslem1  22005  coe1addfv  22167  lply1binom  22213  evl1addd  22244  evl1subd  22245  evl1muld  22246  mamudi  22306  mamudir  22307  1marepvmarrepid  22478  mdetrlin  22505  smadiadetglem1  22574  smadiadetg  22576  cramerimplem1  22586  mat2pmatscmxcl  22643  m2pmfzgsumcl  22651  pmatcollpw  22684  pmatcollpwfi  22685  pmatcollpw3fi1lem1  22689  cpmidpmatlem2  22774  cpmadugsumlemF  22779  chcoeffeqlem  22788  ntrin  22964  topssnei  23027  restbas  23061  restntr  23085  cnntri  23174  fiuncmp  23307  nllyrest  23389  nllyidm  23392  hausllycmp  23397  cldllycmp  23398  hauspwdom  23404  txcld  23506  txcn  23529  txlly  23539  txnlly  23540  txhaus  23550  txlm  23551  txkgen  23555  xkococnlem  23562  cnmpt2res  23580  xkoinjcn  23590  basqtop  23614  qtopeu  23619  trfbas2  23746  neifil  23783  hausflim  23884  alexsubALTlem2  23951  cnextfval  23965  cnextfvval  23968  cnextf  23969  cnextfres  23972  clssubg  24012  utop2nei  24154  utop3cls  24155  utopreg  24156  psmetlecl  24219  xmetlecl  24250  prdsxmetlem  24272  bldisj  24302  imasf1obl  24392  prdsbl  24395  stdbdmet  24420  stdbdmopn  24422  met2ndci  24426  metcnp  24445  metustto  24457  metustexhalf  24460  cfilucfil  24463  metucn  24475  lssnlm  24605  nmotri  24643  nmoid  24646  tgioo  24700  blcvx  24702  xrsmopn  24717  reperflem  24723  reconnlem2  24732  opnreen  24736  metdsge  24754  metdsre  24758  metdscnlem  24760  metnrmlem1a  24763  metnrmlem1  24764  metnrmlem3  24766  cncfmet  24818  cnmpopc  24838  icopnfcnv  24856  icopnfhmeo  24857  cnllycmp  24871  evth  24874  lebnumii  24881  nmoleub2lem3  25031  iscfil2  25182  cfil3i  25185  iscfil3  25189  cfilfcls  25190  iscau3  25194  iscmet3lem2  25208  caubl  25224  lmcau  25229  cssbn  25291  rrxcph  25308  minveclem2  25342  pjthlem1  25353  pjthlem2  25354  ivthicc  25375  ovollecl  25400  ovolunlem1a  25413  ovolunnul  25417  ovoliunlem1  25419  ismbl2  25444  nulmbl2  25453  unmbl  25454  volun  25462  voliunlem2  25468  ioombl1lem2  25476  uniioombllem2a  25499  uniioombllem3  25502  uniioombllem4  25503  dyaddisjlem  25512  dyadmaxlem  25514  opnmbllem  25518  volsup2  25522  volcn  25523  ismbfd  25556  mbfi1fseqlem1  25632  mbfi1fseqlem5  25636  itg2lecl  25655  itg2monolem2  25668  itg2gt0  25677  itgspliticc  25754  ellimc3  25796  limcres  25803  dvfval  25814  dvres3  25830  dvres3a  25831  dvmptresicc  25833  dvnff  25841  dvnadd  25847  dvn2bss  25848  dvnres  25849  dvcmul  25863  dvcmulf  25864  dvmptres3  25876  dvmptres2  25882  dvmptntr  25891  dvexp3  25898  dvferm1lem  25904  dvlip  25914  dvlipcn  25915  dvlip2  25916  c1liplem1  25917  dvgt0lem1  25923  dvgt0lem2  25924  dvne0  25932  lhop1lem  25934  lhop2  25936  lhop  25937  dvcnvrelem1  25938  dvcnvrelem2  25939  dvcvx  25941  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  ftc1lem6  25964  ftc1  25965  ftc2ditglem  25968  itgsubstlem  25971  itgpowd  25973  tdeglem4  25981  mdegaddle  25995  mdegmullem  25999  ply1rem  26087  fta1glem2  26090  fta1blem  26092  ig1peu  26096  ig1pdvds  26101  dgrmulc  26193  dgrcolem1  26195  plydivlem4  26220  plydiveu  26222  fta1lem  26231  vieta1lem1  26234  vieta1lem2  26235  plyexmo  26237  taylfvallem1  26280  taylfval  26282  tayl0  26285  taylplem1  26286  taylply2  26291  taylply2OLD  26292  taylply  26293  dvtaylp  26294  dvntaylp  26295  dvntaylp0  26296  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  ulmcaulem  26319  ulmcau  26320  ulmcn  26324  ulmdvlem1  26325  radcnvlem1  26338  radcnvle  26345  psercn  26352  pserdvlem2  26354  pserdv  26355  abelth  26367  tanregt0  26464  dvlog2lem  26577  efopn  26583  logtayllem  26584  logccv  26588  cxplt3  26625  cxpmul2zd  26641  cxpltd  26644  cxpled  26645  cxplt3d  26660  cxple3d  26661  dvsqrt  26667  cxpcn3  26674  cxpaddle  26678  cxpeq  26683  angcan  26728  angvald  26730  ang180lem2  26736  ang180  26740  isosctrlem3  26746  dquartlem1  26777  atantayl2  26864  leibpi  26868  log2tlbnd  26871  birthdaylem3  26879  xrlimcnp  26894  efrlim  26895  efrlimOLD  26896  o1cxp  26901  jensenlem2  26914  jensen  26915  fsumharmonic  26938  lgamucov  26964  lgamcvg2  26981  wilthlem1  26994  basellem3  27009  basellem6  27012  basellem8  27014  ppisval  27030  chtwordi  27082  ppiwordi  27088  mumullem2  27106  mpodvdsmulf1o  27120  dvdsmulf1o  27122  fsumvma  27140  fsumvma2  27141  chpchtsum  27146  chpub  27147  logfacubnd  27148  dchrmulcl  27176  dchrinv  27188  dchrptlem1  27191  dchrptlem2  27192  sumdchr2  27197  dchr2sum  27200  bposlem7  27217  lgslem1  27224  lgslem3  27226  lgsdirprm  27258  lgsqrlem2  27274  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem4  27305  lgseisen  27306  lgsquadlem1  27307  lgsquad2lem1  27311  lgsquad3  27314  m1lgs  27315  2sqlem7  27351  2sq2  27360  2sqmod  27363  chebbnd1lem2  27397  chebbnd1lem3  27398  rplogsumlem1  27411  rpvmasumlem  27414  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasumlema  27427  dchrisum0flblem2  27436  dchrisum0fno1  27438  dchrisum0re  27440  logdivsum  27460  pntrsumbnd2  27494  pntpbnd1a  27512  pntpbnd1  27513  pntibndlem2  27518  pntlemr  27529  pntlemj  27530  pntlemf  27532  pnt2  27540  padicabv  27557  ostth2lem2  27561  slerecd  27749  sltrecd  27751  madebday  27832  addsproplem6  27904  negsproplem6  27962  mulsproplem13  28054  mulsproplem14  28055  sltmuld  28063  mulsgt0d  28071  f1otrg  28834  brbtwn2  28868  colinearalglem2  28870  axcgrtr  28878  axcgrid  28879  axsegconlem7  28886  axsegcon  28890  ax5seglem3  28894  ax5seglem6  28897  ax5seg  28901  axpaschlem  28903  axlowdimlem17  28921  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  axcontlem8  28934  ecgrtg  28946  usgredg2v  29190  vtxdgoddnumeven  29517  2trlond  29902  eupthp1  30178  nmobndi  30737  ubthlem2  30833  ubthlem3  30834  minvecolem2  30837  shuni  31262  pjhthlem1  31353  chscllem2  31600  pjcompi  31634  mayete3i  31690  unoplin  31882  hmoplin  31904  nmophmi  31993  mdslmd4i  32295  isoun  32658  submuladdd  32696  receqid  32701  xrge0addcld  32718  xrofsup  32723  eliccelico  32733  elicoelioo  32734  difioo  32738  hashpss  32767  sgnmul  32793  rexdiv  32879  mgcmnt1d  32952  mgcmnt2d  32953  chnub  32967  xrge0addgt0  32984  cycpmcl  33071  cycpm2tr  33074  cyc3evpm  33105  cycpmconjslem2  33110  fldgensdrg  33263  qusker  33296  eqgvscpbl  33297  ringlsmss1  33343  ringlsmss2  33344  lidlmcld  33366  intlidl  33367  lidlunitel  33370  elrspunidl  33375  idlinsubrg  33378  isprmidlc  33394  rhmpreimaprmidl  33398  qsidomlem1  33399  ssdifidllem  33403  mxidlmaxv  33415  mxidlprm  33417  ssmxidllem  33420  opprmxidlabs  33434  qsdrnglem2  33443  resssra  33559  ply1degltdimlem  33594  lindsunlem  33596  sdrgfldext  33622  fldsdrgfldext  33633  finexttrb  33636  fldgenfldext  33639  fldextrspunlem1  33646  algextdeglem4  33686  algextdeglem8  33690  constrextdg2lem  33714  mdetpmtr2  33790  mdetpmtr12  33791  madjusmdetlem1  33793  madjusmdetlem4  33796  rhmpreimacn  33851  unitdivcld  33867  xrge0mulc1cn  33907  qqhnm  33956  esumcst  34029  esumfsup  34036  esumpmono  34045  esumcvg  34052  difelsiga  34099  sigapisys  34121  sigapildsys  34128  ldgenpisyslem1  34129  1stmbfm  34227  2ndmbfm  34228  dya2icoseg  34244  sibfinima  34306  probmeasb  34397  orvcgteel  34435  orvclteel  34440  ballotlemsima  34483  ballotlemfrceq  34496  ccatmulgnn0dir  34509  fct2relem  34564  ftc2re  34565  chtvalz  34596  subfacp1lem2a  35152  subfaclim  35160  erdsze2lem2  35176  cvmliftlem2  35258  cvmliftlem10  35266  cvmliftlem13  35268  cvmliftiota  35273  cvmlift2lem9  35283  cvmlift2lem11  35285  cvmlift2lem12  35286  cvmliftphtlem  35289  cvmlift3lem6  35296  cvmlift3lem7  35297  cvmlift3lem9  35299  snmlff  35301  mrsubfval  35480  wzel  35797  wsuclem  35798  brsegle  36081  opnregcld  36303  weiunfrlem  36437  fin2so  37586  poimirlem17  37616  poimirlem23  37622  opnmbllem0  37635  mblfinlem3  37638  mblfinlem4  37639  itg2addnclem  37650  itg2addnc  37653  itg2gt0cn  37654  ftc1cnnclem  37670  ftc1cnnc  37671  areacirclem5  37691  indexdom  37713  sstotbnd2  37753  isbnd3  37763  isbnd3b  37764  cntotbnd  37775  ismtyima  37782  heibor1lem  37788  heiborlem8  37797  rrncmslem  37811  reheibor  37818  lkrlsp  39080  lshpkrlem5  39092  ldualssvscl  39136  ldualssvsubcl  39137  llnmlplnN  39518  llncvrlpln  39537  pmapjat1  39832  pclfinN  39879  lautlt  40070  lauteq  40074  lautco  40076  ltrn11  40105  ltrnle  40108  ltrneq2  40127  cdlemednuN  40279  cdleme20k  40298  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21c  40306  cdleme22e  40323  cdleme22eALTN  40324  cdlemefrs32fva  40379  cdlemg4g  40595  cdlemg18b  40658  cdlemg18c  40659  cdlemj3  40802  dia2dimlem5  41047  dvhopN  41095  cdlemm10N  41097  dihjatcclem4  41400  dochexmidlem2  41440  lclkrlem2o  41500  lcfrlem5  41525  lcfrlem6  41526  lcdlssvscl  41585  mapdpglem6  41657  mapdpglem9  41659  mapdpglem12  41662  mapdpglem14  41664  mapdindp0  41698  hdmaprnlem7N  41834  hdmaprnlem8N  41835  hdmaprnlem3eN  41837  hgmapvvlem3  41904  dvun  42332  addinvcom  42405  evlsaddval  42541  evlsmulval  42542  evladdval  42548  evlmulval  42549  mzpsubst  42721  eldioph2lem1  42733  eldioph2lem2  42734  eldioph2b  42736  diophin  42745  irrapxlem2  42796  irrapxlem4  42798  irrapxlem5  42799  pellexlem1  42802  pellexlem2  42803  pellexlem6  42807  elpell1qr2  42845  pell1qrgaplem  42846  pell1qrgap  42847  pellqrex  42852  pellfundex  42859  pellfund14  42871  rmspecsqrtnq  42879  rmxyadd  42894  congsub  42943  mzpcong  42945  congrep  42946  acongtr  42951  acongrep  42953  jm2.19lem1  42962  jm2.22  42968  jm2.23  42969  jm2.26lem3  42974  jm2.26  42975  jm2.27a  42978  fnwe2lem2  43024  aomclem6  43032  hbtlem2  43097  hbtlem4  43099  hbtlem5  43101  dgraa0p  43122  rngunsnply  43142  proot1hash  43168  nnoeomeqom  43285  cantnf2  43298  omabs2  43305  naddcnff  43335  naddcnffo  43337  naddcnfcom  43339  naddcnfid1  43340  expgrowth  44308  fpmd  45241  abslt2sqd  45340  ioondisj2  45475  ioondisj1  45476  eliocre  45491  ioossioobi  45499  iooiinicc  45524  iooiinioc  45538  lptioo2  45613  limcresiooub  45624  limsupequzlem  45704  xlimmnfvlem2  45815  xlimpnfvlem2  45819  cncfuni  45868  cncfiooicclem1  45875  cxpcncf2  45881  dvcnre  45898  dvresntr  45900  dvresioo  45903  dvbdfbdioolem1  45910  dvnmptdivc  45920  dvnxpaek  45924  itgsinexplem1  45936  itgcoscmulx  45951  itgiccshift  45962  itgperiod  45963  ovolsplit  45970  stoweidlem11  45993  stoweidlem26  46008  stoweidlem34  46016  stoweidlem36  46018  stoweidlem38  46020  stirlinglem5  46060  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem20  46109  fourierdlem58  46146  fourierdlem72  46160  fourierdlem73  46161  fourierdlem74  46162  fourierdlem75  46163  fourierdlem76  46164  fourierdlem79  46167  fourierdlem80  46168  fourierdlem87  46175  fourierdlem94  46182  fourierdlem103  46191  fourierdlem104  46192  fourierdlem107  46195  fourierdlem113  46201  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  etransclem46  46262  etransclem47  46263  rrndistlt  46272  rrnprjdstle  46283  ioorrnopnxrlem  46288  sge0ssre  46379  sge0seq  46428  hsphoidmvle2  46567  hsphoidmvle  46568  hoidmv1lelem1  46573  hoidmv1lelem2  46574  hoidmv1lelem3  46575  hoidmvlelem1  46577  hoidifhspdmvle  46602  hoiqssbllem2  46605  ovolval5lem2  46635  iinhoiicc  46656  iunhoiioo  46658  vonioolem2  46663  vonicclem2  46666  issmflem  46709  submodlt  47335  iccpartdisj  47422  m1expevenALTV  47632  fpprel2  47726  tgoldbach  47802  opstrgric  47911  gpg3kgrtriex  48074  nn0eo  48514  fdivpm  48529  refdivpm  48530  elbigolo1  48543  logbpw2m1  48553  fllog2  48554  dignn0flhalflem1  48601  dignn0flhalflem2  48602  itsclinecirc0in  48761  2itscplem2  48765  itscnhlinecirc02plem1  48768  iccdisj2  48882
  Copyright terms: Public domain W3C validator