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

Theorem syl22anc 1219
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 532 . 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 1216 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  fr2nr  4693  soltmin  5232  f1oprg  5676  fveqf1o  5995  weniso  6040  fr3nr  6386  smogt  6820  smorndom  6821  oacomf1o  6996  th3qlem1  7198  difsnen  7385  undom  7391  enfixsn  7412  domss2  7462  ssenen  7477  marypha1lem  7675  fisupcl  7709  ordtypelem3  7726  ordtypelem8  7731  oieu  7745  oismo  7746  wofib  7751  wemaplem2  7753  wemapso  7757  wemapso2OLD  7758  wemapso2lem  7759  unxpwdom2  7795  infdifsn  7854  oemapvali  7884  cantnflem1c  7887  cantnflem1d  7888  cantnflem1  7889  cantnf  7893  cantnfOLD  7915  cnfcom3  7929  cnfcom3OLD  7937  r1ordg  7977  dif1card  8169  infxpenlem  8172  dfac8clem  8194  infxp  8376  infmap2  8379  cflim2  8424  coftr  8434  fin2i2  8479  enfin2i  8482  fin23lem26  8486  fin23lem27  8489  fin23lem40  8512  isf32lem2  8515  isf32lem3  8516  isf32lem4  8517  isf32lem7  8520  isf32lem9  8522  fin1a2lem13  8573  fin12  8574  alephexp1  8735  gchdomtri  8788  fpwwe2lem12  8800  fpwwe2lem13  8801  gchpwdom  8829  gchhar  8838  adderpqlem  9115  mulerpqlem  9116  addassnq  9119  mulassnq  9120  distrnq  9122  mulidnq  9124  recmulnq  9125  ltexnq  9136  distrlem1pr  9186  distrlem4pr  9187  prlem936  9208  reclem3pr  9210  mulgt0d  9518  mul4d  9573  add4d  9585  add42d  9586  subcan  9656  addsub4d  9758  subadd4d  9759  sub4d  9760  2addsubd  9761  addsubeq4d  9762  muladdd  9794  mulsubd  9795  addgegt0d  9905  addge0d  9907  mulge0d  9908  le2addd  9949  le2subd  9950  ltleaddd  9951  leltaddd  9952  lt2subd  9954  divdivdiv  10024  divcan5  10025  divne0d  10115  recdivd  10116  recdiv2d  10117  divcan6d  10118  ddcand  10119  rec11d  10120  divmuldivd  10140  divmul13d  10141  divmul24d  10142  divadddivd  10143  divsubdivd  10144  divmuleqd  10145  divdivdivd  10146  subrecd  10154  mulge0b  10191  recreclt  10223  divgt0d  10260  mulgt1d  10261  lemulge11d  10262  lemulge12d  10263  ltmul12ad  10266  lemul12ad  10267  lemul12bd  10268  supmul1  10287  nndivtr  10355  qreccl  10965  ledivdivd  11044  lediv12ad  11074  lt2mul2divd  11077  xlt2add  11215  supxrun  11270  supxrre  11282  infmxrre  11290  iccss2  11358  iccssico2  11361  lincmb01cmp  11420  iccf1o  11421  fzrev2i  11513  modaddmodup  11754  modaddmodlo  11755  modsubdir  11759  fzennn  11782  sermono  11830  mulexpz  11896  expaddz  11900  ltexp2a  11907  leexp2a  11911  sqdiv  11923  expmulnbnd  11988  digit1  11990  expsubd  12011  lt2sqd  12034  le2sqd  12035  sq11d  12036  bcm1k  12083  bcp1n  12084  bcp1nk  12085  hashf1lem1  12200  cshw1  12448  2swrd2eqwrdeq  12545  absrele  12789  sqreulem  12839  sqrmuld  12903  sqrsq2d  12904  sqrled  12905  sqrltd  12906  sqr11d  12907  abs3lemd  12939  rlimuni  13020  climuni  13022  lo1resb  13034  o1resb  13036  2clim  13042  addcn2  13063  mulcn2  13065  o1of2  13082  o1rlimmul  13088  lo1add  13096  lo1mul  13097  isercolllem1  13134  caucvgrlem  13142  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  mptfzshft  13237  fsumrev  13238  fsum0diag2  13242  binomlem  13284  climcndslem1  13304  climcndslem2  13305  harmonic  13313  mertenslem1  13336  efcllem  13355  moddvds  13534  dvds1  13573  dvdsext  13576  oexpneg  13587  bitsinv1  13630  sadaddlem  13654  sadasslem  13658  sadeq  13660  mulgcd  13722  dvdssqlem  13735  rpmulgcd2  13783  isprm6  13787  isprm5  13790  crt  13845  eulerthlem2  13849  prmdiveq  13853  pythagtriplem11  13884  pythagtriplem13  13886  iserodd  13894  pcgcd1  13935  pcprmpw2  13940  pcaddlem  13942  fldivp1  13951  4sqlem12  14009  4sqlem14  14011  4sqlem15  14012  4sqlem16  14013  vdwapun  14027  mreexexlem4d  14577  acsfn1  14591  acsfn2  14593  sscpwex  14720  rescabs  14738  catciso  14967  yonedainv  15083  subm0  15475  pmtrff1o  15960  pmtrfcnv  15961  pmtrfb  15962  psgnunilem1  15990  odmodnn0  16034  odeq  16044  dfod2  16056  sylow1lem1  16088  lsmsubg  16144  lsmmod  16163  lsmdisj2  16170  ghmplusg  16319  odadd  16323  gexexlem  16325  lt6abl  16362  cyggex2  16364  dprdfinv  16499  dmdprdsplitlem  16524  dpjidcl  16547  ablfacrp  16557  ablfacrp2  16558  ablfac1c  16562  ablfac1eu  16564  lcomfsupOLD  16964  lcomfsupp  16965  lssvancl1  17006  lssvnegcl  17017  lspprvacl  17060  lspsneli  17062  lspsn  17063  lmhmplusg  17105  lmhmima  17108  lmhmpreima  17109  reslmhm  17113  lbsind2  17142  lsmcl  17144  lsmelval2  17146  lsppreli  17151  lspprabs  17156  pj1lmhm  17161  lssvs0or  17171  lspabs3  17182  lspfixed  17189  lspexch  17190  lsmcv  17202  lspsolv  17204  lidlmcl  17279  drngnidl  17291  2idlcpbl  17296  mplbas2  17531  mplbas2OLD  17532  evlslem3  17580  evlslem1  17581  coe1addfv  17699  evl1addd  17755  evl1subd  17756  evl1muld  17757  gzrngunit  17858  zringlpirlem3  17885  zlpirlem3  17890  prmirredlem  17897  prmirredlemOLD  17900  znf1o  17964  znunithash  17977  evpmodpmf1o  18006  frlmsubgval  18172  frlmvscaval  18174  frlmphllem  18185  frlmphl  18186  frlmssuvc1  18199  frlmssuvc1OLD  18201  frlmsslsp  18203  frlmsslspOLD  18204  frlmup1  18206  frlmup2  18207  lindfind2  18227  lindfrn  18230  f1lindf  18231  islindf4  18247  mamudi  18287  mamudir  18288  1marepvmarrepid  18366  mdetrlin  18389  smadiadetglem1  18457  smadiadetg  18459  cramerimplem1  18469  ntrin  18645  topssnei  18708  restbas  18742  restntr  18766  cnntri  18855  fiuncmp  18987  nllyrest  19070  nllyidm  19073  hausllycmp  19078  cldllycmp  19079  hauspwdom  19085  txcld  19156  txcn  19179  txlly  19189  txnlly  19190  txhaus  19200  txlm  19201  txkgen  19205  xkococnlem  19212  cnmpt2res  19230  xkoinjcn  19240  basqtop  19264  qtopeu  19269  qtophmeo  19370  trfbas2  19396  neifil  19433  hausflim  19534  alexsubALTlem2  19600  cnextfval  19614  cnextfvval  19617  cnextf  19618  clssubg  19659  utop2nei  19805  utop3cls  19806  utopreg  19807  psmetlecl  19871  xmetlecl  19901  prdsxmetlem  19923  bldisj  19953  imasf1obl  20043  prdsbl  20046  stdbdmet  20071  stdbdmopn  20073  met2ndci  20077  metcnp  20096  metusttoOLD  20112  metustto  20113  metustexhalfOLD  20118  metustexhalf  20119  cfilucfilOLD  20124  cfilucfil  20125  metucnOLD  20143  metucn  20144  lssnlm  20261  nmotri  20298  nmoid  20301  tgioo  20353  blcvx  20355  xrsmopn  20369  reperflem  20375  reconnlem2  20384  opnreen  20388  metdsge  20405  metdsre  20409  metdscnlem  20411  metnrmlem1a  20414  metnrmlem1  20415  metnrmlem3  20417  cncfmet  20464  cnmpt2pc  20480  icopnfcnv  20494  icopnfhmeo  20495  cnllycmp  20508  evth  20511  lebnumii  20518  nmoleub2lem3  20650  iscfil2  20757  cfil3i  20760  iscfil3  20764  cfilfcls  20765  iscau3  20769  iscmet3lem2  20783  caubl  20798  lmcau  20803  rrxcph  20876  minveclem2  20893  pjthlem1  20904  pjthlem2  20905  ivthicc  20922  ovollecl  20946  ovolunlem1a  20959  ovolunnul  20963  ovoliunlem1  20965  ismbl2  20990  nulmbl2  20998  unmbl  20999  volun  21006  voliunlem2  21012  ioombl1lem2  21020  uniioombllem2a  21042  uniioombllem3  21045  uniioombllem4  21046  dyaddisjlem  21055  dyadmaxlem  21057  opnmbllem  21061  volsup2  21065  volcn  21066  ismbfd  21098  mbfi1fseqlem1  21173  mbfi1fseqlem5  21177  itg2lecl  21196  itg2monolem2  21209  itg2gt0  21218  itgspliticc  21294  ellimc3  21334  limcres  21341  dvfval  21352  dvres3  21368  dvres3a  21369  dvnff  21377  dvnadd  21383  dvn2bss  21384  dvnres  21385  dvcmul  21398  dvcmulf  21399  dvmptres3  21410  dvmptres2  21416  dvmptntr  21425  dvexp3  21430  dvferm1lem  21436  dvlip  21445  dvlipcn  21446  dvlip2  21447  c1liplem1  21448  dvgt0lem1  21454  dvgt0lem2  21455  dvne0  21463  lhop1lem  21465  lhop2  21467  lhop  21468  dvcnvrelem1  21469  dvcnvrelem2  21470  dvcvx  21472  dvfsumle  21473  dvfsumabs  21475  dvfsumlem2  21479  ftc1lem6  21493  ftc1  21494  ftc2ditglem  21497  itgsubstlem  21500  tdeglem4  21509  mdegaddle  21525  mdegmullem  21529  ply1rem  21615  fta1glem2  21618  fta1blem  21620  ig1peu  21623  ig1pdvds  21628  dgrmulc  21718  dgrcolem1  21720  plydivlem4  21742  plydiveu  21744  fta1lem  21753  vieta1lem1  21756  vieta1lem2  21757  plyexmo  21759  taylfvallem1  21802  taylfval  21804  tayl0  21807  taylplem1  21808  taylply2  21813  taylply  21814  dvtaylp  21815  dvntaylp  21816  dvntaylp0  21817  taylthlem1  21818  taylthlem2  21819  ulmcaulem  21839  ulmcau  21840  ulmcn  21844  ulmdvlem1  21845  radcnvlem1  21858  radcnvle  21865  psercn  21871  pserdvlem2  21873  pserdv  21874  abelth  21886  cosordlem  21967  tanregt0  21975  dvlog2lem  22077  efopn  22083  logtayllem  22084  logccv  22088  cxplt3  22125  cxpmul2zd  22141  cxpltd  22144  cxpled  22145  cxplt3d  22157  cxple3d  22158  dvsqr  22162  cxpcn3  22166  cxpaddle  22170  cxpeq  22175  angcan  22178  angvald  22180  ang180lem2  22186  ang180  22190  isosctrlem3  22198  dquartlem1  22226  atantayl2  22313  leibpilem1  22315  leibpi  22317  log2tlbnd  22320  birthdaylem3  22327  xrlimcnp  22342  efrlim  22343  o1cxp  22348  jensenlem2  22361  jensen  22362  fsumharmonic  22385  wilthlem1  22386  basellem3  22400  basellem6  22403  basellem8  22405  ppisval  22421  chtwordi  22474  ppiwordi  22480  mumullem2  22498  dvdsmulf1o  22514  fsumvma  22532  fsumvma2  22533  chpchtsum  22538  chpub  22539  logfacubnd  22540  dchrmulcl  22568  dchrinv  22580  dchrptlem1  22583  dchrptlem2  22584  sumdchr2  22589  dchr2sum  22592  bposlem7  22609  lgslem1  22615  lgslem3  22617  lgsdirprm  22648  lgsqrlem2  22661  lgseisenlem1  22668  lgseisenlem2  22669  lgseisenlem4  22671  lgseisen  22672  lgsquadlem1  22673  lgsquad2lem1  22677  lgsquad3  22680  m1lgs  22681  2sqlem7  22689  chebbnd1lem2  22699  chebbnd1lem3  22700  rplogsumlem1  22713  rpvmasumlem  22716  dchrvmasumlem1  22724  dchrvmasum2lem  22725  dchrvmasumlema  22729  dchrisum0flblem2  22738  dchrisum0fno1  22740  dchrisum0re  22742  logdivsum  22762  pntrsumbnd2  22796  pntpbnd1a  22814  pntpbnd1  22815  pntibndlem2  22820  pntlemr  22831  pntlemj  22832  pntlemf  22834  pnt2  22842  padicabv  22859  ostth2lem2  22863  f1otrg  23085  brbtwn2  23119  colinearalglem2  23121  axcgrtr  23129  axcgrid  23130  axsegconlem7  23137  axsegcon  23141  ax5seglem3  23145  ax5seglem6  23148  ax5seg  23152  axpaschlem  23154  axlowdimlem17  23172  axcontlem2  23179  axcontlem4  23181  axcontlem7  23184  axcontlem8  23185  ecgrtg  23197  usgraidx2v  23279  iseupa  23554  eupap1  23565  eupath2lem3  23568  nmobndi  24143  ubthlem2  24240  ubthlem3  24241  minvecolem2  24244  shuni  24671  pjhthlem1  24762  chscllem2  25009  pjcompi  25043  mayete3i  25099  mayete3iOLD  25100  unoplin  25292  hmoplin  25314  nmophmi  25403  mdslmd4i  25705  preqsnd  25869  isoun  25965  xrofsup  26023  eliccelico  26035  elicoelioo  26036  difioo  26040  rexdiv  26069  xrge0addgt0  26122  omndadd2d  26139  omndadd2rd  26140  unitdivcld  26300  xrge0mulc1cn  26340  qqhnm  26388  esumcst  26483  esumfsup  26488  esumpmono  26497  esumcvg  26504  difelsiga  26545  1stmbfm  26644  2ndmbfm  26645  dya2icoseg  26661  sibfinima  26694  probmeasb  26782  orvcgteel  26819  orvclteel  26824  ballotlemsima  26867  ballotlemfrceq  26880  sgnmul  26894  ccatmulgnn0dir  26909  ofccat  26910  lgamucov  26993  lgamcvg2  27010  subfacp1lem2a  27037  subfaclim  27045  erdsze2lem2  27061  cvmliftlem2  27144  cvmliftlem10  27152  cvmliftlem13  27154  cvmliftiota  27159  cvmlift2lem9  27169  cvmlift2lem11  27171  cvmlift2lem12  27172  cvmliftphtlem  27175  cvmlift3lem6  27182  cvmlift3lem7  27183  cvmlift3lem9  27185  snmlff  27187  fprodser  27431  fprodshft  27456  fprodrev  27457  rprisefaccl  27495  trpredelss  27665  trpredpo  27668  wzel  27730  wsuclem  27731  nodenselem5  27795  nobndlem6  27807  brsegle  28108  fin2so  28387  opnmbllem0  28398  mblfinlem3  28401  mblfinlem4  28402  itg2addnclem  28414  itg2addnc  28417  itg2gt0cn  28418  ftc1cnnclem  28436  ftc1cnnc  28437  areacirclem5  28459  opnregcld  28496  indexdom  28599  sstotbnd2  28644  isbnd3  28654  isbnd3b  28655  cntotbnd  28666  ismtyima  28673  heibor1lem  28679  heiborlem8  28688  rrncmslem  28702  reheibor  28709  mzpsubst  29056  eldioph2lem1  29069  eldioph2lem2  29070  eldioph2b  29072  diophin  29082  irrapxlem2  29135  irrapxlem4  29137  irrapxlem5  29138  pellexlem1  29141  pellexlem2  29142  pellexlem6  29146  elpell1qr2  29184  pell1qrgaplem  29185  pell1qrgap  29186  pellqrex  29191  pellfundex  29198  pellfund14  29210  rmspecsqrnq  29218  rmxyadd  29233  expmordi  29259  rmxypos  29261  jm2.24  29277  congsub  29284  mzpcong  29286  congrep  29287  acongtr  29292  acongrep  29294  jm2.19lem1  29309  jm2.22  29315  jm2.23  29316  jm2.26lem3  29321  jm2.26  29322  jm2.27a  29325  fnwe2lem2  29375  aomclem6  29383  hbtlem2  29451  hbtlem4  29453  hbtlem5  29455  dgraa0p  29477  rngunsnply  29501  acsfn1p  29527  proot1hash  29539  itgpowd  29561  expgrowth  29580  itgsinexplem1  29765  stoweidlem11  29777  stoweidlem26  29792  stoweidlem34  29800  stoweidlem36  29802  stoweidlem38  29804  stirlinglem5  29844  numclwwlkovf2ex  30650  lply1binom  30811  lkrlsp  32640  lshpkrlem5  32652  ldualssvscl  32696  ldualssvsubcl  32697  llnmlplnN  33076  llncvrlpln  33095  pmapjat1  33390  pclfinN  33437  lautlt  33628  lauteq  33632  lautco  33634  ltrn11  33663  ltrnle  33666  ltrneq2  33685  cdlemednuN  33837  cdleme20k  33856  cdleme20l2  33858  cdleme20l  33859  cdleme20m  33860  cdleme21c  33864  cdleme22e  33881  cdleme22eALTN  33882  cdlemefrs32fva  33937  cdlemg4g  34153  cdlemg18b  34216  cdlemg18c  34217  cdlemj3  34360  dia2dimlem5  34606  dvhopN  34654  cdlemm10N  34656  dihjatcclem4  34959  dochexmidlem2  34999  lclkrlem2o  35059  lcfrlem5  35084  lcfrlem6  35085  lcdlssvscl  35144  mapdpglem6  35216  mapdpglem9  35218  mapdpglem12  35221  mapdpglem14  35223  mapdindp0  35257  hdmaprnlem7N  35396  hdmaprnlem8N  35397  hdmaprnlem3eN  35399  hgmapvvlem3  35466
  Copyright terms: Public domain W3C validator