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

Theorem syl13anc 1228
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 1174 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 659 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973
This theorem is referenced by:  syl23anc  1233  syl33anc  1241  pm2.61da3neOLD  2775  disjxiun  4436  wereu2  4865  ordelord  4889  caovassd  6447  caovcand  6450  caovordid  6454  caovordd  6456  caovdid  6463  caovdird  6466  swoer  7331  swoord1  7332  swoord2  7333  frfi  7757  indexfi  7820  ssfii  7871  elfiun  7882  suplub2  7912  supgtoreq  7920  wemaplem2  7964  htalem  8305  cofsmo  8640  alephsing  8647  sornom  8648  axdc3lem4  8824  zorn2lem1  8867  ttukeylem6  8885  ttukeylem7  8886  prlem934  9400  supfirege  10520  suprfinzcl  10975  fzosubel3  11858  fsuppmapnn0fiublem  12078  seqsplit  12122  seqcaopr  12126  ccatass  12594  wrdcctswrd  12681  wrdeqcats1OLD  12690  wrdeqs1cat  12691  splid  12720  spllen  12721  splfv1  12722  splfv2a  12723  splval2  12724  swrds2  12874  isercolllem2  13570  fsumiun  13717  zprod  13826  pcgcd1  14484  cshwsidrepswmod0  14663  cshwshashlem2  14665  cshwsdisj  14667  firest  14922  iscatd2  15170  posasymb  15781  joinle  15843  meetle  15857  lattrd  15887  latleeqj1  15892  latjlej1  15894  latjlej12  15896  latnlej2  15900  latjidm  15903  latleeqm1  15908  latmlem1  15910  latmlem12  15912  latmidm  15915  latledi  15918  latjass  15924  latj12  15925  latj13  15927  latj31  15928  latjrot  15929  latj4  15930  mod1ile  15934  lubun  15952  clatleglb  15955  latdisdlem  16018  mnd32g  16134  mnd12g  16135  mnd4g  16136  ismndd  16142  prdsmndd  16152  imasmnd  16157  mrcmndind  16196  gsumspl  16211  grpidrcan  16302  grpidlcan  16303  grpinvinv  16304  grplmulf1o  16311  grpinvssd  16314  grpinvadd  16315  grpsubrcan  16318  grpsubadd  16325  grpaddsubass  16327  grppncan  16328  grpsubsub4  16330  grppnpcan2  16331  grpnpncan  16332  grpnpncan0  16333  grpnnncan2  16334  grplactcnv  16337  mulgnn0dir  16364  mulgdirlem  16365  mulgneg2  16368  mulgnnass  16369  mulgnn0ass  16370  mulgass  16371  imasgrp  16385  mhmmnd  16391  nsgconj  16433  isnsg3  16434  nmzsubg  16441  ssnmz  16442  eqger  16450  eqgcpbl  16454  conjghm  16496  conjnmz  16499  conjnmzb  16500  subgga  16537  gass  16538  gasubg  16539  galcan  16541  gacan  16542  gapm  16543  gaorber  16545  gastacl  16546  gastacos  16547  cntzsubm  16572  cntzsubg  16573  oppgmnd  16588  symggen  16694  odmodnn0  16763  mndodconglem  16764  odmod  16769  odcong  16772  odmulgid  16775  odbezout  16779  gexdvdsi  16802  gexdvds  16803  sylow1lem2  16818  sylow1lem4  16820  sylow2blem1  16839  sylow2blem2  16840  sylow2blem3  16841  sylow3lem1  16846  sylow3lem2  16847  lsmass  16887  lsmmod  16892  lsmdisj2  16899  subgdisj1  16908  efgredleme  16960  efgredlemc  16962  efgcpbllemb  16972  frgp0  16977  frgpuplem  16989  abl32  17018  abladdsub4  17023  abladdsub  17024  ablpncan2  17025  ablsubsub  17027  mulgdi  17034  mulgsubdi  17037  odadd1  17053  odadd2  17054  gex2abl  17056  oddvdssubg  17060  cygabl  17092  telgsumfzslem  17212  ablfacrp  17312  pgpfac1lem2  17321  pgpfac1lem3a  17322  pgpfac1lem3  17323  pgpfac1lem4  17324  srgmulgass  17377  srgpcomp  17378  srgpcompp  17379  srgpcomppsc  17380  srgbinomlem3  17388  srgbinomlem4  17389  srgbinomlem  17390  csrgbinom  17392  ringcom  17422  ringlz  17430  ringrz  17431  ringnegl  17435  rngnegr  17436  ringmneg1  17437  ringmneg2  17438  ringsubdi  17440  rngsubdir  17441  mulgass2  17442  prdsringd  17456  imasring  17463  opprring  17475  mulgass3  17481  dvdsrtr  17496  dvdsrmul1  17497  unitgrp  17511  dvrass  17534  dvrcan1  17535  dvrcan3  17536  irredrmul  17551  drngmul0or  17612  subrginv  17640  cntzsubr  17656  lmod0vs  17740  lmodvs0  17741  lmodvsmmulgdi  17742  lmodvneg1  17748  lmodvsneg  17749  lmodcom  17751  lmodsubvs  17761  lmodsubdi  17762  lmodsubdir  17763  lssvsubcl  17785  lssvacl  17795  lssvscl  17796  islss3  17800  lss1d  17804  lssintcl  17805  prdslmodd  17810  lmodvsinv  17877  lmodvsinv2  17878  lmhmplusg  17885  lmhmvsca  17886  lsmcl  17924  pj1lmhm  17941  lvecvs0or  17949  lssvs0or  17951  lvecinv  17954  lspsnvs  17955  lspfixed  17969  lspexch  17970  lspsolvlem  17983  lspsolv  17984  lssacsex  17985  lspsnat  17986  lsppratlem1  17988  lsppratlem3  17990  lsppratlem4  17991  lbsextlem2  18000  lbsextlem4  18002  sralmod  18028  2idlcpbl  18077  unitrrg  18137  assa2ass  18166  issubassa  18168  sraassa  18169  asclghm  18182  asclmul1  18183  asclmul2  18184  asclrhm  18186  assamulgscmlem2  18193  psrbagcon  18217  psrbagconcl  18220  psrbagconf1o  18221  gsumbagdiaglem  18222  psrmulcllem  18235  psrlidm  18251  psrlidmOLD  18252  psrridm  18253  psrridmOLD  18254  psrass1  18255  psrdi  18256  psrdir  18257  psrass23l  18258  psrcom  18259  mplmon2mul  18361  evlslem1  18379  coe1subfv  18502  lply1binomsc  18544  mulgrhm  18710  cygznlem3  18781  evpmodpmf1o  18805  ipdi  18848  ip2di  18849  ipsubdir  18850  ipsubdi  18851  ip2subdi  18852  ipassr  18854  ipassr2  18855  ip2eq  18861  ocvlss  18876  lsmcss  18896  frlmphl  18983  frlmup1  19000  mamuass  19071  mamudi  19072  mamudir  19073  mamuvs1  19074  mamuvs2  19075  dmatmul  19166  dmatsubcl  19167  scmataddcl  19185  smatvscl  19193  scmatghm  19202  mavmulass  19218  mdetrlin  19271  mdetrsca  19272  mdetralt  19277  mdetunilem7  19287  mdetuni0  19290  matinv  19346  pm2mpghm  19484  chpscmatgsummon  19513  chfacfscmulgsum  19528  chfacfpmmulgsum  19532  chfacfpmmulgsum2  19533  cpmadugsumlemB  19542  cpmadugsumlemC  19543  cpmadugsumlemF  19544  iinopn  19578  subbascn  19922  cnhaus  20022  nrmsep2  20024  nrmsep  20025  regsep2  20044  isreg2  20045  hauscmplem  20073  1stcfb  20112  2ndcctbss  20122  ptbasfi  20248  pthaus  20305  txtube  20307  txhaus  20314  xkohaus  20320  kqnrmlem1  20410  kqnrmlem2  20411  nrmr0reg  20416  nrmhmph  20461  fbssint  20505  infil  20530  fgabs  20546  filcon  20550  filuni  20552  trfil2  20554  trfg  20558  ufprim  20576  elfm3  20617  rnelfm  20620  fmfnfmlem2  20622  fmfnfmlem4  20624  hausflimi  20647  hauspwpwf1  20654  fclsneii  20684  supnfcls  20687  flimfnfcls  20695  fclscmpi  20696  alexsublem  20710  ghmcnp  20779  qustgpopn  20784  psmetsym  20980  psmettri  20981  psmetge0  20982  psmetres2  20984  xmetge0  21013  xmetsym  21016  xmettri  21020  xmetres2  21030  prdsxmetlem  21037  prdsmet  21039  imasdsf1olem  21042  imasf1oxmet  21044  bldisj  21067  xblss2ps  21070  xblss2  21071  xmeter  21102  prdsbl  21160  metustexhalfOLD  21232  metustexhalf  21233  metustOLD  21236  metust  21237  nrmmetd  21261  ngpsubcan  21299  nmmtri  21307  nmrtri  21309  ngptgp  21316  nlmvscnlem2  21360  nrginvrcnlem  21365  metdcnlem  21507  clmmulg  21759  cvsmuleqdivd  21777  cvsdiveqd  21778  cphabscl  21798  cphsqrtcl2  21799  cphsqrtcl3  21800  cphnmf  21808  cph2ass  21825  ipcau2  21843  tchcphlem2  21845  ipcnlem2  21850  cfilfcls  21879  iscau3  21883  iscmet3lem2  21897  iscmet3  21898  relcmpcmet  21921  minveclem2  22007  minveclem4  22013  pjthlem1  22018  pjthlem2  22019  uniioombllem4  22161  dyadmax  22173  itg1addlem4  22272  itg1climres  22287  ply1divex  22703  aalioulem2  22895  amgmlem  23517  dvdsppwf1o  23660  perfect1  23701  perfectlem1  23702  perfectlem2  23703  dchrptlem2  23738  colline  24231  ttgcontlem1  24390  axcontlem9  24477  eengtrkg  24490  eengtrkge  24491  4cycl4dv4e  24870  el2spthonot0  25073  usg2spthonot1  25092  clwlknclwlkdifnum  25163  eupa0  25176  eupares  25177  eupap1  25178  frg2woteu  25257  numclwwlk5  25314  numclwwlk6  25315  grpoidinvlem4  25407  grpoasscan2  25438  grpoinvop  25441  grpopncan  25451  grponpcan  25452  grpopnpcan2  25453  grpodiveq  25456  gxcom  25469  gxnn0add  25474  ghgrpOLD  25568  rngo2  25588  rngolz  25601  rngorz  25602  zerdivemp1  25634  vcm  25662  nvmul0or  25745  nvpncan2  25749  nvnncan  25756  nvdif  25766  nvabs  25774  smcnlem  25805  lnomul  25873  minvecolem2  25989  superpos  27471  ssnnssfz  27831  omndmul2  27936  omndmul3  27937  ogrpaddltbi  27943  ogrpaddltrbid  27945  ogrpsublt  27946  ogrpinvlt  27948  isarchi3  27965  archirngz  27967  archiabllem1a  27969  archiabllem1  27971  archiabllem2a  27972  archiabllem2c  27973  slmdvs0  28002  gsumvsca1  28008  gsumvsca2  28009  dvrdir  28015  rdivmuldivd  28016  dvrcan5  28018  ornglmullt  28032  isarchiofld  28042  rhmdvd  28046  rhmunitinv  28047  locfinref  28079  metideq  28107  metider  28108  pstmxmet  28111  lmxrge0  28169  qqhghm  28203  qqhrhm  28204  ispisys2  28383  measdivcst  28433  oddpwdc  28557  ballotlemiex  28704  wrdsplex  28759  cvmopnlem  28987  cvmliftmolem2  28991  cvmliftlem6  28999  cvmliftlem8  29001  cvmliftlem9  29002  cvmlift2lem9  29020  cvmlift3lem2  29029  cvmlift3lem6  29033  cvmlift3lem7  29034  cvmlift3lem9  29036  nodense  29689  cgrtriv  29880  cgrdegen  29882  cgrextend  29886  segconeq  29888  btwntriv2  29890  btwncomand  29893  btwntriv1  29894  btwnintr  29897  btwnexch3  29898  btwnouttr  29902  btwnexch  29903  trisegint  29906  ifscgr  29922  btwnxfr  29934  colineartriv1  29945  colineartriv2  29946  colinearxfr  29953  fscgr  29958  lineid  29961  idinside  29962  endofsegidand  29964  btwnconn1lem5  29969  btwnconn1lem7  29971  btwnconn1lem11  29975  btwnconn1lem12  29976  btwnconn1lem13  29977  brsegle2  29987  segleantisym  29993  broutsideof2  30000  btwnoutside  30003  outsideoftr  30007  outsideofeq  30008  outsideofeu  30009  outsidele  30010  lineunray  30025  lineelsb2  30026  linecom  30028  linethru  30031  heicant  30289  neibastop1  30417  mettrifi  30490  isbnd3  30520  heibor1lem  30545  bfplem2  30559  ghomdiv  30586  zerdivemp1x  30598  irrapxlem5  31001  aomclem2  31240  isnumbasgrplem2  31294  mpaaeu  31340  mendring  31382  mendlmod  31383  caofcan  31469  stoweidlem18  32039  stoweidlem41  32062  stoweidlem45  32066  stoweidlem55  32076  fourierdlem25  32153  fourierdlem31  32159  fourierdlem37  32165  fourierdlem42  32170  etransclem48  32304  rnglz  32944  ssnn0ssfz  33192  zlmodzxzsub  33203  invginvrid  33214  lmodvsmdi  33229  ply1sclrmsm  33237  lincsum  33284  lincscm  33285  lindslinindimp2lem4  33316  lindslinindsimp2lem5  33317  ldepsprlem  33327  lincresunit3lem1  33334  lincresunit3lem2  33335  isldepslvec2  33340  relogbmulbexp  33436  lfladdcl  35193  lflvscl  35199  eqlkr3  35223  lkrlsp  35224  lshpkrlem4  35235  oldmm1  35339  olj01  35347  latmassOLD  35351  latm32  35353  latmrot  35354  latm4  35355  olm01  35358  cmtcomlemN  35370  cmtbr3N  35376  cmtbr4N  35377  lecmtN  35378  omlfh1N  35380  atlen0  35432  atnle  35439  atlatmstc  35441  atlatle  35442  cvlexchb1  35452  cvlcvr1  35461  ishlat3N  35476  hlatjass  35491  hlatj12  35492  hlatj32  35493  hlsupr2  35508  hlhgt2  35510  hl0lt1N  35511  hlrelat  35523  hlrelat2  35524  exatleN  35525  hlrelat3  35533  cvrval5  35536  cvrexchlem  35540  cvratlem  35542  cvrat  35543  atcvr0eq  35547  lnnat  35548  atlt  35558  atlelt  35559  2atlt  35560  atexchltN  35562  cvrat3  35563  2atjm  35566  atbtwn  35567  4noncolr3  35574  athgt  35577  3dimlem3a  35581  3dimlem3OLDN  35583  3dimlem4a  35584  3dimlem4OLDN  35586  3dim1  35588  3dim2  35589  1cvratex  35594  ps-1  35598  ps-2  35599  hlatexch3N  35601  hlatexch4  35602  ps-2b  35603  3atlem1  35604  3atlem2  35605  3atlem5  35608  3atlem6  35609  llnnleat  35634  llncmp  35643  2at0mat0  35646  2atmat0  35647  2atm  35648  lplni2  35658  lvolex3N  35659  lplnnle2at  35662  lplnnleat  35663  lplnnlelln  35664  2atnelpln  35665  llncvrlpln  35679  2atmat  35682  lplncmp  35683  lplnexllnN  35685  2llnjaN  35687  2llnm4  35691  2llnmeqat  35692  lvolnle3at  35703  lvolnleat  35704  2atnelvolN  35708  islvol2aN  35713  4atlem3  35717  4atlem3a  35718  4atlem3b  35719  4atlem4a  35720  4atlem4b  35721  4atlem4c  35722  4atlem4d  35723  4atlem10  35727  4atlem11b  35729  4atlem11  35730  4atlem12b  35732  4atlem12  35733  4at2  35735  lplncvrlvol  35737  lvolcmp  35738  2lplnja  35740  dalemqrprot  35769  dalemply  35775  dalemsly  35776  dalemrot  35778  dalemrotyz  35779  dalem1  35780  dalemcea  35781  dalem3  35785  dalem5  35788  dalem8  35791  dalem-cly  35792  dalem11  35795  dalem12  35796  dalem16  35800  dalem17  35801  dalem18  35802  dalem21  35815  dalem24  35818  dalem25  35819  dalem38  35831  dalem39  35832  dalem44  35837  dalem54  35847  dalem55  35848  dalem57  35850  dalem58  35851  dalem59  35852  dalem60  35853  dath2  35858  2atm2atN  35906  2llnma1b  35907  2llnma3r  35909  cdlema1N  35912  cdlemblem  35914  paddasslem5  35945  paddasslem10  35950  paddasslem12  35952  paddasslem13  35953  paddass  35959  padd12N  35960  padd4N  35961  paddss  35966  pmodlem1  35967  pmodl42N  35972  pmapjoin  35973  pmapjlln1  35976  atmod1i2  35980  llnmod1i2  35981  llnexchb2  35990  dalawlem2  35993  dalawlem3  35994  dalawlem5  35996  dalawlem6  35997  dalawlem7  35998  dalawlem8  35999  dalawlem11  36002  dalawlem12  36003  dalawlem13  36004  pclunN  36019  osumcllem1N  36077  pexmidlem3N  36093  lhp2lt  36122  lhp0lt  36124  lhpexle2lem  36130  lhpexle3lem  36132  lhpocnle  36137  lhpj1  36143  lhpmcvr4N  36147  lhp2at0  36153  lhpat3  36167  4atexlemtlw  36188  4atexlemc  36190  4atexlemnclw  36191  4atexlemcnd  36193  lautcvr  36213  lautj  36214  lautm  36215  ltrnm  36252  ltrnj  36253  ltrncvr  36254  trlval3  36309  cdlemc5  36317  cdlemd2  36321  cdlemd3  36322  cdleme0e  36339  cdleme1  36349  cdleme3c  36352  cdleme3g  36356  cdleme3h  36357  cdleme3  36359  cdleme5  36362  cdleme7c  36367  cdleme7d  36368  cdleme7e  36369  cdleme7ga  36370  cdleme7  36371  cdleme9  36375  cdleme11c  36383  cdleme11g  36387  cdleme11k  36390  cdleme11  36392  cdleme12  36393  cdleme15b  36397  cdleme15d  36399  cdleme16d  36403  cdleme16e  36404  cdleme16f  36405  cdleme17b  36409  cdleme18b  36414  cdleme22gb  36416  cdlemednpq  36421  cdleme19a  36426  cdleme20aN  36432  cdleme20bN  36433  cdleme20c  36434  cdleme20d  36435  cdleme20j  36441  cdleme21c  36450  cdleme22aa  36462  cdleme22b  36464  cdleme22cN  36465  cdleme22d  36466  cdleme22e  36467  cdleme22eALTN  36468  cdleme23b  36473  cdleme23c  36474  cdleme28a  36493  cdleme30a  36501  cdlemefs29bpre0N  36539  cdlemefs29bpre1N  36540  cdlemefs29cpre1N  36541  cdlemefs29clN  36542  cdlemefs32fvaN  36545  cdlemefs32fva1  36546  cdleme32b  36565  cdleme32c  36566  cdleme32e  36568  cdleme35a  36571  cdleme35fnpq  36572  cdleme35b  36573  cdleme35f  36577  cdleme36a  36583  cdleme36m  36584  cdleme37m  36585  cdleme39a  36588  cdleme42c  36595  cdleme42i  36606  cdleme42keg  36609  cdleme42mgN  36611  cdleme48bw  36625  cdlemeg46fjgN  36644  cdlemeg46fjv  36646  cdlemeg46req  36652  cdleme50trn1  36672  cdlemf1  36684  cdlemf2  36685  cdlemg1cex  36711  cdlemg2fv2  36723  cdlemg7fvbwN  36730  cdlemg4c  36735  cdlemg4  36740  cdlemg6c  36743  cdlemg8b  36751  cdlemg10c  36762  cdlemg10  36764  cdlemg11b  36765  cdlemg12f  36771  cdlemg13a  36774  cdlemg17a  36784  cdlemg17dALTN  36787  cdlemg18b  36802  cdlemg19a  36806  cdlemg27a  36815  cdlemg27b  36819  cdlemg33b0  36824  cdlemg33a  36829  cdlemg35  36836  trlcolem  36849  cdlemg42  36852  cdlemg46  36858  trljco  36863  tendopltp  36903  cdlemh1  36938  cdlemh2  36939  cdlemi1  36941  cdlemi  36943  cdlemk3  36956  cdlemk10  36966  cdlemk11  36972  cdlemk15  36978  cdlemk1u  36982  cdlemk5u  36984  cdlemk11u  36994  cdlemk39  37039  cdlemkid1  37045  cdlemk50  37075  cdlemk51  37076  erngdvlem3-rN  37121  tendocnv  37145  tendospcanN  37147  dialss  37170  dia2dimlem1  37188  dia2dimlem2  37189  dia2dimlem3  37190  dia2dimlem10  37197  dia2dimlem12  37199  dvhvaddass  37221  dvhlveclem  37232  cdlemm10N  37242  doca2N  37250  djajN  37261  dib1dim2  37292  diblss  37294  diclspsn  37318  cdlemn2  37319  cdlemn10  37330  dihjustlem  37340  dihord1  37342  dihord2a  37343  dihord2pre2  37350  dib2dim  37367  dih2dimb  37368  dih2dimbALTN  37369  dihopelvalcpre  37372  dihord5b  37383  dihord6b  37384  dihord5apre  37386  dihmeetlem1N  37414  dihglblem5apreN  37415  dihglblem2N  37418  dihglbcpreN  37424  dihmeetbclemN  37428  dihmeetlem3N  37429  dihmeetlem6  37433  dih1dimatlem  37453  djhcvat42  37539  dihjatcclem1  37542  dihjatcclem4  37545  dvh4dimat  37562  lcfl7lem  37623  lclkrlem2m  37643  lcfrlem1  37666  lcdvsass  37731  baerlem3lem1  37831  baerlem5alem1  37832  baerlem5blem1  37833  mapdh6gN  37866  mapdh6hN  37867  hdmap1l6g  37941  hdmap1l6h  37942  hdmapneg  37973  hdmap14lem8  38002  hgmapadd  38021  hgmapmul  38022  hgmapvvlem1  38050  relexpnul  38199
  Copyright terms: Public domain W3C validator