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  2526  disjxiun  4020  wereu2  4390  ordelord  4414  caovassd  6019  caovcand  6022  caovordid  6026  caovordd  6028  caovdid  6035  caovdird  6038  swoer  6688  swoord1  6689  swoord2  6690  frfi  7102  indexfi  7163  ssfii  7172  elfiun  7183  suplub2  7212  wemaplem2  7262  htalem  7566  cofsmo  7895  alephsing  7902  sornom  7903  axdc3lem4  8079  zorn2lem1  8123  ttukeylem6  8141  ttukeylem7  8142  prlem934  8657  fzosubel3  10910  seqsplit  11079  seqcaopr  11083  ccatass  11436  splid  11468  spllen  11469  splfv1  11470  splfv2a  11471  splval2  11472  wrdeqcats1  11474  wrdeqs1cat  11475  swrds2  11560  isercolllem2  12139  fsumiun  12279  pcgcd1  12929  firest  13337  iscatd2  13583  posasymb  14086  meetle  14134  lattrd  14164  latleeqj1  14169  latjlej1  14171  latjlej12  14173  latnlej2  14177  latjidm  14180  latleeqm1  14185  latmlem1  14187  latmlem12  14189  latmidm  14192  latledi  14195  latjass  14201  latj12  14202  latj13  14204  latj31  14205  latjrot  14206  latj4  14207  mod1ile  14211  lubun  14227  clatleglb  14230  latdisdlem  14292  mnd32g  14376  mnd12g  14377  mnd4g  14378  prdsmndd  14405  imasmnd  14410  gsumspl  14466  grpinvinv  14535  grplmulf1o  14542  grpinvadd  14544  grpsubrcan  14547  grpsubadd  14553  grpaddsubass  14555  grppncan  14556  grpsubsub4  14558  grppnpcan2  14559  grpnpncan  14560  grpnnncan2  14561  grplactcnv  14564  mulgnn0dir  14590  mulgdirlem  14591  mulgneg2  14594  mulgnnass  14595  mulgnn0ass  14596  mulgass  14597  imasgrp  14611  nsgconj  14650  isnsg3  14651  nmzsubg  14658  ssnmz  14659  eqger  14667  eqgcpbl  14671  conjghm  14713  conjnmz  14716  conjnmzb  14717  subgga  14754  gass  14755  gasubg  14756  galcan  14758  gacan  14759  gapm  14760  gaorber  14762  gastacl  14763  gastacos  14764  cntzsubm  14811  cntzsubg  14812  oppgmnd  14827  odmodnn0  14855  mndodconglem  14856  odmod  14861  odcong  14864  odmulgid  14867  odbezout  14871  gexdvdsi  14894  gexdvds  14895  sylow1lem2  14910  sylow1lem4  14912  sylow2blem1  14931  sylow2blem2  14932  sylow2blem3  14933  sylow3lem1  14938  sylow3lem2  14939  lsmass  14979  lsmmod  14984  lsmdisj2  14991  subgdisj1  15000  efgredleme  15052  efgredlemc  15054  efgcpbllemb  15064  frgp0  15069  frgpuplem  15081  abl32  15110  abladdsub4  15115  abladdsub  15116  ablpncan2  15117  ablsubsub  15119  mulgdi  15126  mulgsubdi  15129  odadd1  15140  odadd2  15141  gex2abl  15143  oddvdssubg  15147  cygabl  15177  ablfacrp  15301  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem4  15313  rngcom  15369  rnglz  15377  rngrz  15378  rngnegl  15380  rngnegr  15381  rngmneg1  15382  rngmneg2  15383  rngsubdi  15385  rngsubdir  15386  mulgass2  15387  prdsrngd  15395  imasrng  15402  opprrng  15413  mulgass3  15419  dvdsrtr  15434  dvdsrmul1  15435  unitgrp  15449  dvrass  15472  dvrcan1  15473  dvrcan3  15474  irredrmul  15489  drngmul0or  15533  subrginv  15561  cntzsubr  15577  lmod0vs  15663  lmodvs0  15664  lmodvneg1  15667  lmodvsneg  15669  lmodcom  15671  lmodsubvs  15681  lmodsubdi  15682  lmodsubdir  15683  lssvsubcl  15701  lssvacl  15711  lssvscl  15712  islss3  15716  lss1d  15720  lssintcl  15721  prdslmodd  15726  lmodvsinv  15793  lmodvsinv2  15794  lmhmplusg  15801  lmhmvsca  15802  lsmcl  15836  pj1lmhm  15853  lvecvs0or  15861  lssvs0or  15863  lvecinv  15866  lspsnvs  15867  lspfixed  15881  lspexch  15882  lspsolvlem  15895  lspsolv  15896  lssacsex  15897  lspsnat  15898  lsppratlem1  15900  lsppratlem3  15902  lsppratlem4  15903  lbsextlem2  15912  lbsextlem4  15914  sralmod  15939  2idlcpbl  15986  unitrrg  16034  issubassa  16064  sraassa  16065  asclghm  16078  asclmul1  16079  asclmul2  16080  asclrhm  16081  psrbagcon  16117  psrbagconcl  16119  psrbagconf1o  16120  gsumbagdiaglem  16121  psrmulcllem  16132  psrlidm  16148  psrridm  16149  psrass1  16150  psrdi  16151  psrdir  16152  psrcom  16153  psrass23  16154  mplmon2mul  16242  coe1subfv  16343  mulgrhm  16460  cygznlem3  16523  ipdi  16544  ip2di  16545  ipsubdir  16546  ipsubdi  16547  ip2subdi  16548  ipassr  16550  ipassr2  16551  ip2eq  16557  ocvlss  16572  lsmcss  16592  iinopn  16648  subbascn  16984  cnhaus  17082  nrmsep2  17084  nrmsep  17085  regsep2  17104  isreg2  17105  hauscmplem  17133  1stcfb  17171  2ndcctbss  17181  ptbasfi  17276  pthaus  17332  txtube  17334  txhaus  17341  xkohaus  17347  kqnrmlem1  17434  kqnrmlem2  17435  nrmr0reg  17440  nrmhmph  17485  fbssint  17533  infil  17558  fgabs  17574  filcon  17578  filuni  17580  trfil2  17582  trfg  17586  ufprim  17604  elfm3  17645  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  hausflimi  17675  hauspwpwf1  17682  fclsneii  17712  supnfcls  17715  flimfnfcls  17723  fclscmpi  17724  alexsublem  17738  ghmcnp  17797  divstgpopn  17802  xmetge0  17909  xmetsym  17912  xmettri  17915  xmetres2  17925  prdsxmetlem  17932  prdsmet  17934  imasdsf1olem  17937  imasf1oxmet  17939  bldisj  17955  xblss2  17958  xmeter  17979  prdsbl  18037  nrmmetd  18097  ngpsubcan  18135  nmmtri  18143  nmrtri  18145  ngptgp  18152  nlmvscnlem2  18196  nrginvrcnlem  18201  metdcnlem  18341  clmmulg  18591  cphabscl  18621  cphsqrcl2  18622  cphsqrcl3  18623  cphnmf  18631  cph2ass  18648  ipcau2  18664  tchcphlem2  18666  ipcnlem2  18671  cfilfcls  18700  iscau3  18704  iscmet3lem2  18718  iscmet3  18719  relcmpcmet  18742  minveclem2  18790  minveclem4  18796  pjthlem1  18801  pjthlem2  18802  uniioombllem4  18941  dyadmax  18953  itg1addlem4  19054  itg1climres  19069  evlslem1  19399  ply1divex  19522  aalioulem2  19713  amgmlem  20284  dvdsppwf1o  20426  perfect1  20467  perfectlem1  20468  perfectlem2  20469  dchrptlem2  20504  grpoidinvlem4  20874  grpoasscan2  20905  grpoinvop  20908  grpopncan  20918  grponpcan  20919  grpopnpcan2  20920  grpodiveq  20923  gxcom  20936  gxnn0add  20941  ghgrp  21035  rngo2  21055  rngolz  21068  rngorz  21069  vcm  21127  nvmul0or  21210  nvpncan2  21214  nvnncan  21221  nvdif  21231  nvabs  21239  smcnlem  21270  lnomul  21338  minvecolem2  21454  superpos  22934  ballotlemiex  23060  ssnnssfz  23277  lmxrge0  23375  cvmopnlem  23809  cvmliftmolem2  23813  cvmliftlem6  23821  cvmliftlem8  23823  cvmliftlem9  23824  cvmlift2lem9  23842  cvmlift3lem2  23851  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  eupa0  23898  eupares  23899  eupap1  23900  nodense  24343  axcontlem9  24600  cgrtriv  24625  cgrdegen  24627  cgrextend  24631  segconeq  24633  btwntriv2  24635  btwncomand  24638  btwntriv1  24639  btwnintr  24642  btwnexch3  24643  btwnouttr  24647  btwnexch  24648  trisegint  24651  ifscgr  24667  btwnxfr  24679  colineartriv1  24690  colineartriv2  24691  colinearxfr  24698  fscgr  24703  lineid  24706  idinside  24707  endofsegidand  24709  btwnconn1lem5  24714  btwnconn1lem7  24716  btwnconn1lem11  24720  btwnconn1lem12  24721  btwnconn1lem13  24722  brsegle2  24732  segleantisym  24738  broutsideof2  24745  btwnoutside  24748  outsideoftr  24752  outsideofeq  24753  outsideofeu  24754  outsidele  24755  lineunray  24770  lineelsb2  24771  linecom  24773  linethru  24776  resgcom  25351  fprodsub  25379  trran2  25393  cmprtr  25396  ltrran2  25403  ltrinvlem  25406  cmprltr  25410  rltrran  25414  rltrooo  25415  multinv  25422  multinvb  25423  zerdivemp1  25436  mvecrtol  25473  mvecrtol2  25477  mulveczer  25479  mulinvsca  25480  muldisc  25481  glmrngo  25482  cmptdst2  25571  flfnei2  25577  addcanrg  25667  negveud  25668  negveudr  25669  issubrv  25672  neibastop1  26308  syl3an2cOLDOLD  26335  mettrifi  26473  isbnd3  26508  heibor1lem  26533  bfplem2  26547  ghomdiv  26574  zerdivemp1x  26586  irrapxlem5  26911  aomclem2  27152  frlmup1  27250  isnumbasgrplem2  27269  mpaaeu  27355  symggen  27411  mamuass  27460  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  mendrng  27500  mendlmod  27501  caofcan  27540  lubunNEW  29163  lfladdcl  29261  lflvscl  29267  eqlkr3  29291  lkrlsp  29292  lshpkrlem4  29303  oldmm1  29407  olj01  29415  latmassOLD  29419  latm32  29421  latmrot  29422  latm4  29423  olm01  29426  cmtcomlemN  29438  cmtbr3N  29444  cmtbr4N  29445  lecmtN  29446  omlfh1N  29448  atlen0  29500  atnle  29507  atlatmstc  29509  atlatle  29510  cvlexchb1  29520  cvlcvr1  29529  ishlat3N  29544  hlatjass  29559  hlatj12  29560  hlatj32  29561  hlsupr2  29576  hlhgt2  29578  hl0lt1N  29579  hlrelat  29591  hlrelat2  29592  exatleN  29593  hlrelat3  29601  cvrval5  29604  cvrexchlem  29608  cvratlem  29610  cvrat  29611  atcvr0eq  29615  lnnat  29616  atlt  29626  atlelt  29627  2atlt  29628  atexchltN  29630  cvrat3  29631  2atjm  29634  atbtwn  29635  4noncolr3  29642  athgt  29645  3dimlem3a  29649  3dimlem3OLDN  29651  3dimlem4a  29652  3dimlem4OLDN  29654  3dim1  29656  3dim2  29657  1cvratex  29662  ps-1  29666  ps-2  29667  hlatexch3N  29669  hlatexch4  29670  ps-2b  29671  3atlem1  29672  3atlem2  29673  3atlem5  29676  3atlem6  29677  llnnleat  29702  llncmp  29711  2at0mat0  29714  2atmat0  29715  2atm  29716  lplni2  29726  lvolex3N  29727  lplnnle2at  29730  lplnnleat  29731  lplnnlelln  29732  2atnelpln  29733  llncvrlpln  29747  2atmat  29750  lplncmp  29751  lplnexllnN  29753  2llnjaN  29755  2llnm4  29759  2llnmeqat  29760  lvolnle3at  29771  lvolnleat  29772  2atnelvolN  29776  islvol2aN  29781  4atlem3  29785  4atlem3a  29786  4atlem3b  29787  4atlem4a  29788  4atlem4b  29789  4atlem4c  29790  4atlem4d  29791  4atlem10  29795  4atlem11b  29797  4atlem11  29798  4atlem12b  29800  4atlem12  29801  4at2  29803  lplncvrlvol  29805  lvolcmp  29806  2lplnja  29808  dalemqrprot  29837  dalemply  29843  dalemsly  29844  dalemrot  29846  dalemrotyz  29847  dalem1  29848  dalemcea  29849  dalem3  29853  dalem5  29856  dalem8  29859  dalem-cly  29860  dalem11  29863  dalem12  29864  dalem16  29868  dalem17  29869  dalem18  29870  dalem21  29883  dalem24  29886  dalem25  29887  dalem38  29899  dalem39  29900  dalem44  29905  dalem54  29915  dalem55  29916  dalem57  29918  dalem58  29919  dalem59  29920  dalem60  29921  dath2  29926  2atm2atN  29974  2llnma1b  29975  2llnma3r  29977  cdlema1N  29980  cdlemblem  29982  paddasslem5  30013  paddasslem10  30018  paddasslem12  30020  paddasslem13  30021  paddass  30027  padd12N  30028  padd4N  30029  paddss  30034  pmodlem1  30035  pmodl42N  30040  pmapjoin  30041  pmapjlln1  30044  atmod1i2  30048  llnmod1i2  30049  llnexchb2  30058  dalawlem2  30061  dalawlem3  30062  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem8  30067  dalawlem11  30070  dalawlem12  30071  dalawlem13  30072  pclunN  30087  osumcllem1N  30145  pexmidlem3N  30161  lhp2lt  30190  lhp0lt  30192  lhpexle2lem  30198  lhpexle3lem  30200  lhpocnle  30205  lhpj1  30211  lhpmcvr4N  30215  lhp2at0  30221  lhpat3  30235  4atexlemtlw  30256  4atexlemc  30258  4atexlemnclw  30259  4atexlemcnd  30261  lautcvr  30281  lautj  30282  lautm  30283  ltrnm  30320  ltrnj  30321  ltrncvr  30322  trlval3  30376  cdlemc5  30384  cdlemd2  30388  cdlemd3  30389  cdleme0e  30406  cdleme1  30416  cdleme3c  30419  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme5  30429  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme9  30442  cdleme11c  30450  cdleme11g  30454  cdleme11k  30457  cdleme11  30459  cdleme12  30460  cdleme15b  30464  cdleme15d  30466  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme17b  30476  cdleme18b  30481  cdleme22gb  30483  cdlemednpq  30488  cdleme19a  30492  cdleme20aN  30498  cdleme20bN  30499  cdleme20c  30500  cdleme20d  30501  cdleme20j  30507  cdleme21c  30516  cdleme22aa  30528  cdleme22b  30530  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme23b  30539  cdleme23c  30540  cdleme28a  30559  cdleme30a  30567  cdlemefs29bpre0N  30605  cdlemefs29bpre1N  30606  cdlemefs29cpre1N  30607  cdlemefs29clN  30608  cdlemefs32fvaN  30611  cdlemefs32fva1  30612  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35a  30637  cdleme35fnpq  30638  cdleme35b  30639  cdleme35f  30643  cdleme36a  30649  cdleme36m  30650  cdleme37m  30651  cdleme39a  30654  cdleme42c  30661  cdleme42i  30672  cdleme42keg  30675  cdleme42mgN  30677  cdleme48bw  30691  cdlemeg46fjgN  30710  cdlemeg46fjv  30712  cdlemeg46req  30718  cdleme50trn1  30738  cdlemf1  30750  cdlemf2  30751  cdlemg1cex  30777  cdlemg2fv2  30789  cdlemg7fvbwN  30796  cdlemg4c  30801  cdlemg4  30806  cdlemg6c  30809  cdlemg8b  30817  cdlemg10c  30828  cdlemg10  30830  cdlemg11b  30831  cdlemg12f  30837  cdlemg13a  30840  cdlemg17a  30850  cdlemg17dALTN  30853  cdlemg18b  30868  cdlemg19a  30872  cdlemg27a  30881  cdlemg27b  30885  cdlemg33b0  30890  cdlemg33a  30895  cdlemg35  30902  trlcolem  30915  cdlemg42  30918  cdlemg46  30924  trljco  30929  tendopltp  30969  cdlemh1  31004  cdlemh2  31005  cdlemi1  31007  cdlemi  31009  cdlemk3  31022  cdlemk10  31032  cdlemk11  31038  cdlemk15  31044  cdlemk1u  31048  cdlemk5u  31050  cdlemk11u  31060  cdlemk39  31105  cdlemkid1  31111  cdlemk50  31141  cdlemk51  31142  erngdvlem3-rN  31187  tendocnv  31211  tendospcanN  31213  dialss  31236  dia2dimlem1  31254  dia2dimlem2  31255  dia2dimlem3  31256  dia2dimlem10  31263  dia2dimlem12  31265  dvhvaddass  31287  dvhlveclem  31298  cdlemm10N  31308  doca2N  31316  djajN  31327  dib1dim2  31358  diblss  31360  diclspsn  31384  cdlemn2  31385  cdlemn10  31396  dihjustlem  31406  dihord1  31408  dihord2a  31409  dihord2pre2  31416  dib2dim  31433  dih2dimb  31434  dih2dimbALTN  31435  dihopelvalcpre  31438  dihord5b  31449  dihord6b  31450  dihord5apre  31452  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem2N  31484  dihglbcpreN  31490  dihmeetbclemN  31494  dihmeetlem3N  31495  dihmeetlem6  31499  dih1dimatlem  31519  djhcvat42  31605  dihjatcclem1  31608  dihjatcclem4  31611  dvh4dimat  31628  lcfl7lem  31689  lclkrlem2m  31709  lcfrlem1  31732  lcdvsass  31797  baerlem3lem1  31897  baerlem5alem1  31898  baerlem5blem1  31899  mapdh6gN  31932  mapdh6hN  31933  hdmap1l6g  32007  hdmap1l6h  32008  hdmapneg  32039  hdmap14lem8  32068  hgmapadd  32087  hgmapmul  32088  hgmapvvlem1  32116
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