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

Theorem syl22anc 1183
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 518 . 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 1180 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fr2nr  4387  fr3nr  4587  soltmin  5098  fveqf1o  5822  weniso  5868  smogt  6400  smorndom  6401  oacomf1o  6579  th3qlem1  6780  difsnen  6960  undom  6966  domss2  7036  ssenen  7051  marypha1lem  7202  fisupcl  7234  ordtypelem3  7251  ordtypelem8  7256  oieu  7270  oismo  7271  wofib  7276  wemaplem2  7278  wemapso  7282  wemapso2  7283  unxpwdom2  7318  infdifsn  7373  cantnf  7411  cnfcom3  7423  r1ordg  7466  dif1card  7654  infxpenlem  7657  dfac8clem  7675  infxp  7857  infmap2  7860  cflim2  7905  coftr  7915  fin2i2  7960  enfin2i  7963  fin23lem26  7967  fin23lem27  7970  fin23lem40  7993  isf32lem2  7996  isf32lem3  7997  isf32lem4  7998  isf32lem7  8001  isf32lem9  8003  fin1a2lem13  8054  fin12  8055  alephexp1  8217  gchdomtri  8267  fpwwe2lem12  8279  fpwwe2lem13  8280  gchhar  8309  gchpwdom  8312  adderpqlem  8594  mulerpqlem  8595  addassnq  8598  mulassnq  8599  distrnq  8601  mulidnq  8603  recmulnq  8604  ltexnq  8615  distrlem1pr  8665  distrlem4pr  8666  prlem936  8687  reclem3pr  8689  mulgt0d  8987  mul4d  9040  add4d  9051  add42d  9052  subcan  9118  addsub4d  9220  subadd4d  9221  sub4d  9222  2addsubd  9223  addsubeq4d  9224  muladdd  9253  mulsubd  9254  addgegt0d  9362  addge0d  9364  mulge0d  9365  le2addd  9406  le2subd  9407  ltleaddd  9408  leltaddd  9409  lt2subd  9411  divdivdiv  9477  divcan5  9478  divne0d  9568  recdivd  9569  recdiv2d  9570  divcan6d  9571  ddcand  9572  rec11d  9573  divmuldivd  9593  divmul13d  9594  divmul24d  9595  divadddivd  9596  divsubdivd  9597  divmuleqd  9598  divdivdivd  9599  subrecd  9607  recreclt  9671  divgt0d  9708  mulgt1d  9709  lemulge11d  9710  lemulge12d  9711  ltmul12ad  9714  lemul12ad  9715  lemul12bd  9716  supmul1  9735  nndivtr  9803  qreccl  10352  ledivdivd  10431  lediv12ad  10461  lt2mul2divd  10464  xlt2add  10596  supxrun  10650  supxrre  10662  infmxrre  10670  iccss2  10736  iccssico2  10739  lincmb01cmp  10793  iccf1o  10794  fzrev2i  10864  modsubdir  11024  fzennn  11046  sermono  11094  mulexpz  11158  expaddz  11162  ltexp2a  11169  leexp2a  11173  sqdiv  11185  expmulnbnd  11249  digit1  11251  expsubd  11272  lt2sqd  11295  le2sqd  11296  sq11d  11297  bcm1k  11343  bcp1n  11344  bcp1nk  11345  hashf1lem1  11409  absrele  11809  sqreulem  11859  sqrmuld  11923  sqrsq2d  11924  sqrled  11925  sqrltd  11926  sqr11d  11927  abs3lemd  11959  rlimuni  12040  climuni  12042  lo1resb  12054  o1resb  12056  2clim  12062  addcn2  12083  mulcn2  12085  o1of2  12102  o1rlimmul  12108  lo1add  12116  lo1mul  12117  isercolllem1  12154  caucvgrlem  12161  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  fsumrev  12257  fsumshft  12258  fsum0diag2  12261  binomlem  12303  climcndslem1  12324  climcndslem2  12325  harmonic  12333  mertenslem1  12356  efcllem  12375  moddvds  12554  dvds1  12593  dvdsext  12595  oexpneg  12606  bitsinv1  12649  sadaddlem  12673  sadasslem  12677  sadeq  12679  mulgcd  12741  dvdssqlem  12754  rpmulgcd2  12800  isprm6  12804  isprm5  12807  crt  12862  eulerthlem2  12866  prmdiveq  12870  pythagtriplem11  12894  pythagtriplem13  12896  iserodd  12904  pcgcd1  12945  pcprmpw2  12950  pcaddlem  12952  fldivp1  12961  4sqlem12  13019  4sqlem14  13021  4sqlem15  13022  4sqlem16  13023  vdwapun  13037  mreexexlem4d  13565  acsfn1  13579  acsfn2  13581  sscpwex  13708  rescabs  13726  catciso  13955  yonedainv  14071  p0le  14165  ple1  14166  subm0  14449  odmodnn0  14871  odeq  14881  dfod2  14893  sylow1lem1  14925  lsmsubg  14981  lsmmod  15000  lsmdisj2  15007  ghmplusg  15154  odadd  15158  gexexlem  15160  lt6abl  15197  cyggex2  15199  ablfacrp  15317  ablfacrp2  15318  ablfac1c  15322  ablfac1eu  15324  lssvancl1  15718  lssvnegcl  15729  lspprvacl  15772  lspsneli  15774  lspsn  15775  lmhmplusg  15817  lmhmima  15820  lmhmpreima  15821  reslmhm  15825  lbsind2  15850  lsmcl  15852  lsmelval2  15854  lsppreli  15859  lspprabs  15864  pj1lmhm  15869  lssvs0or  15879  lspabs3  15890  lspfixed  15897  lspexch  15898  lsmcv  15910  lspsolv  15912  lidlmcl  15985  drngnidl  15997  2idlcpbl  16002  mplbas2  16228  coe1addfv  16358  gzrngunit  16453  zlpirlem3  16459  prmirredlem  16462  znf1o  16521  znunithash  16534  ntrin  16814  topssnei  16877  restbas  16905  restntr  16928  cnntri  17016  fiuncmp  17147  nllyrest  17228  nllyidm  17231  hausllycmp  17236  cldllycmp  17237  hauspwdom  17243  txcld  17314  txcn  17336  txlly  17346  txnlly  17347  txhaus  17357  txlm  17358  txkgen  17362  xkococnlem  17369  cnmpt2res  17387  xkoinjcn  17397  basqtop  17418  qtopeu  17423  qtophmeo  17524  trfbas2  17554  neifil  17591  hausflim  17692  alexsubALTlem2  17758  clssubg  17807  xmetlecl  17927  prdsxmetlem  17948  bldisj  17971  imasf1obl  18050  prdsbl  18053  stdbdmet  18078  stdbdmopn  18080  met2ndci  18084  metcnp  18103  lssnlm  18227  nmotri  18264  nmoid  18267  tgioo  18318  blcvx  18320  xrsmopn  18334  reperflem  18339  reconnlem2  18348  opnreen  18352  metdsge  18369  metdsre  18373  metdscnlem  18375  metnrmlem1a  18378  metnrmlem1  18379  metnrmlem3  18381  cncfmet  18428  cnmpt2pc  18442  icopnfcnv  18456  icopnfhmeo  18457  cnllycmp  18470  evth  18473  lebnumii  18480  nmoleub2lem3  18612  iscfil2  18708  cfil3i  18711  iscfil3  18715  cfilfcls  18716  iscau3  18720  iscmet3lem2  18734  caubl  18749  lmcau  18754  minveclem2  18806  pjthlem1  18817  pjthlem2  18818  ivthicc  18834  ovollecl  18858  ovolunlem1a  18871  ovolunnul  18875  ovoliunlem1  18877  ismbl2  18902  nulmbl2  18910  unmbl  18911  volun  18918  voliunlem2  18924  ioombl1lem2  18932  uniioombllem2a  18953  uniioombllem3  18956  uniioombllem4  18957  dyaddisjlem  18966  dyadmaxlem  18968  opnmbllem  18972  volsup2  18976  volcn  18977  ismbfd  19011  mbfi1fseqlem1  19086  mbfi1fseqlem5  19090  itg2lecl  19109  itg2monolem2  19122  itg2gt0  19131  itgspliticc  19207  ellimc3  19245  limcres  19252  dvfval  19263  dvres3  19279  dvres3a  19280  dvnff  19288  dvnadd  19294  dvn2bss  19295  dvnres  19296  dvcmul  19309  dvcmulf  19310  dvmptres3  19321  dvmptres2  19327  dvmptntr  19336  dvexp3  19341  dvferm1lem  19347  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  dvgt0lem1  19365  dvgt0lem2  19366  dvne0  19374  lhop1lem  19376  lhop2  19378  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcvx  19383  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  ftc1lem6  19404  ftc1  19405  ftc2ditglem  19408  itgsubstlem  19411  evlslem3  19414  evlslem1  19415  evl1addd  19433  evl1subd  19434  evl1muld  19435  mdegaddle  19476  mdegmullem  19480  ply1rem  19565  fta1glem2  19568  fta1blem  19570  ig1peu  19573  ig1pdvds  19578  dgrmulc  19668  dgrcolem1  19670  plydivlem4  19692  plydiveu  19694  fta1lem  19703  vieta1lem1  19706  vieta1lem2  19707  plyexmo  19709  taylfvallem1  19752  taylfval  19754  tayl0  19757  taylplem1  19758  taylply2  19763  taylply  19764  dvtaylp  19765  dvntaylp  19766  dvntaylp0  19767  taylthlem1  19768  taylthlem2  19769  ulmcaulem  19787  ulmcau  19788  ulmcn  19792  ulmdvlem1  19793  radcnvlem1  19805  radcnvle  19812  psercn  19818  pserdvlem2  19820  pserdv  19821  abelth  19833  cosordlem  19909  tanregt0  19917  dvlog2lem  20015  efopn  20021  logtayllem  20022  logccv  20026  cxplt3  20063  cxpmul2zd  20079  cxpltd  20082  cxpled  20083  cxplt3d  20095  cxple3d  20096  dvsqr  20100  cxpcn3  20104  cxpaddle  20108  cxpeq  20113  angcan  20116  angvald  20118  ang180lem2  20124  ang180lem4  20126  ang180  20128  lawcos  20130  isosctrlem3  20136  dquartlem1  20163  atantayl2  20250  leibpilem1  20252  leibpi  20254  log2tlbnd  20257  birthdaylem3  20264  xrlimcnp  20279  efrlim  20280  o1cxp  20285  jensenlem2  20298  jensen  20299  fsumharmonic  20321  wilthlem1  20322  basellem3  20336  basellem6  20339  basellem8  20341  ppisval  20357  chtwordi  20410  ppiwordi  20416  mumullem2  20434  dvdsmulf1o  20450  fsumvma  20468  fsumvma2  20469  chpchtsum  20474  chpub  20475  logfacubnd  20476  dchrmulcl  20504  dchrinv  20516  dchrptlem1  20519  dchrptlem2  20520  sumdchr2  20525  dchr2sum  20528  bposlem7  20545  lgslem1  20551  lgslem3  20553  lgsdirprm  20584  lgsqrlem2  20597  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem4  20607  lgseisen  20608  lgsquadlem1  20609  lgsquad2lem1  20613  lgsquad3  20616  m1lgs  20617  2sqlem7  20625  chebbnd1lem2  20635  chebbnd1lem3  20636  rplogsumlem1  20649  rpvmasumlem  20652  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrvmasumlema  20665  dchrisum0flblem2  20674  dchrisum0fno1  20676  dchrisum0re  20678  logdivsum  20698  pntrsumbnd2  20732  pntpbnd1a  20750  pntpbnd1  20751  pntibndlem2  20756  pntlemr  20767  pntlemj  20768  pntlemf  20770  pnt2  20778  padicabv  20795  ostth2lem2  20799  nmobndi  21369  ubthlem2  21466  ubthlem3  21467  minvecolem2  21470  shuni  21895  pjhthlem1  21986  chscllem2  22233  pjcompi  22267  mayete3i  22323  mayete3iOLD  22324  unoplin  22516  hmoplin  22538  nmophmi  22627  mdslmd4i  22929  ballotlemsima  23090  ballotlemfrceq  23103  rexdiv  23125  preqsnd  23209  isoun  23257  xrofsup  23270  eliccelico  23285  elicoelioo  23286  difioo  23290  unitdivcld  23300  xrge0mulc1cn  23338  xrge0addgt0  23346  esumcst  23451  esumpcvgval  23461  esumpmono  23462  esumcvg  23469  difelsiga  23509  dya2iocseg  23594  probmeasb  23648  orvcgteel  23683  orvclteel  23688  subfacp1lem2a  23726  subfaclim  23734  erdsze2lem2  23750  cvmliftlem2  23832  cvmliftlem10  23840  cvmliftlem13  23842  cvmliftiota  23847  cvmlift2lem9  23857  cvmlift2lem11  23859  cvmlift2lem12  23860  cvmliftphtlem  23863  cvmlift3lem6  23870  cvmlift3lem7  23871  cvmlift3lem9  23873  iseupa  23896  eupap1  23915  eupath2lem3  23918  snmlff  23927  mulge0b  24101  faclimlem6  24122  faclimlem9  24125  trpredelss  24306  trpredpo  24309  nodenselem5  24410  nobndlem6  24422  brbtwn2  24605  colinearalglem2  24607  axcgrtr  24615  axcgrid  24616  axsegconlem7  24623  axsegcon  24627  ax5seglem3  24631  ax5seglem6  24634  ax5seg  24638  axpaschlem  24640  axlowdimlem17  24658  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  brsegle  24803  bpoly3  24865  itg2addnclem  25003  itg2gt0cn  25006  ftc1cnnclem  25024  ftc1cnnc  25025  areacirclem6  25033  infxpg  25198  curgrpact  25475  limptlimpr2lem1  25677  limptlimpr2lem2  25678  cntrset  25705  opnregcld  26351  indexdom  26516  sstotbnd2  26601  isbnd3  26611  isbnd3b  26612  cntotbnd  26623  ismtyima  26630  heibor1lem  26636  heiborlem8  26645  rrncmslem  26659  reheibor  26666  lcomfsup  26871  mzpsubst  26929  eldioph2lem1  26942  eldioph2lem2  26943  eldioph2b  26945  diophin  26955  irrapxlem2  27011  irrapxlem4  27013  irrapxlem5  27014  pellexlem1  27017  pellexlem2  27018  pellexlem6  27022  elpell1qr2  27060  pell1qrgaplem  27061  pell1qrgap  27062  pellqrex  27067  pellfundex  27074  pellfund14  27086  rmspecsqrnq  27094  rmxyadd  27109  expmordi  27135  rmxypos  27137  jm2.24  27153  congsub  27160  mzpcong  27162  congrep  27163  acongtr  27168  acongrep  27170  jm2.19lem1  27185  jm2.22  27191  jm2.23  27192  jm2.26lem3  27197  jm2.26  27198  jm2.27a  27201  fnwe2lem2  27251  aomclem6  27259  frlmvscaval  27334  frlmssuvc1  27349  frlmsslsp  27351  frlmup1  27353  frlmup2  27354  enfixsn  27360  lindfind2  27391  lindfrn  27394  f1lindf  27395  islindf4  27411  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  dgraa0p  27457  rngunsnply  27481  pmtrff1o  27507  pmtrfcnv  27508  pmtrfb  27509  psgnunilem1  27519  mamudi  27564  mamudir  27565  acsfn1p  27610  proot1hash  27622  expgrowth  27655  f1oprg  28186  lkrlsp  29914  lshpkrlem5  29926  ldualssvscl  29970  ldualssvsubcl  29971  llnmlplnN  30350  llncvrlpln  30369  pmapjat1  30664  pclfinN  30711  lautlt  30902  lauteq  30906  lautco  30908  ltrn11  30937  ltrnle  30940  ltrneq2  30959  cdlemednuN  31111  cdleme20k  31130  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21c  31138  cdleme22e  31155  cdleme22eALTN  31156  cdlemefrs32fva  31211  cdlemg4g  31427  cdlemg18b  31490  cdlemg18c  31491  cdlemj3  31634  dia2dimlem5  31880  dvhopN  31928  cdlemm10N  31930  dihjatcclem4  32233  dochexmidlem2  32273  lclkrlem2o  32333  lcfrlem5  32358  lcfrlem6  32359  lcdlssvscl  32418  mapdpglem6  32490  mapdpglem9  32492  mapdpglem12  32495  mapdpglem14  32497  mapdindp0  32531  hdmaprnlem7N  32670  hdmaprnlem8N  32671  hdmaprnlem3eN  32673  hgmapvvlem3  32740
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 177  df-an 360
  Copyright terms: Public domain W3C validator