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  2630  disjxiun  4150  wereu2  4520  ordelord  4544  caovassd  6185  caovcand  6188  caovordid  6192  caovordd  6194  caovdid  6201  caovdird  6204  swoer  6869  swoord1  6870  swoord2  6871  frfi  7288  indexfi  7349  ssfii  7359  elfiun  7370  suplub2  7399  wemaplem2  7449  htalem  7753  cofsmo  8082  alephsing  8089  sornom  8090  axdc3lem4  8266  zorn2lem1  8309  ttukeylem6  8327  ttukeylem7  8328  prlem934  8843  fzosubel3  11107  seqsplit  11283  seqcaopr  11287  ccatass  11677  splid  11709  spllen  11710  splfv1  11711  splfv2a  11712  splval2  11713  wrdeqcats1  11715  wrdeqs1cat  11716  swrds2  11807  isercolllem2  12386  fsumiun  12527  pcgcd1  13177  firest  13587  iscatd2  13833  posasymb  14336  meetle  14384  lattrd  14414  latleeqj1  14419  latjlej1  14421  latjlej12  14423  latnlej2  14427  latjidm  14430  latleeqm1  14435  latmlem1  14437  latmlem12  14439  latmidm  14442  latledi  14445  latjass  14451  latj12  14452  latj13  14454  latj31  14455  latjrot  14456  latj4  14457  mod1ile  14461  lubun  14477  clatleglb  14480  latdisdlem  14542  mnd32g  14626  mnd12g  14627  mnd4g  14628  prdsmndd  14655  imasmnd  14660  gsumspl  14716  grpinvinv  14785  grplmulf1o  14792  grpinvadd  14794  grpsubrcan  14797  grpsubadd  14803  grpaddsubass  14805  grppncan  14806  grpsubsub4  14808  grppnpcan2  14809  grpnpncan  14810  grpnnncan2  14811  grplactcnv  14814  mulgnn0dir  14840  mulgdirlem  14841  mulgneg2  14844  mulgnnass  14845  mulgnn0ass  14846  mulgass  14847  imasgrp  14861  nsgconj  14900  isnsg3  14901  nmzsubg  14908  ssnmz  14909  eqger  14917  eqgcpbl  14921  conjghm  14963  conjnmz  14966  conjnmzb  14967  subgga  15004  gass  15005  gasubg  15006  galcan  15008  gacan  15009  gapm  15010  gaorber  15012  gastacl  15013  gastacos  15014  cntzsubm  15061  cntzsubg  15062  oppgmnd  15077  odmodnn0  15105  mndodconglem  15106  odmod  15111  odcong  15114  odmulgid  15117  odbezout  15121  gexdvdsi  15144  gexdvds  15145  sylow1lem2  15160  sylow1lem4  15162  sylow2blem1  15181  sylow2blem2  15182  sylow2blem3  15183  sylow3lem1  15188  sylow3lem2  15189  lsmass  15229  lsmmod  15234  lsmdisj2  15241  subgdisj1  15250  efgredleme  15302  efgredlemc  15304  efgcpbllemb  15314  frgp0  15319  frgpuplem  15331  abl32  15360  abladdsub4  15365  abladdsub  15366  ablpncan2  15367  ablsubsub  15369  mulgdi  15376  mulgsubdi  15379  odadd1  15390  odadd2  15391  gex2abl  15393  oddvdssubg  15397  cygabl  15427  ablfacrp  15551  pgpfac1lem2  15560  pgpfac1lem3a  15561  pgpfac1lem3  15562  pgpfac1lem4  15563  rngcom  15619  rnglz  15627  rngrz  15628  rngnegl  15630  rngnegr  15631  rngmneg1  15632  rngmneg2  15633  rngsubdi  15635  rngsubdir  15636  mulgass2  15637  prdsrngd  15645  imasrng  15652  opprrng  15663  mulgass3  15669  dvdsrtr  15684  dvdsrmul1  15685  unitgrp  15699  dvrass  15722  dvrcan1  15723  dvrcan3  15724  irredrmul  15739  drngmul0or  15783  subrginv  15811  cntzsubr  15827  lmod0vs  15910  lmodvs0  15911  lmodvneg1  15914  lmodvsneg  15915  lmodcom  15917  lmodsubvs  15927  lmodsubdi  15928  lmodsubdir  15929  lssvsubcl  15947  lssvacl  15957  lssvscl  15958  islss3  15962  lss1d  15966  lssintcl  15967  prdslmodd  15972  lmodvsinv  16039  lmodvsinv2  16040  lmhmplusg  16047  lmhmvsca  16048  lsmcl  16082  pj1lmhm  16099  lvecvs0or  16107  lssvs0or  16109  lvecinv  16112  lspsnvs  16113  lspfixed  16127  lspexch  16128  lspsolvlem  16141  lspsolv  16142  lssacsex  16143  lspsnat  16144  lsppratlem1  16146  lsppratlem3  16148  lsppratlem4  16149  lbsextlem2  16158  lbsextlem4  16160  sralmod  16185  2idlcpbl  16232  unitrrg  16280  issubassa  16310  sraassa  16311  asclghm  16324  asclmul1  16325  asclmul2  16326  asclrhm  16327  psrbagcon  16363  psrbagconcl  16365  psrbagconf1o  16366  gsumbagdiaglem  16367  psrmulcllem  16378  psrlidm  16394  psrridm  16395  psrass1  16396  psrdi  16397  psrdir  16398  psrcom  16399  psrass23  16400  mplmon2mul  16488  coe1subfv  16586  mulgrhm  16710  cygznlem3  16773  ipdi  16794  ip2di  16795  ipsubdir  16796  ipsubdi  16797  ip2subdi  16798  ipassr  16800  ipassr2  16801  ip2eq  16807  ocvlss  16822  lsmcss  16842  iinopn  16898  subbascn  17240  cnhaus  17340  nrmsep2  17342  nrmsep  17343  regsep2  17362  isreg2  17363  hauscmplem  17391  1stcfb  17429  2ndcctbss  17439  ptbasfi  17534  pthaus  17591  txtube  17593  txhaus  17600  xkohaus  17606  kqnrmlem1  17696  kqnrmlem2  17697  nrmr0reg  17702  nrmhmph  17747  fbssint  17791  infil  17816  fgabs  17832  filcon  17836  filuni  17838  trfil2  17840  trfg  17844  ufprim  17862  elfm3  17903  rnelfm  17906  fmfnfmlem2  17908  fmfnfmlem4  17910  hausflimi  17933  hauspwpwf1  17940  fclsneii  17970  supnfcls  17973  flimfnfcls  17981  fclscmpi  17982  alexsublem  17996  ghmcnp  18065  divstgpopn  18070  xmetge0  18283  xmetsym  18286  xmettri  18289  xmetres2  18299  prdsxmetlem  18306  prdsmet  18308  imasdsf1olem  18311  imasf1oxmet  18313  bldisj  18329  xblss2  18332  xmeter  18353  prdsbl  18411  metustexhalf  18476  metust  18478  nrmmetd  18493  ngpsubcan  18531  nmmtri  18539  nmrtri  18541  ngptgp  18548  nlmvscnlem2  18592  nrginvrcnlem  18597  metdcnlem  18738  clmmulg  18989  cphabscl  19019  cphsqrcl2  19020  cphsqrcl3  19021  cphnmf  19029  cph2ass  19046  ipcau2  19062  tchcphlem2  19064  ipcnlem2  19069  cfilfcls  19098  iscau3  19102  iscmet3lem2  19116  iscmet3  19117  relcmpcmet  19140  minveclem2  19194  minveclem4  19200  pjthlem1  19205  pjthlem2  19206  uniioombllem4  19345  dyadmax  19357  itg1addlem4  19458  itg1climres  19473  evlslem1  19803  ply1divex  19926  aalioulem2  20117  amgmlem  20695  dvdsppwf1o  20838  perfect1  20879  perfectlem1  20880  perfectlem2  20881  dchrptlem2  20916  4cycl4dv4e  21503  eupa0  21544  eupares  21545  eupap1  21546  grpoidinvlem4  21643  grpoasscan2  21674  grpoinvop  21677  grpopncan  21687  grponpcan  21688  grpopnpcan2  21689  grpodiveq  21692  gxcom  21705  gxnn0add  21710  ghgrp  21804  rngo2  21824  rngolz  21837  rngorz  21838  zerdivemp1  21870  vcm  21898  nvmul0or  21981  nvpncan2  21985  nvnncan  21992  nvdif  22002  nvabs  22010  smcnlem  22041  lnomul  22109  minvecolem2  22225  superpos  23705  ssnnssfz  23984  dvrdir  24055  rdivmuldivd  24056  dvrcan5  24058  rhmdvd  24075  rhmunitinv  24076  lmxrge0  24141  qqhghm  24171  qqhrhm  24172  ballotlemiex  24538  cvmopnlem  24744  cvmliftmolem2  24748  cvmliftlem6  24756  cvmliftlem8  24758  cvmliftlem9  24759  cvmlift2lem9  24777  cvmlift3lem2  24786  cvmlift3lem6  24790  cvmlift3lem7  24791  cvmlift3lem9  24793  zprod  25042  nodense  25367  axcontlem9  25625  cgrtriv  25650  cgrdegen  25652  cgrextend  25656  segconeq  25658  btwntriv2  25660  btwncomand  25663  btwntriv1  25664  btwnintr  25667  btwnexch3  25668  btwnouttr  25672  btwnexch  25673  trisegint  25676  ifscgr  25692  btwnxfr  25704  colineartriv1  25715  colineartriv2  25716  colinearxfr  25723  fscgr  25728  lineid  25731  idinside  25732  endofsegidand  25734  btwnconn1lem5  25739  btwnconn1lem7  25741  btwnconn1lem11  25745  btwnconn1lem12  25746  btwnconn1lem13  25747  brsegle2  25757  segleantisym  25763  broutsideof2  25770  btwnoutside  25773  outsideoftr  25777  outsideofeq  25778  outsideofeu  25779  outsidele  25780  lineunray  25795  lineelsb2  25796  linecom  25798  linethru  25801  neibastop1  26079  mettrifi  26154  isbnd3  26184  heibor1lem  26209  bfplem2  26223  ghomdiv  26250  zerdivemp1x  26262  irrapxlem5  26580  aomclem2  26821  frlmup1  26919  isnumbasgrplem2  26938  mpaaeu  27024  symggen  27080  mamuass  27129  mamudi  27130  mamudir  27131  mamuvs1  27132  mamuvs2  27133  mendrng  27169  mendlmod  27170  caofcan  27209  stoweidlem18  27435  stoweidlem41  27458  stoweidlem45  27462  stoweidlem55  27472  lubunNEW  29088  lfladdcl  29186  lflvscl  29192  eqlkr3  29216  lkrlsp  29217  lshpkrlem4  29228  oldmm1  29332  olj01  29340  latmassOLD  29344  latm32  29346  latmrot  29347  latm4  29348  olm01  29351  cmtcomlemN  29363  cmtbr3N  29369  cmtbr4N  29370  lecmtN  29371  omlfh1N  29373  atlen0  29425  atnle  29432  atlatmstc  29434  atlatle  29435  cvlexchb1  29445  cvlcvr1  29454  ishlat3N  29469  hlatjass  29484  hlatj12  29485  hlatj32  29486  hlsupr2  29501  hlhgt2  29503  hl0lt1N  29504  hlrelat  29516  hlrelat2  29517  exatleN  29518  hlrelat3  29526  cvrval5  29529  cvrexchlem  29533  cvratlem  29535  cvrat  29536  atcvr0eq  29540  lnnat  29541  atlt  29551  atlelt  29552  2atlt  29553  atexchltN  29555  cvrat3  29556  2atjm  29559  atbtwn  29560  4noncolr3  29567  athgt  29570  3dimlem3a  29574  3dimlem3OLDN  29576  3dimlem4a  29577  3dimlem4OLDN  29579  3dim1  29581  3dim2  29582  1cvratex  29587  ps-1  29591  ps-2  29592  hlatexch3N  29594  hlatexch4  29595  ps-2b  29596  3atlem1  29597  3atlem2  29598  3atlem5  29601  3atlem6  29602  llnnleat  29627  llncmp  29636  2at0mat0  29639  2atmat0  29640  2atm  29641  lplni2  29651  lvolex3N  29652  lplnnle2at  29655  lplnnleat  29656  lplnnlelln  29657  2atnelpln  29658  llncvrlpln  29672  2atmat  29675  lplncmp  29676  lplnexllnN  29678  2llnjaN  29680  2llnm4  29684  2llnmeqat  29685  lvolnle3at  29696  lvolnleat  29697  2atnelvolN  29701  islvol2aN  29706  4atlem3  29710  4atlem3a  29711  4atlem3b  29712  4atlem4a  29713  4atlem4b  29714  4atlem4c  29715  4atlem4d  29716  4atlem10  29720  4atlem11b  29722  4atlem11  29723  4atlem12b  29725  4atlem12  29726  4at2  29728  lplncvrlvol  29730  lvolcmp  29731  2lplnja  29733  dalemqrprot  29762  dalemply  29768  dalemsly  29769  dalemrot  29771  dalemrotyz  29772  dalem1  29773  dalemcea  29774  dalem3  29778  dalem5  29781  dalem8  29784  dalem-cly  29785  dalem11  29788  dalem12  29789  dalem16  29793  dalem17  29794  dalem18  29795  dalem21  29808  dalem24  29811  dalem25  29812  dalem38  29824  dalem39  29825  dalem44  29830  dalem54  29840  dalem55  29841  dalem57  29843  dalem58  29844  dalem59  29845  dalem60  29846  dath2  29851  2atm2atN  29899  2llnma1b  29900  2llnma3r  29902  cdlema1N  29905  cdlemblem  29907  paddasslem5  29938  paddasslem10  29943  paddasslem12  29945  paddasslem13  29946  paddass  29952  padd12N  29953  padd4N  29954  paddss  29959  pmodlem1  29960  pmodl42N  29965  pmapjoin  29966  pmapjlln1  29969  atmod1i2  29973  llnmod1i2  29974  llnexchb2  29983  dalawlem2  29986  dalawlem3  29987  dalawlem5  29989  dalawlem6  29990  dalawlem7  29991  dalawlem8  29992  dalawlem11  29995  dalawlem12  29996  dalawlem13  29997  pclunN  30012  osumcllem1N  30070  pexmidlem3N  30086  lhp2lt  30115  lhp0lt  30117  lhpexle2lem  30123  lhpexle3lem  30125  lhpocnle  30130  lhpj1  30136  lhpmcvr4N  30140  lhp2at0  30146  lhpat3  30160  4atexlemtlw  30181  4atexlemc  30183  4atexlemnclw  30184  4atexlemcnd  30186  lautcvr  30206  lautj  30207  lautm  30208  ltrnm  30245  ltrnj  30246  ltrncvr  30247  trlval3  30301  cdlemc5  30309  cdlemd2  30313  cdlemd3  30314  cdleme0e  30331  cdleme1  30341  cdleme3c  30344  cdleme3g  30348  cdleme3h  30349  cdleme3  30351  cdleme5  30354  cdleme7c  30359  cdleme7d  30360  cdleme7e  30361  cdleme7ga  30362  cdleme7  30363  cdleme9  30367  cdleme11c  30375  cdleme11g  30379  cdleme11k  30382  cdleme11  30384  cdleme12  30385  cdleme15b  30389  cdleme15d  30391  cdleme16d  30395  cdleme16e  30396  cdleme16f  30397  cdleme17b  30401  cdleme18b  30406  cdleme22gb  30408  cdlemednpq  30413  cdleme19a  30417  cdleme20aN  30423  cdleme20bN  30424  cdleme20c  30425  cdleme20d  30426  cdleme20j  30432  cdleme21c  30441  cdleme22aa  30453  cdleme22b  30455  cdleme22cN  30456  cdleme22d  30457  cdleme22e  30458  cdleme22eALTN  30459  cdleme23b  30464  cdleme23c  30465  cdleme28a  30484  cdleme30a  30492  cdlemefs29bpre0N  30530  cdlemefs29bpre1N  30531  cdlemefs29cpre1N  30532  cdlemefs29clN  30533  cdlemefs32fvaN  30536  cdlemefs32fva1  30537  cdleme32b  30556  cdleme32c  30557  cdleme32e  30559  cdleme35a  30562  cdleme35fnpq  30563  cdleme35b  30564  cdleme35f  30568  cdleme36a  30574  cdleme36m  30575  cdleme37m  30576  cdleme39a  30579  cdleme42c  30586  cdleme42i  30597  cdleme42keg  30600  cdleme42mgN  30602  cdleme48bw  30616  cdlemeg46fjgN  30635  cdlemeg46fjv  30637  cdlemeg46req  30643  cdleme50trn1  30663  cdlemf1  30675  cdlemf2  30676  cdlemg1cex  30702  cdlemg2fv2  30714  cdlemg7fvbwN  30721  cdlemg4c  30726  cdlemg4  30731  cdlemg6c  30734  cdlemg8b  30742  cdlemg10c  30753  cdlemg10  30755  cdlemg11b  30756  cdlemg12f  30762  cdlemg13a  30765  cdlemg17a  30775  cdlemg17dALTN  30778  cdlemg18b  30793  cdlemg19a  30797  cdlemg27a  30806  cdlemg27b  30810  cdlemg33b0  30815  cdlemg33a  30820  cdlemg35  30827  trlcolem  30840  cdlemg42  30843  cdlemg46  30849  trljco  30854  tendopltp  30894  cdlemh1  30929  cdlemh2  30930  cdlemi1  30932  cdlemi  30934  cdlemk3  30947  cdlemk10  30957  cdlemk11  30963  cdlemk15  30969  cdlemk1u  30973  cdlemk5u  30975  cdlemk11u  30985  cdlemk39  31030  cdlemkid1  31036  cdlemk50  31066  cdlemk51  31067  erngdvlem3-rN  31112  tendocnv  31136  tendospcanN  31138  dialss  31161  dia2dimlem1  31179  dia2dimlem2  31180  dia2dimlem3  31181  dia2dimlem10  31188  dia2dimlem12  31190  dvhvaddass  31212  dvhlveclem  31223  cdlemm10N  31233  doca2N  31241  djajN  31252  dib1dim2  31283  diblss  31285  diclspsn  31309  cdlemn2  31310  cdlemn10  31321  dihjustlem  31331  dihord1  31333  dihord2a  31334  dihord2pre2  31341  dib2dim  31358  dih2dimb  31359  dih2dimbALTN  31360  dihopelvalcpre  31363  dihord5b  31374  dihord6b  31375  dihord5apre  31377  dihmeetlem1N  31405  dihglblem5apreN  31406  dihglblem2N  31409  dihglbcpreN  31415  dihmeetbclemN  31419  dihmeetlem3N  31420  dihmeetlem6  31424  dih1dimatlem  31444  djhcvat42  31530  dihjatcclem1  31533  dihjatcclem4  31536  dvh4dimat  31553  lcfl7lem  31614  lclkrlem2m  31634  lcfrlem1  31657  lcdvsass  31722  baerlem3lem1  31822  baerlem5alem1  31823  baerlem5blem1  31824  mapdh6gN  31857  mapdh6hN  31858  hdmap1l6g  31932  hdmap1l6h  31933  hdmapneg  31964  hdmap14lem8  31993  hgmapadd  32012  hgmapmul  32013  hgmapvvlem1  32041
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