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  2539  disjxiun  4036  wereu2  4406  ordelord  4430  caovassd  6035  caovcand  6038  caovordid  6042  caovordd  6044  caovdid  6051  caovdird  6054  swoer  6704  swoord1  6705  swoord2  6706  frfi  7118  indexfi  7179  ssfii  7188  elfiun  7199  suplub2  7228  wemaplem2  7278  htalem  7582  cofsmo  7911  alephsing  7918  sornom  7919  axdc3lem4  8095  zorn2lem1  8139  ttukeylem6  8157  ttukeylem7  8158  prlem934  8673  fzosubel3  10926  seqsplit  11095  seqcaopr  11099  ccatass  11452  splid  11484  spllen  11485  splfv1  11486  splfv2a  11487  splval2  11488  wrdeqcats1  11490  wrdeqs1cat  11491  swrds2  11576  isercolllem2  12155  fsumiun  12295  pcgcd1  12945  firest  13353  iscatd2  13599  posasymb  14102  meetle  14150  lattrd  14180  latleeqj1  14185  latjlej1  14187  latjlej12  14189  latnlej2  14193  latjidm  14196  latleeqm1  14201  latmlem1  14203  latmlem12  14205  latmidm  14208  latledi  14211  latjass  14217  latj12  14218  latj13  14220  latj31  14221  latjrot  14222  latj4  14223  mod1ile  14227  lubun  14243  clatleglb  14246  latdisdlem  14308  mnd32g  14392  mnd12g  14393  mnd4g  14394  prdsmndd  14421  imasmnd  14426  gsumspl  14482  grpinvinv  14551  grplmulf1o  14558  grpinvadd  14560  grpsubrcan  14563  grpsubadd  14569  grpaddsubass  14571  grppncan  14572  grpsubsub4  14574  grppnpcan2  14575  grpnpncan  14576  grpnnncan2  14577  grplactcnv  14580  mulgnn0dir  14606  mulgdirlem  14607  mulgneg2  14610  mulgnnass  14611  mulgnn0ass  14612  mulgass  14613  imasgrp  14627  nsgconj  14666  isnsg3  14667  nmzsubg  14674  ssnmz  14675  eqger  14683  eqgcpbl  14687  conjghm  14729  conjnmz  14732  conjnmzb  14733  subgga  14770  gass  14771  gasubg  14772  galcan  14774  gacan  14775  gapm  14776  gaorber  14778  gastacl  14779  gastacos  14780  cntzsubm  14827  cntzsubg  14828  oppgmnd  14843  odmodnn0  14871  mndodconglem  14872  odmod  14877  odcong  14880  odmulgid  14883  odbezout  14887  gexdvdsi  14910  gexdvds  14911  sylow1lem2  14926  sylow1lem4  14928  sylow2blem1  14947  sylow2blem2  14948  sylow2blem3  14949  sylow3lem1  14954  sylow3lem2  14955  lsmass  14995  lsmmod  15000  lsmdisj2  15007  subgdisj1  15016  efgredleme  15068  efgredlemc  15070  efgcpbllemb  15080  frgp0  15085  frgpuplem  15097  abl32  15126  abladdsub4  15131  abladdsub  15132  ablpncan2  15133  ablsubsub  15135  mulgdi  15142  mulgsubdi  15145  odadd1  15156  odadd2  15157  gex2abl  15159  oddvdssubg  15163  cygabl  15193  ablfacrp  15317  pgpfac1lem2  15326  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfac1lem4  15329  rngcom  15385  rnglz  15393  rngrz  15394  rngnegl  15396  rngnegr  15397  rngmneg1  15398  rngmneg2  15399  rngsubdi  15401  rngsubdir  15402  mulgass2  15403  prdsrngd  15411  imasrng  15418  opprrng  15429  mulgass3  15435  dvdsrtr  15450  dvdsrmul1  15451  unitgrp  15465  dvrass  15488  dvrcan1  15489  dvrcan3  15490  irredrmul  15505  drngmul0or  15549  subrginv  15577  cntzsubr  15593  lmod0vs  15679  lmodvs0  15680  lmodvneg1  15683  lmodvsneg  15685  lmodcom  15687  lmodsubvs  15697  lmodsubdi  15698  lmodsubdir  15699  lssvsubcl  15717  lssvacl  15727  lssvscl  15728  islss3  15732  lss1d  15736  lssintcl  15737  prdslmodd  15742  lmodvsinv  15809  lmodvsinv2  15810  lmhmplusg  15817  lmhmvsca  15818  lsmcl  15852  pj1lmhm  15869  lvecvs0or  15877  lssvs0or  15879  lvecinv  15882  lspsnvs  15883  lspfixed  15897  lspexch  15898  lspsolvlem  15911  lspsolv  15912  lssacsex  15913  lspsnat  15914  lsppratlem1  15916  lsppratlem3  15918  lsppratlem4  15919  lbsextlem2  15928  lbsextlem4  15930  sralmod  15955  2idlcpbl  16002  unitrrg  16050  issubassa  16080  sraassa  16081  asclghm  16094  asclmul1  16095  asclmul2  16096  asclrhm  16097  psrbagcon  16133  psrbagconcl  16135  psrbagconf1o  16136  gsumbagdiaglem  16137  psrmulcllem  16148  psrlidm  16164  psrridm  16165  psrass1  16166  psrdi  16167  psrdir  16168  psrcom  16169  psrass23  16170  mplmon2mul  16258  coe1subfv  16359  mulgrhm  16476  cygznlem3  16539  ipdi  16560  ip2di  16561  ipsubdir  16562  ipsubdi  16563  ip2subdi  16564  ipassr  16566  ipassr2  16567  ip2eq  16573  ocvlss  16588  lsmcss  16608  iinopn  16664  subbascn  17000  cnhaus  17098  nrmsep2  17100  nrmsep  17101  regsep2  17120  isreg2  17121  hauscmplem  17149  1stcfb  17187  2ndcctbss  17197  ptbasfi  17292  pthaus  17348  txtube  17350  txhaus  17357  xkohaus  17363  kqnrmlem1  17450  kqnrmlem2  17451  nrmr0reg  17456  nrmhmph  17501  fbssint  17549  infil  17574  fgabs  17590  filcon  17594  filuni  17596  trfil2  17598  trfg  17602  ufprim  17620  elfm3  17661  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  hausflimi  17691  hauspwpwf1  17698  fclsneii  17728  supnfcls  17731  flimfnfcls  17739  fclscmpi  17740  alexsublem  17754  ghmcnp  17813  divstgpopn  17818  xmetge0  17925  xmetsym  17928  xmettri  17931  xmetres2  17941  prdsxmetlem  17948  prdsmet  17950  imasdsf1olem  17953  imasf1oxmet  17955  bldisj  17971  xblss2  17974  xmeter  17995  prdsbl  18053  nrmmetd  18113  ngpsubcan  18151  nmmtri  18159  nmrtri  18161  ngptgp  18168  nlmvscnlem2  18212  nrginvrcnlem  18217  metdcnlem  18357  clmmulg  18607  cphabscl  18637  cphsqrcl2  18638  cphsqrcl3  18639  cphnmf  18647  cph2ass  18664  ipcau2  18680  tchcphlem2  18682  ipcnlem2  18687  cfilfcls  18716  iscau3  18720  iscmet3lem2  18734  iscmet3  18735  relcmpcmet  18758  minveclem2  18806  minveclem4  18812  pjthlem1  18817  pjthlem2  18818  uniioombllem4  18957  dyadmax  18969  itg1addlem4  19070  itg1climres  19085  evlslem1  19415  ply1divex  19538  aalioulem2  19729  amgmlem  20300  dvdsppwf1o  20442  perfect1  20483  perfectlem1  20484  perfectlem2  20485  dchrptlem2  20520  grpoidinvlem4  20890  grpoasscan2  20921  grpoinvop  20924  grpopncan  20934  grponpcan  20935  grpopnpcan2  20936  grpodiveq  20939  gxcom  20952  gxnn0add  20957  ghgrp  21051  rngo2  21071  rngolz  21084  rngorz  21085  vcm  21143  nvmul0or  21226  nvpncan2  21230  nvnncan  21237  nvdif  21247  nvabs  21255  smcnlem  21286  lnomul  21354  minvecolem2  21470  superpos  22950  ballotlemiex  23076  ssnnssfz  23292  lmxrge0  23390  cvmopnlem  23824  cvmliftmolem2  23828  cvmliftlem6  23836  cvmliftlem8  23838  cvmliftlem9  23839  cvmlift2lem9  23857  cvmlift3lem2  23866  cvmlift3lem6  23870  cvmlift3lem7  23871  cvmlift3lem9  23873  eupa0  23913  eupares  23914  eupap1  23915  zprod  24160  nodense  24414  axcontlem9  24672  cgrtriv  24697  cgrdegen  24699  cgrextend  24703  segconeq  24705  btwntriv2  24707  btwncomand  24710  btwntriv1  24711  btwnintr  24714  btwnexch3  24715  btwnouttr  24719  btwnexch  24720  trisegint  24723  ifscgr  24739  btwnxfr  24751  colineartriv1  24762  colineartriv2  24763  colinearxfr  24770  fscgr  24775  lineid  24778  idinside  24779  endofsegidand  24781  btwnconn1lem5  24786  btwnconn1lem7  24788  btwnconn1lem11  24792  btwnconn1lem12  24793  btwnconn1lem13  24794  brsegle2  24804  segleantisym  24810  broutsideof2  24817  btwnoutside  24820  outsideoftr  24824  outsideofeq  24825  outsideofeu  24826  outsidele  24827  lineunray  24842  lineelsb2  24843  linecom  24845  linethru  24848  resgcom  25454  fprodsub  25482  trran2  25496  cmprtr  25499  ltrran2  25506  ltrinvlem  25509  cmprltr  25513  rltrran  25517  rltrooo  25518  multinv  25525  multinvb  25526  zerdivemp1  25539  mvecrtol  25576  mvecrtol2  25580  mulveczer  25582  mulinvsca  25583  muldisc  25584  glmrngo  25585  cmptdst2  25674  flfnei2  25680  addcanrg  25770  negveud  25771  negveudr  25772  issubrv  25775  neibastop1  26411  syl3an2cOLDOLD  26438  mettrifi  26576  isbnd3  26611  heibor1lem  26636  bfplem2  26650  ghomdiv  26677  zerdivemp1x  26689  irrapxlem5  27014  aomclem2  27255  frlmup1  27353  isnumbasgrplem2  27372  mpaaeu  27458  symggen  27514  mamuass  27563  mamudi  27564  mamudir  27565  mamuvs1  27566  mamuvs2  27567  mendrng  27603  mendlmod  27604  caofcan  27643  4cycl4dv4e  28414  lubunNEW  29785  lfladdcl  29883  lflvscl  29889  eqlkr3  29913  lkrlsp  29914  lshpkrlem4  29925  oldmm1  30029  olj01  30037  latmassOLD  30041  latm32  30043  latmrot  30044  latm4  30045  olm01  30048  cmtcomlemN  30060  cmtbr3N  30066  cmtbr4N  30067  lecmtN  30068  omlfh1N  30070  atlen0  30122  atnle  30129  atlatmstc  30131  atlatle  30132  cvlexchb1  30142  cvlcvr1  30151  ishlat3N  30166  hlatjass  30181  hlatj12  30182  hlatj32  30183  hlsupr2  30198  hlhgt2  30200  hl0lt1N  30201  hlrelat  30213  hlrelat2  30214  exatleN  30215  hlrelat3  30223  cvrval5  30226  cvrexchlem  30230  cvratlem  30232  cvrat  30233  atcvr0eq  30237  lnnat  30238  atlt  30248  atlelt  30249  2atlt  30250  atexchltN  30252  cvrat3  30253  2atjm  30256  atbtwn  30257  4noncolr3  30264  athgt  30267  3dimlem3a  30271  3dimlem3OLDN  30273  3dimlem4a  30274  3dimlem4OLDN  30276  3dim1  30278  3dim2  30279  1cvratex  30284  ps-1  30288  ps-2  30289  hlatexch3N  30291  hlatexch4  30292  ps-2b  30293  3atlem1  30294  3atlem2  30295  3atlem5  30298  3atlem6  30299  llnnleat  30324  llncmp  30333  2at0mat0  30336  2atmat0  30337  2atm  30338  lplni2  30348  lvolex3N  30349  lplnnle2at  30352  lplnnleat  30353  lplnnlelln  30354  2atnelpln  30355  llncvrlpln  30369  2atmat  30372  lplncmp  30373  lplnexllnN  30375  2llnjaN  30377  2llnm4  30381  2llnmeqat  30382  lvolnle3at  30393  lvolnleat  30394  2atnelvolN  30398  islvol2aN  30403  4atlem3  30407  4atlem3a  30408  4atlem3b  30409  4atlem4a  30410  4atlem4b  30411  4atlem4c  30412  4atlem4d  30413  4atlem10  30417  4atlem11b  30419  4atlem11  30420  4atlem12b  30422  4atlem12  30423  4at2  30425  lplncvrlvol  30427  lvolcmp  30428  2lplnja  30430  dalemqrprot  30459  dalemply  30465  dalemsly  30466  dalemrot  30468  dalemrotyz  30469  dalem1  30470  dalemcea  30471  dalem3  30475  dalem5  30478  dalem8  30481  dalem-cly  30482  dalem11  30485  dalem12  30486  dalem16  30490  dalem17  30491  dalem18  30492  dalem21  30505  dalem24  30508  dalem25  30509  dalem38  30521  dalem39  30522  dalem44  30527  dalem54  30537  dalem55  30538  dalem57  30540  dalem58  30541  dalem59  30542  dalem60  30543  dath2  30548  2atm2atN  30596  2llnma1b  30597  2llnma3r  30599  cdlema1N  30602  cdlemblem  30604  paddasslem5  30635  paddasslem10  30640  paddasslem12  30642  paddasslem13  30643  paddass  30649  padd12N  30650  padd4N  30651  paddss  30656  pmodlem1  30657  pmodl42N  30662  pmapjoin  30663  pmapjlln1  30666  atmod1i2  30670  llnmod1i2  30671  llnexchb2  30680  dalawlem2  30683  dalawlem3  30684  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem11  30692  dalawlem12  30693  dalawlem13  30694  pclunN  30709  osumcllem1N  30767  pexmidlem3N  30783  lhp2lt  30812  lhp0lt  30814  lhpexle2lem  30820  lhpexle3lem  30822  lhpocnle  30827  lhpj1  30833  lhpmcvr4N  30837  lhp2at0  30843  lhpat3  30857  4atexlemtlw  30878  4atexlemc  30880  4atexlemnclw  30881  4atexlemcnd  30883  lautcvr  30903  lautj  30904  lautm  30905  ltrnm  30942  ltrnj  30943  ltrncvr  30944  trlval3  30998  cdlemc5  31006  cdlemd2  31010  cdlemd3  31011  cdleme0e  31028  cdleme1  31038  cdleme3c  31041  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme5  31051  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme9  31064  cdleme11c  31072  cdleme11g  31076  cdleme11k  31079  cdleme11  31081  cdleme12  31082  cdleme15b  31086  cdleme15d  31088  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme17b  31098  cdleme18b  31103  cdleme22gb  31105  cdlemednpq  31110  cdleme19a  31114  cdleme20aN  31120  cdleme20bN  31121  cdleme20c  31122  cdleme20d  31123  cdleme20j  31129  cdleme21c  31138  cdleme22aa  31150  cdleme22b  31152  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme23b  31161  cdleme23c  31162  cdleme28a  31181  cdleme30a  31189  cdlemefs29bpre0N  31227  cdlemefs29bpre1N  31228  cdlemefs29cpre1N  31229  cdlemefs29clN  31230  cdlemefs32fvaN  31233  cdlemefs32fva1  31234  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35a  31259  cdleme35fnpq  31260  cdleme35b  31261  cdleme35f  31265  cdleme36a  31271  cdleme36m  31272  cdleme37m  31273  cdleme39a  31276  cdleme42c  31283  cdleme42i  31294  cdleme42keg  31297  cdleme42mgN  31299  cdleme48bw  31313  cdlemeg46fjgN  31332  cdlemeg46fjv  31334  cdlemeg46req  31340  cdleme50trn1  31360  cdlemf1  31372  cdlemf2  31373  cdlemg1cex  31399  cdlemg2fv2  31411  cdlemg7fvbwN  31418  cdlemg4c  31423  cdlemg4  31428  cdlemg6c  31431  cdlemg8b  31439  cdlemg10c  31450  cdlemg10  31452  cdlemg11b  31453  cdlemg12f  31459  cdlemg13a  31462  cdlemg17a  31472  cdlemg17dALTN  31475  cdlemg18b  31490  cdlemg19a  31494  cdlemg27a  31503  cdlemg27b  31507  cdlemg33b0  31512  cdlemg33a  31517  cdlemg35  31524  trlcolem  31537  cdlemg42  31540  cdlemg46  31546  trljco  31551  tendopltp  31591  cdlemh1  31626  cdlemh2  31627  cdlemi1  31629  cdlemi  31631  cdlemk3  31644  cdlemk10  31654  cdlemk11  31660  cdlemk15  31666  cdlemk1u  31670  cdlemk5u  31672  cdlemk11u  31682  cdlemk39  31727  cdlemkid1  31733  cdlemk50  31763  cdlemk51  31764  erngdvlem3-rN  31809  tendocnv  31833  tendospcanN  31835  dialss  31858  dia2dimlem1  31876  dia2dimlem2  31877  dia2dimlem3  31878  dia2dimlem10  31885  dia2dimlem12  31887  dvhvaddass  31909  dvhlveclem  31920  cdlemm10N  31930  doca2N  31938  djajN  31949  dib1dim2  31980  diblss  31982  diclspsn  32006  cdlemn2  32007  cdlemn10  32018  dihjustlem  32028  dihord1  32030  dihord2a  32031  dihord2pre2  32038  dib2dim  32055  dih2dimb  32056  dih2dimbALTN  32057  dihopelvalcpre  32060  dihord5b  32071  dihord6b  32072  dihord5apre  32074  dihmeetlem1N  32102  dihglblem5apreN  32103  dihglblem2N  32106  dihglbcpreN  32112  dihmeetbclemN  32116  dihmeetlem3N  32117  dihmeetlem6  32121  dih1dimatlem  32141  djhcvat42  32227  dihjatcclem1  32230  dihjatcclem4  32233  dvh4dimat  32250  lcfl7lem  32311  lclkrlem2m  32331  lcfrlem1  32354  lcdvsass  32419  baerlem3lem1  32519  baerlem5alem1  32520  baerlem5blem1  32521  mapdh6gN  32554  mapdh6hN  32555  hdmap1l6g  32629  hdmap1l6h  32630  hdmapneg  32661  hdmap14lem8  32690  hgmapadd  32709  hgmapmul  32710  hgmapvvlem1  32738
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