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

Theorem syl13anc 1184
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 )
syl13anc.5  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
Assertion
Ref Expression
syl13anc  |-  ( ph  ->  et )

Proof of Theorem syl13anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
52, 3, 43jca 1132 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 642 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl23anc  1189  syl33anc  1197  pm2.61da3ne  2528  disjxiun  4022  wereu2  4392  ordelord  4416  caovassd  6021  caovcand  6024  caovordid  6028  caovordd  6030  caovdid  6037  caovdird  6040  swoer  6690  swoord1  6691  swoord2  6692  frfi  7104  indexfi  7165  ssfii  7174  elfiun  7185  suplub2  7214  wemaplem2  7264  htalem  7568  cofsmo  7897  alephsing  7904  sornom  7905  axdc3lem4  8081  zorn2lem1  8125  ttukeylem6  8143  ttukeylem7  8144  prlem934  8659  fzosubel3  10912  seqsplit  11081  seqcaopr  11085  ccatass  11438  splid  11470  spllen  11471  splfv1  11472  splfv2a  11473  splval2  11474  wrdeqcats1  11476  wrdeqs1cat  11477  swrds2  11562  isercolllem2  12141  fsumiun  12281  pcgcd1  12931  firest  13339  iscatd2  13585  posasymb  14088  meetle  14136  lattrd  14166  latleeqj1  14171  latjlej1  14173  latjlej12  14175  latnlej2  14179  latjidm  14182  latleeqm1  14187  latmlem1  14189  latmlem12  14191  latmidm  14194  latledi  14197  latjass  14203  latj12  14204  latj13  14206  latj31  14207  latjrot  14208  latj4  14209  mod1ile  14213  lubun  14229  clatleglb  14232  latdisdlem  14294  mnd32g  14378  mnd12g  14379  mnd4g  14380  prdsmndd  14407  imasmnd  14412  gsumspl  14468  grpinvinv  14537  grplmulf1o  14544  grpinvadd  14546  grpsubrcan  14549  grpsubadd  14555  grpaddsubass  14557  grppncan  14558  grpsubsub4  14560  grppnpcan2  14561  grpnpncan  14562  grpnnncan2  14563  grplactcnv  14566  mulgnn0dir  14592  mulgdirlem  14593  mulgneg2  14596  mulgnnass  14597  mulgnn0ass  14598  mulgass  14599  imasgrp  14613  nsgconj  14652  isnsg3  14653  nmzsubg  14660  ssnmz  14661  eqger  14669  eqgcpbl  14673  conjghm  14715  conjnmz  14718  conjnmzb  14719  subgga  14756  gass  14757  gasubg  14758  galcan  14760  gacan  14761  gapm  14762  gaorber  14764  gastacl  14765  gastacos  14766  cntzsubm  14813  cntzsubg  14814  oppgmnd  14829  odmodnn0  14857  mndodconglem  14858  odmod  14863  odcong  14866  odmulgid  14869  odbezout  14873  gexdvdsi  14896  gexdvds  14897  sylow1lem2  14912  sylow1lem4  14914  sylow2blem1  14933  sylow2blem2  14934  sylow2blem3  14935  sylow3lem1  14940  sylow3lem2  14941  lsmass  14981  lsmmod  14986  lsmdisj2  14993  subgdisj1  15002  efgredleme  15054  efgredlemc  15056  efgcpbllemb  15066  frgp0  15071  frgpuplem  15083  abl32  15112  abladdsub4  15117  abladdsub  15118  ablpncan2  15119  ablsubsub  15121  mulgdi  15128  mulgsubdi  15131  odadd1  15142  odadd2  15143  gex2abl  15145  oddvdssubg  15149  cygabl  15179  ablfacrp  15303  pgpfac1lem2  15312  pgpfac1lem3a  15313  pgpfac1lem3  15314  pgpfac1lem4  15315  rngcom  15371  rnglz  15379  rngrz  15380  rngnegl  15382  rngnegr  15383  rngmneg1  15384  rngmneg2  15385  rngsubdi  15387  rngsubdir  15388  mulgass2  15389  prdsrngd  15397  imasrng  15404  opprrng  15415  mulgass3  15421  dvdsrtr  15436  dvdsrmul1  15437  unitgrp  15451  dvrass  15474  dvrcan1  15475  dvrcan3  15476  irredrmul  15491  drngmul0or  15535  subrginv  15563  cntzsubr  15579  lmod0vs  15665  lmodvs0  15666  lmodvneg1  15669  lmodvsneg  15671  lmodcom  15673  lmodsubvs  15683  lmodsubdi  15684  lmodsubdir  15685  lssvsubcl  15703  lssvacl  15713  lssvscl  15714  islss3  15718  lss1d  15722  lssintcl  15723  prdslmodd  15728  lmodvsinv  15795  lmodvsinv2  15796  lmhmplusg  15803  lmhmvsca  15804  lsmcl  15838  pj1lmhm  15855  lvecvs0or  15863  lssvs0or  15865  lvecinv  15868  lspsnvs  15869  lspfixed  15883  lspexch  15884  lspsolvlem  15897  lspsolv  15898  lssacsex  15899  lspsnat  15900  lsppratlem1  15902  lsppratlem3  15904  lsppratlem4  15905  lbsextlem2  15914  lbsextlem4  15916  sralmod  15941  2idlcpbl  15988  unitrrg  16036  issubassa  16066  sraassa  16067  asclghm  16080  asclmul1  16081  asclmul2  16082  asclrhm  16083  psrbagcon  16119  psrbagconcl  16121  psrbagconf1o  16122  gsumbagdiaglem  16123  psrmulcllem  16134  psrlidm  16150  psrridm  16151  psrass1  16152  psrdi  16153  psrdir  16154  psrcom  16155  psrass23  16156  mplmon2mul  16244  coe1subfv  16345  mulgrhm  16462  cygznlem3  16525  ipdi  16546  ip2di  16547  ipsubdir  16548  ipsubdi  16549  ip2subdi  16550  ipassr  16552  ipassr2  16553  ip2eq  16559  ocvlss  16574  lsmcss  16594  iinopn  16650  subbascn  16986  cnhaus  17084  nrmsep2  17086  nrmsep  17087  regsep2  17106  isreg2  17107  hauscmplem  17135  1stcfb  17173  2ndcctbss  17183  ptbasfi  17278  pthaus  17334  txtube  17336  txhaus  17343  xkohaus  17349  kqnrmlem1  17436  kqnrmlem2  17437  nrmr0reg  17442  nrmhmph  17487  fbssint  17535  infil  17560  fgabs  17576  filcon  17580  filuni  17582  trfil2  17584  trfg  17588  ufprim  17606  elfm3  17647  rnelfm  17650  fmfnfmlem2  17652  fmfnfmlem4  17654  hausflimi  17677  hauspwpwf1  17684  fclsneii  17714  supnfcls  17717  flimfnfcls  17725  fclscmpi  17726  alexsublem  17740  ghmcnp  17799  divstgpopn  17804  xmetge0  17911  xmetsym  17914  xmettri  17917  xmetres2  17927  prdsxmetlem  17934  prdsmet  17936  imasdsf1olem  17939  imasf1oxmet  17941  bldisj  17957  xblss2  17960  xmeter  17981  prdsbl  18039  nrmmetd  18099  ngpsubcan  18137  nmmtri  18145  nmrtri  18147  ngptgp  18154  nlmvscnlem2  18198  nrginvrcnlem  18203  metdcnlem  18343  clmmulg  18593  cphabscl  18623  cphsqrcl2  18624  cphsqrcl3  18625  cphnmf  18633  cph2ass  18650  ipcau2  18666  tchcphlem2  18668  ipcnlem2  18673  cfilfcls  18702  iscau3  18706  iscmet3lem2  18720  iscmet3  18721  relcmpcmet  18744  minveclem2  18792  minveclem4  18798  pjthlem1  18803  pjthlem2  18804  uniioombllem4  18943  dyadmax  18955  itg1addlem4  19056  itg1climres  19071  evlslem1  19401  ply1divex  19524  aalioulem2  19715  amgmlem  20286  dvdsppwf1o  20428  perfect1  20469  perfectlem1  20470  perfectlem2  20471  dchrptlem2  20506  grpoidinvlem4  20876  grpoasscan2  20907  grpoinvop  20910  grpopncan  20920  grponpcan  20921  grpopnpcan2  20922  grpodiveq  20925  gxcom  20938  gxnn0add  20943  ghgrp  21037  rngo2  21057  rngolz  21070  rngorz  21071  vcm  21129  nvmul0or  21212  nvpncan2  21216  nvnncan  21223  nvdif  21233  nvabs  21241  smcnlem  21272  lnomul  21340  minvecolem2  21456  superpos  22936  ballotlemiex  23062  ssnnssfz  23279  lmxrge0  23377  cvmopnlem  23811  cvmliftmolem2  23815  cvmliftlem6  23823  cvmliftlem8  23825  cvmliftlem9  23826  cvmlift2lem9  23844  cvmlift3lem2  23853  cvmlift3lem6  23857  cvmlift3lem7  23858  cvmlift3lem9  23860  eupa0  23900  eupares  23901  eupap1  23902  nodense  24345  axcontlem9  24602  cgrtriv  24627  cgrdegen  24629  cgrextend  24633  segconeq  24635  btwntriv2  24637  btwncomand  24640  btwntriv1  24641  btwnintr  24644  btwnexch3  24645  btwnouttr  24649  btwnexch  24650  trisegint  24653  ifscgr  24669  btwnxfr  24681  colineartriv1  24692  colineartriv2  24693  colinearxfr  24700  fscgr  24705  lineid  24708  idinside  24709  endofsegidand  24711  btwnconn1lem5  24716  btwnconn1lem7  24718  btwnconn1lem11  24722  btwnconn1lem12  24723  btwnconn1lem13  24724  brsegle2  24734  segleantisym  24740  broutsideof2  24747  btwnoutside  24750  outsideoftr  24754  outsideofeq  24755  outsideofeu  24756  outsidele  24757  lineunray  24772  lineelsb2  24773  linecom  24775  linethru  24778  resgcom  25362  fprodsub  25390  trran2  25404  cmprtr  25407  ltrran2  25414  ltrinvlem  25417  cmprltr  25421  rltrran  25425  rltrooo  25426  multinv  25433  multinvb  25434  zerdivemp1  25447  mvecrtol  25484  mvecrtol2  25488  mulveczer  25490  mulinvsca  25491  muldisc  25492  glmrngo  25493  cmptdst2  25582  flfnei2  25588  addcanrg  25678  negveud  25679  negveudr  25680  issubrv  25683  neibastop1  26319  syl3an2cOLDOLD  26346  mettrifi  26484  isbnd3  26519  heibor1lem  26544  bfplem2  26558  ghomdiv  26585  zerdivemp1x  26597  irrapxlem5  26922  aomclem2  27163  frlmup1  27261  isnumbasgrplem2  27280  mpaaeu  27366  symggen  27422  mamuass  27471  mamudi  27472  mamudir  27473  mamuvs1  27474  mamuvs2  27475  mendrng  27511  mendlmod  27512  caofcan  27551  lubunNEW  29236  lfladdcl  29334  lflvscl  29340  eqlkr3  29364  lkrlsp  29365  lshpkrlem4  29376  oldmm1  29480  olj01  29488  latmassOLD  29492  latm32  29494  latmrot  29495  latm4  29496  olm01  29499  cmtcomlemN  29511  cmtbr3N  29517  cmtbr4N  29518  lecmtN  29519  omlfh1N  29521  atlen0  29573  atnle  29580  atlatmstc  29582  atlatle  29583  cvlexchb1  29593  cvlcvr1  29602  ishlat3N  29617  hlatjass  29632  hlatj12  29633  hlatj32  29634  hlsupr2  29649  hlhgt2  29651  hl0lt1N  29652  hlrelat  29664  hlrelat2  29665  exatleN  29666  hlrelat3  29674  cvrval5  29677  cvrexchlem  29681  cvratlem  29683  cvrat  29684  atcvr0eq  29688  lnnat  29689  atlt  29699  atlelt  29700  2atlt  29701  atexchltN  29703  cvrat3  29704  2atjm  29707  atbtwn  29708  4noncolr3  29715  athgt  29718  3dimlem3a  29722  3dimlem3OLDN  29724  3dimlem4a  29725  3dimlem4OLDN  29727  3dim1  29729  3dim2  29730  1cvratex  29735  ps-1  29739  ps-2  29740  hlatexch3N  29742  hlatexch4  29743  ps-2b  29744  3atlem1  29745  3atlem2  29746  3atlem5  29749  3atlem6  29750  llnnleat  29775  llncmp  29784  2at0mat0  29787  2atmat0  29788  2atm  29789  lplni2  29799  lvolex3N  29800  lplnnle2at  29803  lplnnleat  29804  lplnnlelln  29805  2atnelpln  29806  llncvrlpln  29820  2atmat  29823  lplncmp  29824  lplnexllnN  29826  2llnjaN  29828  2llnm4  29832  2llnmeqat  29833  lvolnle3at  29844  lvolnleat  29845  2atnelvolN  29849  islvol2aN  29854  4atlem3  29858  4atlem3a  29859  4atlem3b  29860  4atlem4a  29861  4atlem4b  29862  4atlem4c  29863  4atlem4d  29864  4atlem10  29868  4atlem11b  29870  4atlem11  29871  4atlem12b  29873  4atlem12  29874  4at2  29876  lplncvrlvol  29878  lvolcmp  29879  2lplnja  29881  dalemqrprot  29910  dalemply  29916  dalemsly  29917  dalemrot  29919  dalemrotyz  29920  dalem1  29921  dalemcea  29922  dalem3  29926  dalem5  29929  dalem8  29932  dalem-cly  29933  dalem11  29936  dalem12  29937  dalem16  29941  dalem17  29942  dalem18  29943  dalem21  29956  dalem24  29959  dalem25  29960  dalem38  29972  dalem39  29973  dalem44  29978  dalem54  29988  dalem55  29989  dalem57  29991  dalem58  29992  dalem59  29993  dalem60  29994  dath2  29999  2atm2atN  30047  2llnma1b  30048  2llnma3r  30050  cdlema1N  30053  cdlemblem  30055  paddasslem5  30086  paddasslem10  30091  paddasslem12  30093  paddasslem13  30094  paddass  30100  padd12N  30101  padd4N  30102  paddss  30107  pmodlem1  30108  pmodl42N  30113  pmapjoin  30114  pmapjlln1  30117  atmod1i2  30121  llnmod1i2  30122  llnexchb2  30131  dalawlem2  30134  dalawlem3  30135  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem11  30143  dalawlem12  30144  dalawlem13  30145  pclunN  30160  osumcllem1N  30218  pexmidlem3N  30234  lhp2lt  30263  lhp0lt  30265  lhpexle2lem  30271  lhpexle3lem  30273  lhpocnle  30278  lhpj1  30284  lhpmcvr4N  30288  lhp2at0  30294  lhpat3  30308  4atexlemtlw  30329  4atexlemc  30331  4atexlemnclw  30332  4atexlemcnd  30334  lautcvr  30354  lautj  30355  lautm  30356  ltrnm  30393  ltrnj  30394  ltrncvr  30395  trlval3  30449  cdlemc5  30457  cdlemd2  30461  cdlemd3  30462  cdleme0e  30479  cdleme1  30489  cdleme3c  30492  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme5  30502  cdleme7c  30507  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme9  30515  cdleme11c  30523  cdleme11g  30527  cdleme11k  30530  cdleme11  30532  cdleme12  30533  cdleme15b  30537  cdleme15d  30539  cdleme16d  30543  cdleme16e  30544  cdleme16f  30545  cdleme17b  30549  cdleme18b  30554  cdleme22gb  30556  cdlemednpq  30561  cdleme19a  30565  cdleme20aN  30571  cdleme20bN  30572  cdleme20c  30573  cdleme20d  30574  cdleme20j  30580  cdleme21c  30589  cdleme22aa  30601  cdleme22b  30603  cdleme22cN  30604  cdleme22d  30605  cdleme22e  30606  cdleme22eALTN  30607  cdleme23b  30612  cdleme23c  30613  cdleme28a  30632  cdleme30a  30640  cdlemefs29bpre0N  30678  cdlemefs29bpre1N  30679  cdlemefs29cpre1N  30680  cdlemefs29clN  30681  cdlemefs32fvaN  30684  cdlemefs32fva1  30685  cdleme32b  30704  cdleme32c  30705  cdleme32e  30707  cdleme35a  30710  cdleme35fnpq  30711  cdleme35b  30712  cdleme35f  30716  cdleme36a  30722  cdleme36m  30723  cdleme37m  30724  cdleme39a  30727  cdleme42c  30734  cdleme42i  30745  cdleme42keg  30748  cdleme42mgN  30750  cdleme48bw  30764  cdlemeg46fjgN  30783  cdlemeg46fjv  30785  cdlemeg46req  30791  cdleme50trn1  30811  cdlemf1  30823  cdlemf2  30824  cdlemg1cex  30850  cdlemg2fv2  30862  cdlemg7fvbwN  30869  cdlemg4c  30874  cdlemg4  30879  cdlemg6c  30882  cdlemg8b  30890  cdlemg10c  30901  cdlemg10  30903  cdlemg11b  30904  cdlemg12f  30910  cdlemg13a  30913  cdlemg17a  30923  cdlemg17dALTN  30926  cdlemg18b  30941  cdlemg19a  30945  cdlemg27a  30954  cdlemg27b  30958  cdlemg33b0  30963  cdlemg33a  30968  cdlemg35  30975  trlcolem  30988  cdlemg42  30991  cdlemg46  30997  trljco  31002  tendopltp  31042  cdlemh1  31077  cdlemh2  31078  cdlemi1  31080  cdlemi  31082  cdlemk3  31095  cdlemk10  31105  cdlemk11  31111  cdlemk15  31117  cdlemk1u  31121  cdlemk5u  31123  cdlemk11u  31133  cdlemk39  31178  cdlemkid1  31184  cdlemk50  31214  cdlemk51  31215  erngdvlem3-rN  31260  tendocnv  31284  tendospcanN  31286  dialss  31309  dia2dimlem1  31327  dia2dimlem2  31328  dia2dimlem3  31329  dia2dimlem10  31336  dia2dimlem12  31338  dvhvaddass  31360  dvhlveclem  31371  cdlemm10N  31381  doca2N  31389  djajN  31400  dib1dim2  31431  diblss  31433  diclspsn  31457  cdlemn2  31458  cdlemn10  31469  dihjustlem  31479  dihord1  31481  dihord2a  31482  dihord2pre2  31489  dib2dim  31506  dih2dimb  31507  dih2dimbALTN  31508  dihopelvalcpre  31511  dihord5b  31522  dihord6b  31523  dihord5apre  31525  dihmeetlem1N  31553  dihglblem5apreN  31554  dihglblem2N  31557  dihglbcpreN  31563  dihmeetbclemN  31567  dihmeetlem3N  31568  dihmeetlem6  31572  dih1dimatlem  31592  djhcvat42  31678  dihjatcclem1  31681  dihjatcclem4  31684  dvh4dimat  31701  lcfl7lem  31762  lclkrlem2m  31782  lcfrlem1  31805  lcdvsass  31870  baerlem3lem1  31970  baerlem5alem1  31971  baerlem5blem1  31972  mapdh6gN  32005  mapdh6hN  32006  hdmap1l6g  32080  hdmap1l6h  32081  hdmapneg  32112  hdmap14lem8  32141  hgmapadd  32160  hgmapmul  32161  hgmapvvlem1  32189
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  df-3an 936
  Copyright terms: Public domain W3C validator