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

Theorem syl22anc 1229
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 1226 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  4857  soltmin  5406  f1oprg  5856  fveqf1o  6193  weniso  6238  fr3nr  6599  smogt  7038  smorndom  7039  oacomf1o  7214  difsnen  7599  undom  7605  enfixsn  7626  domss2  7676  ssenen  7691  marypha1lem  7893  fisupcl  7927  ordtypelem3  7945  ordtypelem8  7950  oieu  7964  oismo  7965  wofib  7970  wemaplem2  7972  wemapso  7976  wemapso2OLD  7977  wemapso2lem  7978  unxpwdom2  8014  infdifsn  8073  oemapvali  8103  cantnflem1c  8106  cantnflem1d  8107  cantnflem1  8108  cantnf  8112  cantnfOLD  8134  cnfcom3  8148  cnfcom3OLD  8156  r1ordg  8196  dif1card  8388  infxpenlem  8391  dfac8clem  8413  infxp  8595  infmap2  8598  cflim2  8643  coftr  8653  fin2i2  8698  enfin2i  8701  fin23lem26  8705  fin23lem27  8708  fin23lem40  8731  isf32lem2  8734  isf32lem3  8735  isf32lem4  8736  isf32lem7  8739  isf32lem9  8741  fin1a2lem13  8792  fin12  8793  alephexp1  8954  gchdomtri  9007  fpwwe2lem12  9019  fpwwe2lem13  9020  gchpwdom  9048  gchhar  9057  adderpqlem  9332  mulerpqlem  9333  addassnq  9336  mulassnq  9337  distrnq  9339  mulidnq  9341  recmulnq  9342  ltexnq  9353  distrlem1pr  9403  distrlem4pr  9404  prlem936  9425  reclem3pr  9427  mulcmpblnr  9448  mulgt0d  9736  mul4d  9791  add4d  9803  add42d  9804  subcan  9874  addsub4d  9977  subadd4d  9978  sub4d  9979  2addsubd  9980  addsubeq4d  9981  muladdd  10014  mulsubd  10015  addgegt0d  10126  addge0d  10128  mulge0d  10129  le2addd  10170  le2subd  10171  ltleaddd  10172  leltaddd  10173  lt2subd  10175  divdivdiv  10245  divcan5  10246  divne0d  10336  recdivd  10337  recdiv2d  10338  divcan6d  10339  ddcand  10340  rec11d  10341  divmuldivd  10361  divmul13d  10362  divmul24d  10363  divadddivd  10364  divsubdivd  10365  divmuleqd  10366  divdivdivd  10367  subrecd  10375  mulge0b  10412  recreclt  10444  divgt0d  10481  mulgt1d  10482  lemulge11d  10483  lemulge12d  10484  ltmul12ad  10487  lemul12ad  10488  lemul12bd  10489  supmul1  10508  nndivtr  10577  qreccl  11202  ledivdivd  11281  lediv12ad  11311  lt2mul2divd  11314  xlt2add  11452  supxrun  11507  supxrre  11519  infmxrre  11527  iccss2  11595  iccssico2  11598  lincmb01cmp  11663  iccf1o  11664  fzrev2i  11744  modaddmodup  12018  modaddmodlo  12019  modsubdir  12023  fzennn  12046  sermono  12107  mulexpz  12174  expaddz  12178  ltexp2a  12185  leexp2a  12189  sqdiv  12201  expmulnbnd  12266  digit1  12268  expsubd  12289  lt2sqd  12312  le2sqd  12313  sq11d  12314  bcm1k  12361  bcp1n  12362  bcp1nk  12363  hashf1lem1  12470  cshw1  12753  2swrd2eqwrdeq  12854  absrele  13104  sqreulem  13155  sqrtmuld  13219  sqrtsq2d  13220  sqrtled  13221  sqrtltd  13222  sqr11d  13223  abs3lemd  13255  rlimuni  13336  climuni  13338  lo1resb  13350  o1resb  13352  2clim  13358  addcn2  13379  mulcn2  13381  o1of2  13398  o1rlimmul  13404  lo1add  13412  lo1mul  13413  isercolllem1  13450  caucvgrlem  13458  iseraltlem2  13468  iseraltlem3  13469  iseralt  13470  mptfzshft  13556  fsumrev  13557  fsum0diag2  13561  binomlem  13604  climcndslem1  13624  climcndslem2  13625  harmonic  13633  mertenslem1  13656  efcllem  13675  moddvds  13854  dvds1  13893  dvdsext  13896  oexpneg  13908  bitsinv1  13951  sadaddlem  13975  sadasslem  13979  sadeq  13981  mulgcd  14043  dvdssqlem  14056  rpmulgcd2  14105  isprm6  14109  isprm5  14112  crt  14167  eulerthlem2  14171  prmdiveq  14175  pythagtriplem11  14208  pythagtriplem13  14210  iserodd  14218  pcgcd1  14259  pcprmpw2  14264  pcaddlem  14266  fldivp1  14275  4sqlem12  14333  4sqlem14  14335  4sqlem15  14336  4sqlem16  14337  vdwapun  14351  mreexexlem4d  14902  acsfn1  14916  acsfn2  14918  sscpwex  15045  rescabs  15063  catciso  15292  yonedainv  15408  subm0  15806  pmtrff1o  16294  pmtrfcnv  16295  pmtrfb  16296  psgnunilem1  16324  odmodnn0  16370  odeq  16380  dfod2  16392  sylow1lem1  16424  lsmsubg  16480  lsmmod  16499  lsmdisj2  16506  ghmplusg  16655  odadd  16659  gexexlem  16661  lt6abl  16700  cyggex2  16702  dprdfinv  16861  dmdprdsplitlem  16886  dpjidcl  16909  ablfacrp  16919  ablfacrp2  16920  ablfac1c  16924  ablfac1eu  16926  lcomfsupOLD  17349  lcomfsupp  17350  lssvancl1  17391  lssvnegcl  17402  lspprvacl  17445  lspsneli  17447  lspsn  17448  lmhmplusg  17490  lmhmima  17493  lmhmpreima  17494  reslmhm  17498  lbsind2  17527  lsmcl  17529  lsmelval2  17531  lsppreli  17536  lspprabs  17541  pj1lmhm  17546  lssvs0or  17556  lspabs3  17567  lspfixed  17574  lspexch  17575  lsmcv  17587  lspsolv  17589  lidlmcl  17664  drngnidl  17676  2idlcpbl  17681  mplbas2  17933  mplbas2OLD  17934  evlslem3  17982  evlslem1  17983  coe1addfv  18105  lply1binom  18147  evl1addd  18176  evl1subd  18177  evl1muld  18178  gzrngunit  18279  zringlpirlem3  18306  zlpirlem3  18311  prmirredlem  18318  prmirredlemOLD  18321  znf1o  18385  znunithash  18398  evpmodpmf1o  18427  frlmsubgval  18593  frlmvscaval  18595  frlmphllem  18606  frlmphl  18607  frlmssuvc1  18620  frlmssuvc1OLD  18622  frlmsslsp  18624  frlmsslspOLD  18625  frlmup1  18627  frlmup2  18628  lindfind2  18648  lindfrn  18651  f1lindf  18652  islindf4  18668  mamudi  18700  mamudir  18701  1marepvmarrepid  18872  mdetrlin  18899  smadiadetglem1  18968  smadiadetg  18970  cramerimplem1  18980  mat2pmatscmxcl  19036  m2pmfzgsumcl  19044  pmatcollpw  19077  pmatcollpwfi  19078  pmatcollpw3fi1lem1  19082  cpmidpmatlem2  19167  cpmadugsumlemF  19172  chcoeffeqlem  19181  ntrin  19356  topssnei  19419  restbas  19453  restntr  19477  cnntri  19566  fiuncmp  19698  nllyrest  19781  nllyidm  19784  hausllycmp  19789  cldllycmp  19790  hauspwdom  19796  txcld  19867  txcn  19890  txlly  19900  txnlly  19901  txhaus  19911  txlm  19912  txkgen  19916  xkococnlem  19923  cnmpt2res  19941  xkoinjcn  19951  basqtop  19975  qtopeu  19980  qtophmeo  20081  trfbas2  20107  neifil  20144  hausflim  20245  alexsubALTlem2  20311  cnextfval  20325  cnextfvval  20328  cnextf  20329  clssubg  20370  utop2nei  20516  utop3cls  20517  utopreg  20518  psmetlecl  20582  xmetlecl  20612  prdsxmetlem  20634  bldisj  20664  imasf1obl  20754  prdsbl  20757  stdbdmet  20782  stdbdmopn  20784  met2ndci  20788  metcnp  20807  metusttoOLD  20823  metustto  20824  metustexhalfOLD  20829  metustexhalf  20830  cfilucfilOLD  20835  cfilucfil  20836  metucnOLD  20854  metucn  20855  lssnlm  20972  nmotri  21009  nmoid  21012  tgioo  21064  blcvx  21066  xrsmopn  21080  reperflem  21086  reconnlem2  21095  opnreen  21099  metdsge  21116  metdsre  21120  metdscnlem  21122  metnrmlem1a  21125  metnrmlem1  21126  metnrmlem3  21128  cncfmet  21175  cnmpt2pc  21191  icopnfcnv  21205  icopnfhmeo  21206  cnllycmp  21219  evth  21222  lebnumii  21229  nmoleub2lem3  21361  iscfil2  21468  cfil3i  21471  iscfil3  21475  cfilfcls  21476  iscau3  21480  iscmet3lem2  21494  caubl  21509  lmcau  21514  rrxcph  21587  minveclem2  21604  pjthlem1  21615  pjthlem2  21616  ivthicc  21633  ovollecl  21657  ovolunlem1a  21670  ovolunnul  21674  ovoliunlem1  21676  ismbl2  21701  nulmbl2  21710  unmbl  21711  volun  21718  voliunlem2  21724  ioombl1lem2  21732  uniioombllem2a  21754  uniioombllem3  21757  uniioombllem4  21758  dyaddisjlem  21767  dyadmaxlem  21769  opnmbllem  21773  volsup2  21777  volcn  21778  ismbfd  21810  mbfi1fseqlem1  21885  mbfi1fseqlem5  21889  itg2lecl  21908  itg2monolem2  21921  itg2gt0  21930  itgspliticc  22006  ellimc3  22046  limcres  22053  dvfval  22064  dvres3  22080  dvres3a  22081  dvnff  22089  dvnadd  22095  dvn2bss  22096  dvnres  22097  dvcmul  22110  dvcmulf  22111  dvmptres3  22122  dvmptres2  22128  dvmptntr  22137  dvexp3  22142  dvferm1lem  22148  dvlip  22157  dvlipcn  22158  dvlip2  22159  c1liplem1  22160  dvgt0lem1  22166  dvgt0lem2  22167  dvne0  22175  lhop1lem  22177  lhop2  22179  lhop  22180  dvcnvrelem1  22181  dvcnvrelem2  22182  dvcvx  22184  dvfsumle  22185  dvfsumabs  22187  dvfsumlem2  22191  ftc1lem6  22205  ftc1  22206  ftc2ditglem  22209  itgsubstlem  22212  tdeglem4  22221  mdegaddle  22237  mdegmullem  22241  ply1rem  22327  fta1glem2  22330  fta1blem  22332  ig1peu  22335  ig1pdvds  22340  dgrmulc  22430  dgrcolem1  22432  plydivlem4  22454  plydiveu  22456  fta1lem  22465  vieta1lem1  22468  vieta1lem2  22469  plyexmo  22471  taylfvallem1  22514  taylfval  22516  tayl0  22519  taylplem1  22520  taylply2  22525  taylply  22526  dvtaylp  22527  dvntaylp  22528  dvntaylp0  22529  taylthlem1  22530  taylthlem2  22531  ulmcaulem  22551  ulmcau  22552  ulmcn  22556  ulmdvlem1  22557  radcnvlem1  22570  radcnvle  22577  psercn  22583  pserdvlem2  22585  pserdv  22586  abelth  22598  cosordlem  22679  tanregt0  22687  dvlog2lem  22789  efopn  22795  logtayllem  22796  logccv  22800  cxplt3  22837  cxpmul2zd  22853  cxpltd  22856  cxpled  22857  cxplt3d  22869  cxple3d  22870  dvsqrt  22874  cxpcn3  22878  cxpaddle  22882  cxpeq  22887  angcan  22890  angvald  22892  ang180lem2  22898  ang180  22902  isosctrlem3  22910  dquartlem1  22938  atantayl2  23025  leibpilem1  23027  leibpi  23029  log2tlbnd  23032  birthdaylem3  23039  xrlimcnp  23054  efrlim  23055  o1cxp  23060  jensenlem2  23073  jensen  23074  fsumharmonic  23097  wilthlem1  23098  basellem3  23112  basellem6  23115  basellem8  23117  ppisval  23133  chtwordi  23186  ppiwordi  23192  mumullem2  23210  dvdsmulf1o  23226  fsumvma  23244  fsumvma2  23245  chpchtsum  23250  chpub  23251  logfacubnd  23252  dchrmulcl  23280  dchrinv  23292  dchrptlem1  23295  dchrptlem2  23296  sumdchr2  23301  dchr2sum  23304  bposlem7  23321  lgslem1  23327  lgslem3  23329  lgsdirprm  23360  lgsqrlem2  23373  lgseisenlem1  23380  lgseisenlem2  23381  lgseisenlem4  23383  lgseisen  23384  lgsquadlem1  23385  lgsquad2lem1  23389  lgsquad3  23392  m1lgs  23393  2sqlem7  23401  chebbnd1lem2  23411  chebbnd1lem3  23412  rplogsumlem1  23425  rpvmasumlem  23428  dchrvmasumlem1  23436  dchrvmasum2lem  23437  dchrvmasumlema  23441  dchrisum0flblem2  23450  dchrisum0fno1  23452  dchrisum0re  23454  logdivsum  23474  pntrsumbnd2  23508  pntpbnd1a  23526  pntpbnd1  23527  pntibndlem2  23532  pntlemr  23543  pntlemj  23544  pntlemf  23546  pnt2  23554  padicabv  23571  ostth2lem2  23575  f1otrg  23878  brbtwn2  23912  colinearalglem2  23914  axcgrtr  23922  axcgrid  23923  axsegconlem7  23930  axsegcon  23934  ax5seglem3  23938  ax5seglem6  23941  ax5seg  23945  axpaschlem  23947  axlowdimlem17  23965  axcontlem2  23972  axcontlem4  23974  axcontlem7  23977  axcontlem8  23978  ecgrtg  23990  usgraidx2v  24097  iseupa  24669  eupap1  24680  eupath2lem3  24683  numclwwlkovf2ex  24791  nmobndi  25394  ubthlem2  25491  ubthlem3  25492  minvecolem2  25495  shuni  25922  pjhthlem1  26013  chscllem2  26260  pjcompi  26294  mayete3i  26350  mayete3iOLD  26351  unoplin  26543  hmoplin  26565  nmophmi  26654  mdslmd4i  26956  preqsnd  27120  isoun  27220  xrofsup  27278  eliccelico  27284  elicoelioo  27285  difioo  27289  rexdiv  27318  xrge0addgt0  27371  omndadd2d  27388  omndadd2rd  27389  unitdivcld  27547  xrge0mulc1cn  27587  qqhnm  27635  esumcst  27739  esumfsup  27744  esumpmono  27753  esumcvg  27760  difelsiga  27801  1stmbfm  27899  2ndmbfm  27900  dya2icoseg  27916  sibfinima  27949  probmeasb  28037  orvcgteel  28074  orvclteel  28079  ballotlemsima  28122  ballotlemfrceq  28135  sgnmul  28149  ccatmulgnn0dir  28164  ofccat  28165  lgamucov  28248  lgamcvg2  28265  subfacp1lem2a  28292  subfaclim  28300  erdsze2lem2  28316  cvmliftlem2  28399  cvmliftlem10  28407  cvmliftlem13  28409  cvmliftiota  28414  cvmlift2lem9  28424  cvmlift2lem11  28426  cvmlift2lem12  28427  cvmliftphtlem  28430  cvmlift3lem6  28437  cvmlift3lem7  28438  cvmlift3lem9  28440  snmlff  28442  fprodser  28686  fprodshft  28711  fprodrev  28712  rprisefaccl  28750  trpredelss  28920  trpredpo  28923  wzel  28985  wsuclem  28986  nodenselem5  29050  nobndlem6  29062  brsegle  29363  fin2so  29645  opnmbllem0  29655  mblfinlem3  29658  mblfinlem4  29659  itg2addnclem  29671  itg2addnc  29674  itg2gt0cn  29675  ftc1cnnclem  29693  ftc1cnnc  29694  areacirclem5  29716  opnregcld  29753  indexdom  29856  sstotbnd2  29901  isbnd3  29911  isbnd3b  29912  cntotbnd  29923  ismtyima  29930  heibor1lem  29936  heiborlem8  29945  rrncmslem  29959  reheibor  29966  mzpsubst  30313  eldioph2lem1  30325  eldioph2lem2  30326  eldioph2b  30328  diophin  30338  irrapxlem2  30391  irrapxlem4  30393  irrapxlem5  30394  pellexlem1  30397  pellexlem2  30398  pellexlem6  30402  elpell1qr2  30440  pell1qrgaplem  30441  pell1qrgap  30442  pellqrex  30447  pellfundex  30454  pellfund14  30466  rmspecsqrtnq  30474  rmxyadd  30489  expmordi  30515  rmxypos  30517  jm2.24  30533  congsub  30540  mzpcong  30542  congrep  30543  acongtr  30548  acongrep  30550  jm2.19lem1  30563  jm2.22  30569  jm2.23  30570  jm2.26lem3  30575  jm2.26  30576  jm2.27a  30579  fnwe2lem2  30629  aomclem6  30637  hbtlem2  30705  hbtlem4  30707  hbtlem5  30709  dgraa0p  30731  rngunsnply  30755  acsfn1p  30781  proot1hash  30793  itgpowd  30815  expgrowth  30868  elicore  31129  eliocre  31139  ioossioobi  31149  limcresiooub  31212  cncfuni  31253  dvcnre  31272  dvresntr  31274  dvmptresicc  31277  dvresioo  31279  dvbdfbdioolem1  31286  itgsinexplem1  31299  itgcoscmulx  31315  stoweidlem11  31339  stoweidlem26  31354  stoweidlem34  31362  stoweidlem36  31364  stoweidlem38  31366  stirlinglem5  31406  fourierdlem20  31455  fourierdlem58  31493  fourierdlem72  31507  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem80  31515  fourierdlem87  31522  fourierdlem94  31529  fourierdlem103  31538  fourierdlem104  31539  fourierdlem107  31542  fourierdlem113  31548  sqwvfoura  31557  sqwvfourb  31558  fourierswlem  31559  fouriersw  31560  uhgeq12d  31870  usgedgvadf1  31910  usgedgvadf1ALT  31913  lkrlsp  33917  lshpkrlem5  33929  ldualssvscl  33973  ldualssvsubcl  33974  llnmlplnN  34353  llncvrlpln  34372  pmapjat1  34667  pclfinN  34714  lautlt  34905  lauteq  34909  lautco  34911  ltrn11  34940  ltrnle  34943  ltrneq2  34962  cdlemednuN  35114  cdleme20k  35133  cdleme20l2  35135  cdleme20l  35136  cdleme20m  35137  cdleme21c  35141  cdleme22e  35158  cdleme22eALTN  35159  cdlemefrs32fva  35214  cdlemg4g  35430  cdlemg18b  35493  cdlemg18c  35494  cdlemj3  35637  dia2dimlem5  35883  dvhopN  35931  cdlemm10N  35933  dihjatcclem4  36236  dochexmidlem2  36276  lclkrlem2o  36336  lcfrlem5  36361  lcfrlem6  36362  lcdlssvscl  36421  mapdpglem6  36493  mapdpglem9  36495  mapdpglem12  36498  mapdpglem14  36500  mapdindp0  36534  hdmaprnlem7N  36673  hdmaprnlem8N  36674  hdmaprnlem3eN  36676  hgmapvvlem3  36743
  Copyright terms: Public domain W3C validator