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

Theorem syl22anc 1186
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl22anc.5  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta ) )  ->  et )
Assertion
Ref Expression
syl22anc  |-  ( ph  ->  et )

Proof of Theorem syl22anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 520 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylXanc.3 . 2  |-  ( ph  ->  th )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl22anc.5 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta ) )  ->  et )
73, 4, 5, 6syl12anc 1183 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  fr2nr  4561  fr3nr  4761  soltmin  5274  f1oprg  5719  fveqf1o  6030  weniso  6076  smogt  6630  smorndom  6631  oacomf1o  6809  th3qlem1  7011  difsnen  7191  undom  7197  domss2  7267  ssenen  7282  marypha1lem  7439  fisupcl  7473  ordtypelem3  7490  ordtypelem8  7495  oieu  7509  oismo  7510  wofib  7515  wemaplem2  7517  wemapso  7521  wemapso2  7522  unxpwdom2  7557  infdifsn  7612  cantnf  7650  cnfcom3  7662  r1ordg  7705  dif1card  7893  infxpenlem  7896  dfac8clem  7914  infxp  8096  infmap2  8099  cflim2  8144  coftr  8154  fin2i2  8199  enfin2i  8202  fin23lem26  8206  fin23lem27  8209  fin23lem40  8232  isf32lem2  8235  isf32lem3  8236  isf32lem4  8237  isf32lem7  8240  isf32lem9  8242  fin1a2lem13  8293  fin12  8294  alephexp1  8455  gchdomtri  8505  fpwwe2lem12  8517  fpwwe2lem13  8518  gchhar  8547  gchpwdom  8550  adderpqlem  8832  mulerpqlem  8833  addassnq  8836  mulassnq  8837  distrnq  8839  mulidnq  8841  recmulnq  8842  ltexnq  8853  distrlem1pr  8903  distrlem4pr  8904  prlem936  8925  reclem3pr  8927  mulgt0d  9226  mul4d  9279  add4d  9290  add42d  9291  subcan  9357  addsub4d  9459  subadd4d  9460  sub4d  9461  2addsubd  9462  addsubeq4d  9463  muladdd  9492  mulsubd  9493  addgegt0d  9601  addge0d  9603  mulge0d  9604  le2addd  9645  le2subd  9646  ltleaddd  9647  leltaddd  9648  lt2subd  9650  divdivdiv  9716  divcan5  9717  divne0d  9807  recdivd  9808  recdiv2d  9809  divcan6d  9810  ddcand  9811  rec11d  9812  divmuldivd  9832  divmul13d  9833  divmul24d  9834  divadddivd  9835  divsubdivd  9836  divmuleqd  9837  divdivdivd  9838  subrecd  9846  recreclt  9910  divgt0d  9947  mulgt1d  9948  lemulge11d  9949  lemulge12d  9950  ltmul12ad  9953  lemul12ad  9954  lemul12bd  9955  supmul1  9974  nndivtr  10042  qreccl  10595  ledivdivd  10674  lediv12ad  10704  lt2mul2divd  10707  xlt2add  10840  supxrun  10895  supxrre  10907  infmxrre  10915  iccss2  10982  iccssico2  10985  lincmb01cmp  11039  iccf1o  11040  fzrev2i  11111  modsubdir  11286  fzennn  11308  sermono  11356  mulexpz  11421  expaddz  11425  ltexp2a  11432  leexp2a  11436  sqdiv  11448  expmulnbnd  11512  digit1  11514  expsubd  11535  lt2sqd  11558  le2sqd  11559  sq11d  11560  bcm1k  11607  bcp1n  11608  bcp1nk  11609  hashf1lem1  11705  absrele  12114  sqreulem  12164  sqrmuld  12228  sqrsq2d  12229  sqrled  12230  sqrltd  12231  sqr11d  12232  abs3lemd  12264  rlimuni  12345  climuni  12347  lo1resb  12359  o1resb  12361  2clim  12367  addcn2  12388  mulcn2  12390  o1of2  12407  o1rlimmul  12413  lo1add  12421  lo1mul  12422  isercolllem1  12459  caucvgrlem  12467  iseraltlem2  12477  iseraltlem3  12478  iseralt  12479  fsumrev  12563  fsumshft  12564  fsum0diag2  12567  binomlem  12609  climcndslem1  12630  climcndslem2  12631  harmonic  12639  mertenslem1  12662  efcllem  12681  moddvds  12860  dvds1  12899  dvdsext  12901  oexpneg  12912  bitsinv1  12955  sadaddlem  12979  sadasslem  12983  sadeq  12985  mulgcd  13047  dvdssqlem  13060  rpmulgcd2  13106  isprm6  13110  isprm5  13113  crt  13168  eulerthlem2  13172  prmdiveq  13176  pythagtriplem11  13200  pythagtriplem13  13202  iserodd  13210  pcgcd1  13251  pcprmpw2  13256  pcaddlem  13258  fldivp1  13267  4sqlem12  13325  4sqlem14  13327  4sqlem15  13328  4sqlem16  13329  vdwapun  13343  mreexexlem4d  13873  acsfn1  13887  acsfn2  13889  sscpwex  14016  rescabs  14034  catciso  14263  yonedainv  14379  p0le  14473  ple1  14474  subm0  14757  odmodnn0  15179  odeq  15189  dfod2  15201  sylow1lem1  15233  lsmsubg  15289  lsmmod  15308  lsmdisj2  15315  ghmplusg  15462  odadd  15466  gexexlem  15468  lt6abl  15505  cyggex2  15507  ablfacrp  15625  ablfacrp2  15626  ablfac1c  15630  ablfac1eu  15632  lssvancl1  16022  lssvnegcl  16033  lspprvacl  16076  lspsneli  16078  lspsn  16079  lmhmplusg  16121  lmhmima  16124  lmhmpreima  16125  reslmhm  16129  lbsind2  16154  lsmcl  16156  lsmelval2  16158  lsppreli  16163  lspprabs  16168  pj1lmhm  16173  lssvs0or  16183  lspabs3  16194  lspfixed  16201  lspexch  16202  lsmcv  16214  lspsolv  16216  lidlmcl  16289  drngnidl  16301  2idlcpbl  16306  mplbas2  16532  coe1addfv  16659  gzrngunit  16765  zlpirlem3  16771  prmirredlem  16774  znf1o  16833  znunithash  16846  ntrin  17126  topssnei  17189  restbas  17223  restntr  17247  cnntri  17336  fiuncmp  17468  nllyrest  17550  nllyidm  17553  hausllycmp  17558  cldllycmp  17559  hauspwdom  17565  txcld  17636  txcn  17659  txlly  17669  txnlly  17670  txhaus  17680  txlm  17681  txkgen  17685  xkococnlem  17692  cnmpt2res  17710  xkoinjcn  17720  basqtop  17744  qtopeu  17749  qtophmeo  17850  trfbas2  17876  neifil  17913  hausflim  18014  alexsubALTlem2  18080  cnextfval  18094  cnextfvval  18097  cnextf  18098  clssubg  18139  utop2nei  18281  utop3cls  18282  utopreg  18283  psmetlecl  18347  xmetlecl  18377  prdsxmetlem  18399  bldisj  18429  imasf1obl  18519  prdsbl  18522  stdbdmet  18547  stdbdmopn  18549  met2ndci  18553  metcnp  18572  metusttoOLD  18588  metustto  18589  metustexhalfOLD  18594  metustexhalf  18595  cfilucfilOLD  18600  cfilucfil  18601  metucnOLD  18619  metucn  18620  lssnlm  18737  nmotri  18774  nmoid  18777  tgioo  18828  blcvx  18830  xrsmopn  18844  reperflem  18850  reconnlem2  18859  opnreen  18863  metdsge  18880  metdsre  18884  metdscnlem  18886  metnrmlem1a  18889  metnrmlem1  18890  metnrmlem3  18892  cncfmet  18939  cnmpt2pc  18954  icopnfcnv  18968  icopnfhmeo  18969  cnllycmp  18982  evth  18985  lebnumii  18992  nmoleub2lem3  19124  iscfil2  19220  cfil3i  19223  iscfil3  19227  cfilfcls  19228  iscau3  19232  iscmet3lem2  19246  caubl  19261  lmcau  19266  minveclem2  19328  pjthlem1  19339  pjthlem2  19340  ivthicc  19356  ovollecl  19380  ovolunlem1a  19393  ovolunnul  19397  ovoliunlem1  19399  ismbl2  19424  nulmbl2  19432  unmbl  19433  volun  19440  voliunlem2  19446  ioombl1lem2  19454  uniioombllem2a  19475  uniioombllem3  19478  uniioombllem4  19479  dyaddisjlem  19488  dyadmaxlem  19490  opnmbllem  19494  volsup2  19498  volcn  19499  ismbfd  19533  mbfi1fseqlem1  19608  mbfi1fseqlem5  19612  itg2lecl  19631  itg2monolem2  19644  itg2gt0  19653  itgspliticc  19729  ellimc3  19767  limcres  19774  dvfval  19785  dvres3  19801  dvres3a  19802  dvnff  19810  dvnadd  19816  dvn2bss  19817  dvnres  19818  dvcmul  19831  dvcmulf  19832  dvmptres3  19843  dvmptres2  19849  dvmptntr  19858  dvexp3  19863  dvferm1lem  19869  dvlip  19878  dvlipcn  19879  dvlip2  19880  c1liplem1  19881  dvgt0lem1  19887  dvgt0lem2  19888  dvne0  19896  lhop1lem  19898  lhop2  19900  lhop  19901  dvcnvrelem1  19902  dvcnvrelem2  19903  dvcvx  19905  dvfsumle  19906  dvfsumabs  19908  dvfsumlem2  19912  ftc1lem6  19926  ftc1  19927  ftc2ditglem  19930  itgsubstlem  19933  evlslem3  19936  evlslem1  19937  evl1addd  19955  evl1subd  19956  evl1muld  19957  mdegaddle  19998  mdegmullem  20002  ply1rem  20087  fta1glem2  20090  fta1blem  20092  ig1peu  20095  ig1pdvds  20100  dgrmulc  20190  dgrcolem1  20192  plydivlem4  20214  plydiveu  20216  fta1lem  20225  vieta1lem1  20228  vieta1lem2  20229  plyexmo  20231  taylfvallem1  20274  taylfval  20276  tayl0  20279  taylplem1  20280  taylply2  20285  taylply  20286  dvtaylp  20287  dvntaylp  20288  dvntaylp0  20289  taylthlem1  20290  taylthlem2  20291  ulmcaulem  20311  ulmcau  20312  ulmcn  20316  ulmdvlem1  20317  radcnvlem1  20330  radcnvle  20337  psercn  20343  pserdvlem2  20345  pserdv  20346  abelth  20358  cosordlem  20434  tanregt0  20442  dvlog2lem  20544  efopn  20550  logtayllem  20551  logccv  20555  cxplt3  20592  cxpmul2zd  20608  cxpltd  20611  cxpled  20612  cxplt3d  20624  cxple3d  20625  dvsqr  20629  cxpcn3  20633  cxpaddle  20637  cxpeq  20642  angcan  20645  angvald  20647  ang180lem2  20653  ang180  20657  isosctrlem3  20665  dquartlem1  20692  atantayl2  20779  leibpilem1  20781  leibpi  20783  log2tlbnd  20786  birthdaylem3  20793  xrlimcnp  20808  efrlim  20809  o1cxp  20814  jensenlem2  20827  jensen  20828  fsumharmonic  20851  wilthlem1  20852  basellem3  20866  basellem6  20869  basellem8  20871  ppisval  20887  chtwordi  20940  ppiwordi  20946  mumullem2  20964  dvdsmulf1o  20980  fsumvma  20998  fsumvma2  20999  chpchtsum  21004  chpub  21005  logfacubnd  21006  dchrmulcl  21034  dchrinv  21046  dchrptlem1  21049  dchrptlem2  21050  sumdchr2  21055  dchr2sum  21058  bposlem7  21075  lgslem1  21081  lgslem3  21083  lgsdirprm  21114  lgsqrlem2  21127  lgseisenlem1  21134  lgseisenlem2  21135  lgseisenlem4  21137  lgseisen  21138  lgsquadlem1  21139  lgsquad2lem1  21143  lgsquad3  21146  m1lgs  21147  2sqlem7  21155  chebbnd1lem2  21165  chebbnd1lem3  21166  rplogsumlem1  21179  rpvmasumlem  21182  dchrvmasumlem1  21190  dchrvmasum2lem  21191  dchrvmasumlema  21195  dchrisum0flblem2  21204  dchrisum0fno1  21206  dchrisum0re  21208  logdivsum  21228  pntrsumbnd2  21262  pntpbnd1a  21280  pntpbnd1  21281  pntibndlem2  21286  pntlemr  21297  pntlemj  21298  pntlemf  21300  pnt2  21308  padicabv  21325  ostth2lem2  21329  usgraidx2v  21413  iseupa  21688  eupap1  21699  eupath2lem3  21702  nmobndi  22277  ubthlem2  22374  ubthlem3  22375  minvecolem2  22378  shuni  22803  pjhthlem1  22894  chscllem2  23141  pjcompi  23175  mayete3i  23231  mayete3iOLD  23232  unoplin  23424  hmoplin  23446  nmophmi  23535  mdslmd4i  23837  preqsnd  24001  isoun  24090  xrofsup  24127  eliccelico  24141  elicoelioo  24142  difioo  24146  rexdiv  24173  xrge0addgt0  24215  ofldchr  24245  unitdivcld  24300  xrge0mulc1cn  24328  qqhnm  24375  esumcst  24456  esumfsup  24461  esumpmono  24470  esumcvg  24477  difelsiga  24517  1stmbfm  24611  2ndmbfm  24612  dya2icoseg  24628  probmeasb  24689  orvcgteel  24726  orvclteel  24731  ballotlemsima  24774  ballotlemfrceq  24787  lgamucov  24823  lgamcvg2  24840  subfacp1lem2a  24867  subfaclim  24875  erdsze2lem2  24891  cvmliftlem2  24974  cvmliftlem10  24982  cvmliftlem13  24984  cvmliftiota  24989  cvmlift2lem9  24999  cvmlift2lem11  25001  cvmlift2lem12  25002  cvmliftphtlem  25005  cvmlift3lem6  25012  cvmlift3lem7  25013  cvmlift3lem9  25015  snmlff  25017  mulge0b  25192  fprodser  25276  fprodshft  25301  fprodrev  25302  rprisefaccl  25340  trpredelss  25511  trpredpo  25514  wzel  25576  wsuclem  25577  nodenselem5  25641  nobndlem6  25653  brbtwn2  25845  colinearalglem2  25847  axcgrtr  25855  axcgrid  25856  axsegconlem7  25863  axsegcon  25867  ax5seglem3  25871  ax5seglem6  25874  ax5seg  25878  axpaschlem  25880  axlowdimlem17  25898  axcontlem2  25905  axcontlem4  25907  axcontlem7  25910  axcontlem8  25911  brsegle  26043  opnmbllem0  26243  mblfinlem3  26246  mblfinlem4  26247  itg2addnclem  26257  itg2addnc  26260  itg2gt0cn  26261  ftc1cnnclem  26279  ftc1cnnc  26280  areacirclem5  26297  opnregcld  26334  indexdom  26437  sstotbnd2  26484  isbnd3  26494  isbnd3b  26495  cntotbnd  26506  ismtyima  26513  heibor1lem  26519  heiborlem8  26528  rrncmslem  26542  reheibor  26549  lcomfsup  26748  mzpsubst  26806  eldioph2lem1  26819  eldioph2lem2  26820  eldioph2b  26822  diophin  26832  irrapxlem2  26887  irrapxlem4  26889  irrapxlem5  26890  pellexlem1  26893  pellexlem2  26894  pellexlem6  26898  elpell1qr2  26936  pell1qrgaplem  26937  pell1qrgap  26938  pellqrex  26943  pellfundex  26950  pellfund14  26962  rmspecsqrnq  26970  rmxyadd  26985  expmordi  27011  rmxypos  27013  jm2.24  27029  congsub  27036  mzpcong  27038  congrep  27039  acongtr  27044  acongrep  27046  jm2.19lem1  27061  jm2.22  27067  jm2.23  27068  jm2.26lem3  27073  jm2.26  27074  jm2.27a  27077  fnwe2lem2  27127  aomclem6  27135  frlmvscaval  27209  frlmssuvc1  27224  frlmsslsp  27226  frlmup1  27228  frlmup2  27229  enfixsn  27235  lindfind2  27266  lindfrn  27269  f1lindf  27270  islindf4  27286  hbtlem2  27306  hbtlem4  27308  hbtlem5  27310  dgraa0p  27332  rngunsnply  27356  pmtrff1o  27382  pmtrfcnv  27383  pmtrfb  27384  psgnunilem1  27394  mamudi  27439  mamudir  27440  acsfn1p  27485  proot1hash  27497  expgrowth  27530  itgsinexplem1  27725  stoweidlem11  27737  stoweidlem26  27752  stoweidlem34  27760  stoweidlem36  27762  stoweidlem38  27764  stirlinglem5  27804  cshw1  28276  lkrlsp  29901  lshpkrlem5  29913  ldualssvscl  29957  ldualssvsubcl  29958  llnmlplnN  30337  llncvrlpln  30356  pmapjat1  30651  pclfinN  30698  lautlt  30889  lauteq  30893  lautco  30895  ltrn11  30924  ltrnle  30927  ltrneq2  30946  cdlemednuN  31098  cdleme20k  31117  cdleme20l2  31119  cdleme20l  31120  cdleme20m  31121  cdleme21c  31125  cdleme22e  31142  cdleme22eALTN  31143  cdlemefrs32fva  31198  cdlemg4g  31414  cdlemg18b  31477  cdlemg18c  31478  cdlemj3  31621  dia2dimlem5  31867  dvhopN  31915  cdlemm10N  31917  dihjatcclem4  32220  dochexmidlem2  32260  lclkrlem2o  32320  lcfrlem5  32345  lcfrlem6  32346  lcdlssvscl  32405  mapdpglem6  32477  mapdpglem9  32479  mapdpglem12  32482  mapdpglem14  32484  mapdindp0  32518  hdmaprnlem7N  32657  hdmaprnlem8N  32658  hdmaprnlem3eN  32660  hgmapvvlem3  32727
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator