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

Theorem syl13anc 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 )
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 1134 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 643 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl23anc  1191  syl33anc  1199  pm2.61da3ne  2651  disjxiun  4173  wereu2  4543  ordelord  4567  caovassd  6209  caovcand  6212  caovordid  6216  caovordd  6218  caovdid  6225  caovdird  6228  swoer  6896  swoord1  6897  swoord2  6898  frfi  7315  indexfi  7376  ssfii  7386  elfiun  7397  suplub2  7426  wemaplem2  7476  htalem  7780  cofsmo  8109  alephsing  8116  sornom  8117  axdc3lem4  8293  zorn2lem1  8336  ttukeylem6  8354  ttukeylem7  8355  prlem934  8870  fzosubel3  11138  seqsplit  11315  seqcaopr  11319  ccatass  11709  splid  11741  spllen  11742  splfv1  11743  splfv2a  11744  splval2  11745  wrdeqcats1  11747  wrdeqs1cat  11748  swrds2  11839  isercolllem2  12418  fsumiun  12559  pcgcd1  13209  firest  13619  iscatd2  13865  posasymb  14368  meetle  14416  lattrd  14446  latleeqj1  14451  latjlej1  14453  latjlej12  14455  latnlej2  14459  latjidm  14462  latleeqm1  14467  latmlem1  14469  latmlem12  14471  latmidm  14474  latledi  14477  latjass  14483  latj12  14484  latj13  14486  latj31  14487  latjrot  14488  latj4  14489  mod1ile  14493  lubun  14509  clatleglb  14512  latdisdlem  14574  mnd32g  14658  mnd12g  14659  mnd4g  14660  prdsmndd  14687  imasmnd  14692  gsumspl  14748  grpinvinv  14817  grplmulf1o  14824  grpinvadd  14826  grpsubrcan  14829  grpsubadd  14835  grpaddsubass  14837  grppncan  14838  grpsubsub4  14840  grppnpcan2  14841  grpnpncan  14842  grpnnncan2  14843  grplactcnv  14846  mulgnn0dir  14872  mulgdirlem  14873  mulgneg2  14876  mulgnnass  14877  mulgnn0ass  14878  mulgass  14879  imasgrp  14893  nsgconj  14932  isnsg3  14933  nmzsubg  14940  ssnmz  14941  eqger  14949  eqgcpbl  14953  conjghm  14995  conjnmz  14998  conjnmzb  14999  subgga  15036  gass  15037  gasubg  15038  galcan  15040  gacan  15041  gapm  15042  gaorber  15044  gastacl  15045  gastacos  15046  cntzsubm  15093  cntzsubg  15094  oppgmnd  15109  odmodnn0  15137  mndodconglem  15138  odmod  15143  odcong  15146  odmulgid  15149  odbezout  15153  gexdvdsi  15176  gexdvds  15177  sylow1lem2  15192  sylow1lem4  15194  sylow2blem1  15213  sylow2blem2  15214  sylow2blem3  15215  sylow3lem1  15220  sylow3lem2  15221  lsmass  15261  lsmmod  15266  lsmdisj2  15273  subgdisj1  15282  efgredleme  15334  efgredlemc  15336  efgcpbllemb  15346  frgp0  15351  frgpuplem  15363  abl32  15392  abladdsub4  15397  abladdsub  15398  ablpncan2  15399  ablsubsub  15401  mulgdi  15408  mulgsubdi  15411  odadd1  15422  odadd2  15423  gex2abl  15425  oddvdssubg  15429  cygabl  15459  ablfacrp  15583  pgpfac1lem2  15592  pgpfac1lem3a  15593  pgpfac1lem3  15594  pgpfac1lem4  15595  rngcom  15651  rnglz  15659  rngrz  15660  rngnegl  15662  rngnegr  15663  rngmneg1  15664  rngmneg2  15665  rngsubdi  15667  rngsubdir  15668  mulgass2  15669  prdsrngd  15677  imasrng  15684  opprrng  15695  mulgass3  15701  dvdsrtr  15716  dvdsrmul1  15717  unitgrp  15731  dvrass  15754  dvrcan1  15755  dvrcan3  15756  irredrmul  15771  drngmul0or  15815  subrginv  15843  cntzsubr  15859  lmod0vs  15942  lmodvs0  15943  lmodvneg1  15946  lmodvsneg  15947  lmodcom  15949  lmodsubvs  15959  lmodsubdi  15960  lmodsubdir  15961  lssvsubcl  15979  lssvacl  15989  lssvscl  15990  islss3  15994  lss1d  15998  lssintcl  15999  prdslmodd  16004  lmodvsinv  16071  lmodvsinv2  16072  lmhmplusg  16079  lmhmvsca  16080  lsmcl  16114  pj1lmhm  16131  lvecvs0or  16139  lssvs0or  16141  lvecinv  16144  lspsnvs  16145  lspfixed  16159  lspexch  16160  lspsolvlem  16173  lspsolv  16174  lssacsex  16175  lspsnat  16176  lsppratlem1  16178  lsppratlem3  16180  lsppratlem4  16181  lbsextlem2  16190  lbsextlem4  16192  sralmod  16217  2idlcpbl  16264  unitrrg  16312  issubassa  16342  sraassa  16343  asclghm  16356  asclmul1  16357  asclmul2  16358  asclrhm  16359  psrbagcon  16395  psrbagconcl  16397  psrbagconf1o  16398  gsumbagdiaglem  16399  psrmulcllem  16410  psrlidm  16426  psrridm  16427  psrass1  16428  psrdi  16429  psrdir  16430  psrcom  16431  psrass23  16432  mplmon2mul  16520  coe1subfv  16618  mulgrhm  16746  cygznlem3  16809  ipdi  16830  ip2di  16831  ipsubdir  16832  ipsubdi  16833  ip2subdi  16834  ipassr  16836  ipassr2  16837  ip2eq  16843  ocvlss  16858  lsmcss  16878  iinopn  16934  subbascn  17276  cnhaus  17376  nrmsep2  17378  nrmsep  17379  regsep2  17398  isreg2  17399  hauscmplem  17427  1stcfb  17465  2ndcctbss  17475  ptbasfi  17570  pthaus  17627  txtube  17629  txhaus  17636  xkohaus  17642  kqnrmlem1  17732  kqnrmlem2  17733  nrmr0reg  17738  nrmhmph  17783  fbssint  17827  infil  17852  fgabs  17868  filcon  17872  filuni  17874  trfil2  17876  trfg  17880  ufprim  17898  elfm3  17939  rnelfm  17942  fmfnfmlem2  17944  fmfnfmlem4  17946  hausflimi  17969  hauspwpwf1  17976  fclsneii  18006  supnfcls  18009  flimfnfcls  18017  fclscmpi  18018  alexsublem  18032  ghmcnp  18101  divstgpopn  18106  psmetsym  18298  psmettri  18299  psmetge0  18300  psmetres2  18302  xmetge0  18331  xmetsym  18334  xmettri  18338  xmetres2  18348  prdsxmetlem  18355  prdsmet  18357  imasdsf1olem  18360  imasf1oxmet  18362  bldisj  18385  xblss2ps  18388  xblss2  18389  xmeter  18420  prdsbl  18478  metustexhalfOLD  18550  metustexhalf  18551  metustOLD  18554  metust  18555  nrmmetd  18579  ngpsubcan  18617  nmmtri  18625  nmrtri  18627  ngptgp  18634  nlmvscnlem2  18678  nrginvrcnlem  18683  metdcnlem  18824  clmmulg  19075  cphabscl  19105  cphsqrcl2  19106  cphsqrcl3  19107  cphnmf  19115  cph2ass  19132  ipcau2  19148  tchcphlem2  19150  ipcnlem2  19155  cfilfcls  19184  iscau3  19188  iscmet3lem2  19202  iscmet3  19203  relcmpcmet  19226  minveclem2  19284  minveclem4  19290  pjthlem1  19295  pjthlem2  19296  uniioombllem4  19435  dyadmax  19447  itg1addlem4  19548  itg1climres  19563  evlslem1  19893  ply1divex  20016  aalioulem2  20207  amgmlem  20785  dvdsppwf1o  20928  perfect1  20969  perfectlem1  20970  perfectlem2  20971  dchrptlem2  21006  4cycl4dv4e  21612  eupa0  21653  eupares  21654  eupap1  21655  grpoidinvlem4  21752  grpoasscan2  21783  grpoinvop  21786  grpopncan  21796  grponpcan  21797  grpopnpcan2  21798  grpodiveq  21801  gxcom  21814  gxnn0add  21819  ghgrp  21913  rngo2  21933  rngolz  21946  rngorz  21947  zerdivemp1  21979  vcm  22007  nvmul0or  22090  nvpncan2  22094  nvnncan  22101  nvdif  22111  nvabs  22119  smcnlem  22150  lnomul  22218  minvecolem2  22334  superpos  23814  ssnnssfz  24105  dvrdir  24183  rdivmuldivd  24184  dvrcan5  24186  rhmdvd  24216  rhmunitinv  24217  metideq  24245  metider  24246  pstmxmet  24249  lmxrge0  24294  qqhghm  24329  qqhrhm  24330  ballotlemiex  24716  cvmopnlem  24922  cvmliftmolem2  24926  cvmliftlem6  24934  cvmliftlem8  24936  cvmliftlem9  24937  cvmlift2lem9  24955  cvmlift3lem2  24964  cvmlift3lem6  24968  cvmlift3lem7  24969  cvmlift3lem9  24971  zprod  25220  nodense  25561  axcontlem9  25819  cgrtriv  25844  cgrdegen  25846  cgrextend  25850  segconeq  25852  btwntriv2  25854  btwncomand  25857  btwntriv1  25858  btwnintr  25861  btwnexch3  25862  btwnouttr  25866  btwnexch  25867  trisegint  25870  ifscgr  25886  btwnxfr  25898  colineartriv1  25909  colineartriv2  25910  colinearxfr  25917  fscgr  25922  lineid  25925  idinside  25926  endofsegidand  25928  btwnconn1lem5  25933  btwnconn1lem7  25935  btwnconn1lem11  25939  btwnconn1lem12  25940  btwnconn1lem13  25941  brsegle2  25951  segleantisym  25957  broutsideof2  25964  btwnoutside  25967  outsideoftr  25971  outsideofeq  25972  outsideofeu  25973  outsidele  25974  lineunray  25989  lineelsb2  25990  linecom  25992  linethru  25995  neibastop1  26282  mettrifi  26357  isbnd3  26387  heibor1lem  26412  bfplem2  26426  ghomdiv  26453  zerdivemp1x  26465  irrapxlem5  26783  aomclem2  27024  frlmup1  27122  isnumbasgrplem2  27141  mpaaeu  27227  symggen  27283  mamuass  27332  mamudi  27333  mamudir  27334  mamuvs1  27335  mamuvs2  27336  mendrng  27372  mendlmod  27373  caofcan  27412  stoweidlem18  27638  stoweidlem41  27661  stoweidlem45  27665  stoweidlem55  27675  swrdccatin2  28022  el2spthonot0  28072  usg2spthonot1  28091  frg2woteu  28162  lubunNEW  29460  lfladdcl  29558  lflvscl  29564  eqlkr3  29588  lkrlsp  29589  lshpkrlem4  29600  oldmm1  29704  olj01  29712  latmassOLD  29716  latm32  29718  latmrot  29719  latm4  29720  olm01  29723  cmtcomlemN  29735  cmtbr3N  29741  cmtbr4N  29742  lecmtN  29743  omlfh1N  29745  atlen0  29797  atnle  29804  atlatmstc  29806  atlatle  29807  cvlexchb1  29817  cvlcvr1  29826  ishlat3N  29841  hlatjass  29856  hlatj12  29857  hlatj32  29858  hlsupr2  29873  hlhgt2  29875  hl0lt1N  29876  hlrelat  29888  hlrelat2  29889  exatleN  29890  hlrelat3  29898  cvrval5  29901  cvrexchlem  29905  cvratlem  29907  cvrat  29908  atcvr0eq  29912  lnnat  29913  atlt  29923  atlelt  29924  2atlt  29925  atexchltN  29927  cvrat3  29928  2atjm  29931  atbtwn  29932  4noncolr3  29939  athgt  29942  3dimlem3a  29946  3dimlem3OLDN  29948  3dimlem4a  29949  3dimlem4OLDN  29951  3dim1  29953  3dim2  29954  1cvratex  29959  ps-1  29963  ps-2  29964  hlatexch3N  29966  hlatexch4  29967  ps-2b  29968  3atlem1  29969  3atlem2  29970  3atlem5  29973  3atlem6  29974  llnnleat  29999  llncmp  30008  2at0mat0  30011  2atmat0  30012  2atm  30013  lplni2  30023  lvolex3N  30024  lplnnle2at  30027  lplnnleat  30028  lplnnlelln  30029  2atnelpln  30030  llncvrlpln  30044  2atmat  30047  lplncmp  30048  lplnexllnN  30050  2llnjaN  30052  2llnm4  30056  2llnmeqat  30057  lvolnle3at  30068  lvolnleat  30069  2atnelvolN  30073  islvol2aN  30078  4atlem3  30082  4atlem3a  30083  4atlem3b  30084  4atlem4a  30085  4atlem4b  30086  4atlem4c  30087  4atlem4d  30088  4atlem10  30092  4atlem11b  30094  4atlem11  30095  4atlem12b  30097  4atlem12  30098  4at2  30100  lplncvrlvol  30102  lvolcmp  30103  2lplnja  30105  dalemqrprot  30134  dalemply  30140  dalemsly  30141  dalemrot  30143  dalemrotyz  30144  dalem1  30145  dalemcea  30146  dalem3  30150  dalem5  30153  dalem8  30156  dalem-cly  30157  dalem11  30160  dalem12  30161  dalem16  30165  dalem17  30166  dalem18  30167  dalem21  30180  dalem24  30183  dalem25  30184  dalem38  30196  dalem39  30197  dalem44  30202  dalem54  30212  dalem55  30213  dalem57  30215  dalem58  30216  dalem59  30217  dalem60  30218  dath2  30223  2atm2atN  30271  2llnma1b  30272  2llnma3r  30274  cdlema1N  30277  cdlemblem  30279  paddasslem5  30310  paddasslem10  30315  paddasslem12  30317  paddasslem13  30318  paddass  30324  padd12N  30325  padd4N  30326  paddss  30331  pmodlem1  30332  pmodl42N  30337  pmapjoin  30338  pmapjlln1  30341  atmod1i2  30345  llnmod1i2  30346  llnexchb2  30355  dalawlem2  30358  dalawlem3  30359  dalawlem5  30361  dalawlem6  30362  dalawlem7  30363  dalawlem8  30364  dalawlem11  30367  dalawlem12  30368  dalawlem13  30369  pclunN  30384  osumcllem1N  30442  pexmidlem3N  30458  lhp2lt  30487  lhp0lt  30489  lhpexle2lem  30495  lhpexle3lem  30497  lhpocnle  30502  lhpj1  30508  lhpmcvr4N  30512  lhp2at0  30518  lhpat3  30532  4atexlemtlw  30553  4atexlemc  30555  4atexlemnclw  30556  4atexlemcnd  30558  lautcvr  30578  lautj  30579  lautm  30580  ltrnm  30617  ltrnj  30618  ltrncvr  30619  trlval3  30673  cdlemc5  30681  cdlemd2  30685  cdlemd3  30686  cdleme0e  30703  cdleme1  30713  cdleme3c  30716  cdleme3g  30720  cdleme3h  30721  cdleme3  30723  cdleme5  30726  cdleme7c  30731  cdleme7d  30732  cdleme7e  30733  cdleme7ga  30734  cdleme7  30735  cdleme9  30739  cdleme11c  30747  cdleme11g  30751  cdleme11k  30754  cdleme11  30756  cdleme12  30757  cdleme15b  30761  cdleme15d  30763  cdleme16d  30767  cdleme16e  30768  cdleme16f  30769  cdleme17b  30773  cdleme18b  30778  cdleme22gb  30780  cdlemednpq  30785  cdleme19a  30789  cdleme20aN  30795  cdleme20bN  30796  cdleme20c  30797  cdleme20d  30798  cdleme20j  30804  cdleme21c  30813  cdleme22aa  30825  cdleme22b  30827  cdleme22cN  30828  cdleme22d  30829  cdleme22e  30830  cdleme22eALTN  30831  cdleme23b  30836  cdleme23c  30837  cdleme28a  30856  cdleme30a  30864  cdlemefs29bpre0N  30902  cdlemefs29bpre1N  30903  cdlemefs29cpre1N  30904  cdlemefs29clN  30905  cdlemefs32fvaN  30908  cdlemefs32fva1  30909  cdleme32b  30928  cdleme32c  30929  cdleme32e  30931  cdleme35a  30934  cdleme35fnpq  30935  cdleme35b  30936  cdleme35f  30940  cdleme36a  30946  cdleme36m  30947  cdleme37m  30948  cdleme39a  30951  cdleme42c  30958  cdleme42i  30969  cdleme42keg  30972  cdleme42mgN  30974  cdleme48bw  30988  cdlemeg46fjgN  31007  cdlemeg46fjv  31009  cdlemeg46req  31015  cdleme50trn1  31035  cdlemf1  31047  cdlemf2  31048  cdlemg1cex  31074  cdlemg2fv2  31086  cdlemg7fvbwN  31093  cdlemg4c  31098  cdlemg4  31103  cdlemg6c  31106  cdlemg8b  31114  cdlemg10c  31125  cdlemg10  31127  cdlemg11b  31128  cdlemg12f  31134  cdlemg13a  31137  cdlemg17a  31147  cdlemg17dALTN  31150  cdlemg18b  31165  cdlemg19a  31169  cdlemg27a  31178  cdlemg27b  31182  cdlemg33b0  31187  cdlemg33a  31192  cdlemg35  31199  trlcolem  31212  cdlemg42  31215  cdlemg46  31221  trljco  31226  tendopltp  31266  cdlemh1  31301  cdlemh2  31302  cdlemi1  31304  cdlemi  31306  cdlemk3  31319  cdlemk10  31329  cdlemk11  31335  cdlemk15  31341  cdlemk1u  31345  cdlemk5u  31347  cdlemk11u  31357  cdlemk39  31402  cdlemkid1  31408  cdlemk50  31438  cdlemk51  31439  erngdvlem3-rN  31484  tendocnv  31508  tendospcanN  31510  dialss  31533  dia2dimlem1  31551  dia2dimlem2  31552  dia2dimlem3  31553  dia2dimlem10  31560  dia2dimlem12  31562  dvhvaddass  31584  dvhlveclem  31595  cdlemm10N  31605  doca2N  31613  djajN  31624  dib1dim2  31655  diblss  31657  diclspsn  31681  cdlemn2  31682  cdlemn10  31693  dihjustlem  31703  dihord1  31705  dihord2a  31706  dihord2pre2  31713  dib2dim  31730  dih2dimb  31731  dih2dimbALTN  31732  dihopelvalcpre  31735  dihord5b  31746  dihord6b  31747  dihord5apre  31749  dihmeetlem1N  31777  dihglblem5apreN  31778  dihglblem2N  31781  dihglbcpreN  31787  dihmeetbclemN  31791  dihmeetlem3N  31792  dihmeetlem6  31796  dih1dimatlem  31816  djhcvat42  31902  dihjatcclem1  31905  dihjatcclem4  31908  dvh4dimat  31925  lcfl7lem  31986  lclkrlem2m  32006  lcfrlem1  32029  lcdvsass  32094  baerlem3lem1  32194  baerlem5alem1  32195  baerlem5blem1  32196  mapdh6gN  32229  mapdh6hN  32230  hdmap1l6g  32304  hdmap1l6h  32305  hdmapneg  32336  hdmap14lem8  32365  hgmapadd  32384  hgmapmul  32385  hgmapvvlem1  32413
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator