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

Theorem syl13anc 1266
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 1185 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl13anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )
)  ->  et )
71, 5, 6syl2anc 665 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  syl23anc  1271  syl33anc  1279  disjxiun  4356  wereu2  4786  ordelord  5400  caovassd  6419  caovcand  6422  caovordid  6426  caovordd  6428  caovdid  6435  caovdird  6438  swoer  7339  swoord1  7340  swoord2  7341  frfi  7762  indexfi  7828  ssfii  7879  elfiun  7890  suplub2  7921  supgtoreq  7932  infltoreq  7964  wemaplem2  8008  htalem  8312  cofsmo  8643  alephsing  8650  sornom  8651  axdc3lem4  8827  zorn2lem1  8870  ttukeylem6  8888  ttukeylem7  8889  prlem934  9402  supfirege  10542  suprfinzcl  10994  fzosubel3  11918  fsuppmapnn0fiublem  12145  seqsplit  12189  seqcaopr  12193  ccatass  12673  wrdcctswrd  12760  wrdeqcats1OLD  12769  wrdeqs1cat  12770  splid  12799  spllen  12800  splfv1  12801  splfv2a  12802  splval2  12803  swrds2  12957  isercolllem2  13665  fsumiun  13817  zprod  13927  lcmftp  14545  pcgcd1  14762  cshwsidrepswmod0  15001  cshwshashlem2  15003  cshwsdisj  15005  firest  15267  iscatd2  15523  posasymb  16134  joinle  16196  meetle  16210  lattrd  16240  latleeqj1  16245  latjlej1  16247  latjlej12  16249  latnlej2  16253  latjidm  16256  latleeqm1  16261  latmlem1  16263  latmlem12  16265  latmidm  16268  latledi  16271  latjass  16277  latj12  16278  latj13  16280  latj31  16281  latjrot  16282  latj4  16283  mod1ile  16287  lubun  16305  clatleglb  16308  latdisdlem  16371  mnd32g  16487  mnd12g  16488  mnd4g  16489  ismndd  16495  prdsmndd  16505  imasmnd  16510  mrcmndind  16549  gsumspl  16564  grpidrcan  16655  grpidlcan  16656  grpinvinv  16657  grplmulf1o  16664  grpinvssd  16667  grpinvadd  16668  grpsubrcan  16671  grpsubadd  16678  grpaddsubass  16680  grppncan  16681  grpsubsub4  16683  grppnpcan2  16684  grpnpncan  16685  grpnpncan0  16686  grpnnncan2  16687  grplactcnv  16690  mulgnn0dir  16717  mulgdirlem  16718  mulgneg2  16721  mulgnnass  16722  mulgnn0ass  16723  mulgass  16724  imasgrp  16738  mhmmnd  16744  nsgconj  16786  isnsg3  16787  nmzsubg  16794  ssnmz  16795  eqger  16803  eqgcpbl  16807  conjghm  16849  conjnmz  16852  conjnmzb  16853  subgga  16890  gass  16891  gasubg  16892  galcan  16894  gacan  16895  gapm  16896  gaorber  16898  gastacl  16899  gastacos  16900  cntzsubm  16925  cntzsubg  16926  oppgmnd  16941  symggen  17047  odmodnn0  17125  mndodconglem  17126  odmod  17131  odcong  17134  odmulgid  17141  odbezout  17145  gexdvdsi  17170  gexdvds  17171  sylow1lem2  17187  sylow1lem4  17189  sylow2blem1  17208  sylow2blem2  17209  sylow2blem3  17210  sylow3lem1  17215  sylow3lem2  17216  lsmass  17256  lsmmod  17261  lsmdisj2  17268  subgdisj1  17277  efgredleme  17329  efgredlemc  17331  efgcpbllemb  17341  frgp0  17346  frgpuplem  17358  abl32  17387  abladdsub4  17392  abladdsub  17393  ablpncan2  17394  ablsubsub  17396  mulgdi  17403  mulgsubdi  17406  odadd1  17422  odadd2  17423  gex2abl  17425  oddvdssubg  17429  cygabl  17461  telgsumfzslem  17554  ablfacrp  17635  pgpfac1lem2  17644  pgpfac1lem3a  17645  pgpfac1lem3  17646  pgpfac1lem4  17647  srgmulgass  17700  srgpcomp  17701  srgpcompp  17702  srgpcomppsc  17703  srgbinomlem3  17711  srgbinomlem4  17712  srgbinomlem  17713  csrgbinom  17715  ringcom  17745  ringlz  17753  ringrz  17754  ringnegl  17758  rngnegr  17759  ringmneg1  17760  ringmneg2  17761  ringsubdi  17763  rngsubdir  17764  mulgass2  17765  prdsringd  17776  imasring  17783  opprring  17795  mulgass3  17801  dvdsrtr  17816  dvdsrmul1  17817  unitgrp  17831  dvrass  17854  dvrcan1  17855  dvrcan3  17856  irredrmul  17871  drngmul0or  17932  subrginv  17960  cntzsubr  17976  lmod0vs  18060  lmodvs0  18061  lmodvsmmulgdi  18062  lmodvneg1  18067  lmodvsneg  18068  lmodcom  18070  lmodsubvs  18080  lmodsubdi  18081  lmodsubdir  18082  lssvsubcl  18103  lssvacl  18113  lssvscl  18114  islss3  18118  lss1d  18122  lssintcl  18123  prdslmodd  18128  lmodvsinv  18195  lmodvsinv2  18196  lmhmplusg  18203  lmhmvsca  18204  lsmcl  18242  pj1lmhm  18259  lvecvs0or  18267  lssvs0or  18269  lvecinv  18272  lspsnvs  18273  lspfixed  18287  lspexch  18288  lspsolvlem  18301  lspsolv  18302  lssacsex  18303  lspsnat  18304  lsppratlem1  18306  lsppratlem3  18308  lsppratlem4  18309  lbsextlem2  18318  lbsextlem4  18320  sralmod  18346  2idlcpbl  18394  unitrrg  18453  assa2ass  18482  issubassa  18484  sraassa  18485  asclghm  18498  asclmul1  18499  asclmul2  18500  asclrhm  18502  assamulgscmlem2  18509  psrbagcon  18531  psrbagconcl  18533  psrbagconf1o  18534  gsumbagdiaglem  18535  psrmulcllem  18547  psrlidm  18563  psrridm  18564  psrass1  18565  psrdi  18566  psrdir  18567  psrass23l  18568  psrcom  18569  mplmon2mul  18660  evlslem1  18674  coe1subfv  18795  lply1binomsc  18837  mulgrhm  19004  cygznlem3  19075  evpmodpmf1o  19099  ipdi  19142  ip2di  19143  ipsubdir  19144  ipsubdi  19145  ip2subdi  19146  ipassr  19148  ipassr2  19149  ip2eq  19155  ocvlss  19170  lsmcss  19190  frlmphl  19274  frlmup1  19291  mamuass  19362  mamudi  19363  mamudir  19364  mamuvs1  19365  mamuvs2  19366  dmatmul  19457  dmatsubcl  19458  scmataddcl  19476  smatvscl  19484  scmatghm  19493  mavmulass  19509  mdetrlin  19562  mdetrsca  19563  mdetralt  19568  mdetunilem7  19578  mdetuni0  19581  matinv  19637  pm2mpghm  19775  chpscmatgsummon  19804  chfacfscmulgsum  19819  chfacfpmmulgsum  19823  chfacfpmmulgsum2  19824  cpmadugsumlemB  19833  cpmadugsumlemC  19834  cpmadugsumlemF  19835  iinopn  19867  subbascn  20205  cnhaus  20305  nrmsep2  20307  nrmsep  20308  regsep2  20327  isreg2  20328  hauscmplem  20356  1stcfb  20395  2ndcctbss  20405  ptbasfi  20531  pthaus  20588  txtube  20590  txhaus  20597  xkohaus  20603  kqnrmlem1  20693  kqnrmlem2  20694  nrmr0reg  20699  nrmhmph  20744  fbssint  20788  infil  20813  fgabs  20829  filcon  20833  filuni  20835  trfil2  20837  trfg  20841  ufprim  20859  elfm3  20900  rnelfm  20903  fmfnfmlem2  20905  fmfnfmlem4  20907  hausflimi  20930  hauspwpwf1  20937  fclsneii  20967  supnfcls  20970  flimfnfcls  20978  fclscmpi  20979  alexsublem  20994  ghmcnp  21064  qustgpopn  21069  psmetsym  21261  psmettri  21262  psmetge0  21263  psmetres2  21265  xmetge0  21294  xmetsym  21297  xmettri  21301  xmetres2  21311  prdsxmetlem  21318  prdsmet  21320  imasdsf1olem  21323  imasf1oxmet  21325  bldisj  21348  xblss2ps  21351  xblss2  21352  xmeter  21383  prdsbl  21441  metustexhalf  21506  metust  21508  nrmmetd  21524  ngpsubcan  21562  nmmtri  21570  nmrtri  21572  ngptgp  21579  nlmvscnlem2  21623  nrginvrcnlem  21628  metdcnlem  21789  clmmulg  22059  cvsmuleqdivd  22077  cvsdiveqd  22078  cphabscl  22098  cphsqrtcl2  22099  cphsqrtcl3  22100  cphnmf  22108  cph2ass  22125  ipcau2  22143  tchcphlem2  22145  ipcnlem2  22150  cfilfcls  22179  iscau3  22183  iscmet3lem2  22197  iscmet3  22198  relcmpcmet  22221  minveclem2  22303  minveclem4  22309  minveclem2OLD  22315  minveclem4OLD  22321  pjthlem1  22326  pjthlem2  22327  uniioombllem4  22479  dyadmax  22491  itg1addlem4  22592  itg1climres  22607  ply1divex  23022  aalioulem2  23224  amgmlem  23850  dvdsppwf1o  24050  perfect1  24091  perfectlem1  24092  perfectlem2  24093  dchrptlem2  24128  colline  24629  ttgcontlem1  24850  axcontlem9  24937  eengtrkg  24950  eengtrkge  24951  4cycl4dv4e  25331  el2spthonot0  25534  usg2spthonot1  25553  clwlknclwlkdifnum  25624  eupa0  25637  eupares  25638  eupap1  25639  frg2woteu  25718  numclwwlk5  25775  numclwwlk6  25776  grpoidinvlem4  25870  grpoasscan2  25901  grpoinvop  25904  grpopncan  25914  grponpcan  25915  grpopnpcan2  25916  grpodiveq  25919  gxcom  25932  gxnn0add  25937  ghgrpOLD  26031  rngo2  26051  rngolz  26064  rngorz  26065  zerdivemp1  26097  vcm  26125  nvmul0or  26208  nvpncan2  26212  nvnncan  26219  nvdif  26229  nvabs  26237  smcnlem  26268  lnomul  26336  minvecolem2  26452  minvecolem2OLD  26462  superpos  27942  ssnnssfz  28310  omndmul2  28419  omndmul3  28420  ogrpaddltbi  28426  ogrpaddltrbid  28428  ogrpsublt  28429  ogrpinvlt  28431  isarchi3  28448  archirngz  28450  archiabllem1a  28452  archiabllem1  28454  archiabllem2a  28455  archiabllem2c  28456  slmdvs0  28485  gsumvsca1  28490  gsumvsca2  28491  dvrdir  28498  rdivmuldivd  28499  dvrcan5  28501  ornglmullt  28515  isarchiofld  28525  rhmdvd  28529  rhmunitinv  28530  psgnfzto1stlem  28558  mdetpmtr1  28594  mdetpmtr12  28596  mdetlap  28603  locfinref  28613  metideq  28641  metider  28642  pstmxmet  28645  lmxrge0  28703  qqhghm  28737  qqhrhm  28738  ispisys2  28920  rossros  28947  measdivcst  28992  oddpwdc  29132  ballotlemiex  29279  ballotlemiexOLD  29317  wrdsplex  29372  cvmopnlem  29946  cvmliftmolem2  29950  cvmliftlem6  29958  cvmliftlem8  29960  cvmliftlem9  29961  cvmlift2lem9  29979  cvmlift3lem2  29988  cvmlift3lem6  29992  cvmlift3lem7  29993  cvmlift3lem9  29995  nodense  30520  cgrtriv  30711  cgrdegen  30713  cgrextend  30717  segconeq  30719  btwntriv2  30721  btwncomand  30724  btwntriv1  30725  btwnintr  30728  btwnexch3  30729  btwnouttr  30733  btwnexch  30734  trisegint  30737  ifscgr  30753  btwnxfr  30765  colineartriv1  30776  colineartriv2  30777  colinearxfr  30784  fscgr  30789  lineid  30792  idinside  30793  endofsegidand  30795  btwnconn1lem5  30800  btwnconn1lem7  30802  btwnconn1lem11  30806  btwnconn1lem12  30807  btwnconn1lem13  30808  brsegle2  30818  segleantisym  30824  broutsideof2  30831  btwnoutside  30834  outsideoftr  30838  outsideofeq  30839  outsideofeu  30840  outsidele  30841  lineunray  30856  lineelsb2  30857  linecom  30859  linethru  30862  neibastop1  30957  poimirlem28  31869  poimirlem32  31873  heicant  31876  mettrifi  31987  isbnd3  32017  heibor1lem  32042  bfplem2  32056  ghomdiv  32083  zerdivemp1x  32095  lfladdcl  32543  lflvscl  32549  eqlkr3  32573  lkrlsp  32574  lshpkrlem4  32585  oldmm1  32689  olj01  32697  latmassOLD  32701  latm32  32703  latmrot  32704  latm4  32705  olm01  32708  cmtcomlemN  32720  cmtbr3N  32726  cmtbr4N  32727  lecmtN  32728  omlfh1N  32730  atlen0  32782  atnle  32789  atlatmstc  32791  atlatle  32792  cvlexchb1  32802  cvlcvr1  32811  ishlat3N  32826  hlatjass  32841  hlatj12  32842  hlatj32  32843  hlsupr2  32858  hlhgt2  32860  hl0lt1N  32861  hlrelat  32873  hlrelat2  32874  exatleN  32875  hlrelat3  32883  cvrval5  32886  cvrexchlem  32890  cvratlem  32892  cvrat  32893  atcvr0eq  32897  lnnat  32898  atlt  32908  atlelt  32909  2atlt  32910  atexchltN  32912  cvrat3  32913  2atjm  32916  atbtwn  32917  4noncolr3  32924  athgt  32927  3dimlem3a  32931  3dimlem3OLDN  32933  3dimlem4a  32934  3dimlem4OLDN  32936  3dim1  32938  3dim2  32939  1cvratex  32944  ps-1  32948  ps-2  32949  hlatexch3N  32951  hlatexch4  32952  ps-2b  32953  3atlem1  32954  3atlem2  32955  3atlem5  32958  3atlem6  32959  llnnleat  32984  llncmp  32993  2at0mat0  32996  2atmat0  32997  2atm  32998  lplni2  33008  lvolex3N  33009  lplnnle2at  33012  lplnnleat  33013  lplnnlelln  33014  2atnelpln  33015  llncvrlpln  33029  2atmat  33032  lplncmp  33033  lplnexllnN  33035  2llnjaN  33037  2llnm4  33041  2llnmeqat  33042  lvolnle3at  33053  lvolnleat  33054  2atnelvolN  33058  islvol2aN  33063  4atlem3  33067  4atlem3a  33068  4atlem3b  33069  4atlem4a  33070  4atlem4b  33071  4atlem4c  33072  4atlem4d  33073  4atlem10  33077  4atlem11b  33079  4atlem11  33080  4atlem12b  33082  4atlem12  33083  4at2  33085  lplncvrlvol  33087  lvolcmp  33088  2lplnja  33090  dalemqrprot  33119  dalemply  33125  dalemsly  33126  dalemrot  33128  dalemrotyz  33129  dalem1  33130  dalemcea  33131  dalem3  33135  dalem5  33138  dalem8  33141  dalem-cly  33142  dalem11  33145  dalem12  33146  dalem16  33150  dalem17  33151  dalem18  33152  dalem21  33165  dalem24  33168  dalem25  33169  dalem38  33181  dalem39  33182  dalem44  33187  dalem54  33197  dalem55  33198  dalem57  33200  dalem58  33201  dalem59  33202  dalem60  33203  dath2  33208  2atm2atN  33256  2llnma1b  33257  2llnma3r  33259  cdlema1N  33262  cdlemblem  33264  paddasslem5  33295  paddasslem10  33300  paddasslem12  33302  paddasslem13  33303  paddass  33309  padd12N  33310  padd4N  33311  paddss  33316  pmodlem1  33317  pmodl42N  33322  pmapjoin  33323  pmapjlln1  33326  atmod1i2  33330  llnmod1i2  33331  llnexchb2  33340  dalawlem2  33343  dalawlem3  33344  dalawlem5  33346  dalawlem6  33347  dalawlem7  33348  dalawlem8  33349  dalawlem11  33352  dalawlem12  33353  dalawlem13  33354  pclunN  33369  osumcllem1N  33427  pexmidlem3N  33443  lhp2lt  33472  lhp0lt  33474  lhpexle2lem  33480  lhpexle3lem  33482  lhpocnle  33487  lhpj1  33493  lhpmcvr4N  33497  lhp2at0  33503  lhpat3  33517  4atexlemtlw  33538  4atexlemc  33540  4atexlemnclw  33541  4atexlemcnd  33543  lautcvr  33563  lautj  33564  lautm  33565  ltrnm  33602  ltrnj  33603  ltrncvr  33604  trlval3  33659  cdlemc5  33667  cdlemd2  33671  cdlemd3  33672  cdleme0e  33689  cdleme1  33699  cdleme3c  33702  cdleme3g  33706  cdleme3h  33707  cdleme3  33709  cdleme5  33712  cdleme7c  33717  cdleme7d  33718  cdleme7e  33719  cdleme7ga  33720  cdleme7  33721  cdleme9  33725  cdleme11c  33733  cdleme11g  33737  cdleme11k  33740  cdleme11  33742  cdleme12  33743  cdleme15b  33747  cdleme15d  33749  cdleme16d  33753  cdleme16e  33754  cdleme16f  33755  cdleme17b  33759  cdleme18b  33764  cdleme22gb  33766  cdlemednpq  33771  cdleme19a  33776  cdleme20aN  33782  cdleme20bN  33783  cdleme20c  33784  cdleme20d  33785  cdleme20j  33791  cdleme21c  33800  cdleme22aa  33812  cdleme22b  33814  cdleme22cN  33815  cdleme22d  33816  cdleme22e  33817  cdleme22eALTN  33818  cdleme23b  33823  cdleme23c  33824  cdleme28a  33843  cdleme30a  33851  cdlemefs29bpre0N  33889  cdlemefs29bpre1N  33890  cdlemefs29cpre1N  33891  cdlemefs29clN  33892  cdlemefs32fvaN  33895  cdlemefs32fva1  33896  cdleme32b  33915  cdleme32c  33916  cdleme32e  33918  cdleme35a  33921  cdleme35fnpq  33922  cdleme35b  33923  cdleme35f  33927  cdleme36a  33933  cdleme36m  33934  cdleme37m  33935  cdleme39a  33938  cdleme42c  33945  cdleme42i  33956  cdleme42keg  33959  cdleme42mgN  33961  cdleme48bw  33975  cdlemeg46fjgN  33994  cdlemeg46fjv  33996  cdlemeg46req  34002  cdleme50trn1  34022  cdlemf1  34034  cdlemf2  34035  cdlemg1cex  34061  cdlemg2fv2  34073  cdlemg7fvbwN  34080  cdlemg4c  34085  cdlemg4  34090  cdlemg6c  34093  cdlemg8b  34101  cdlemg10c  34112  cdlemg10  34114  cdlemg11b  34115  cdlemg12f  34121  cdlemg13a  34124  cdlemg17a  34134  cdlemg17dALTN  34137  cdlemg18b  34152  cdlemg19a  34156  cdlemg27a  34165  cdlemg27b  34169  cdlemg33b0  34174  cdlemg33a  34179  cdlemg35  34186  trlcolem  34199  cdlemg42  34202  cdlemg46  34208  trljco  34213  tendopltp  34253  cdlemh1  34288  cdlemh2  34289  cdlemi1  34291  cdlemi  34293  cdlemk3  34306  cdlemk10  34316  cdlemk11  34322  cdlemk15  34328  cdlemk1u  34332  cdlemk5u  34334  cdlemk11u  34344  cdlemk39  34389  cdlemkid1  34395  cdlemk50  34425  cdlemk51  34426  erngdvlem3-rN  34471  tendocnv  34495  tendospcanN  34497  dialss  34520  dia2dimlem1  34538  dia2dimlem2  34539  dia2dimlem3  34540  dia2dimlem10  34547  dia2dimlem12  34549  dvhvaddass  34571  dvhlveclem  34582  cdlemm10N  34592  doca2N  34600  djajN  34611  dib1dim2  34642  diblss  34644  diclspsn  34668  cdlemn2  34669  cdlemn10  34680  dihjustlem  34690  dihord1  34692  dihord2a  34693  dihord2pre2  34700  dib2dim  34717  dih2dimb  34718  dih2dimbALTN  34719  dihopelvalcpre  34722  dihord5b  34733  dihord6b  34734  dihord5apre  34736  dihmeetlem1N  34764  dihglblem5apreN  34765  dihglblem2N  34768  dihglbcpreN  34774  dihmeetbclemN  34778  dihmeetlem3N  34779  dihmeetlem6  34783  dih1dimatlem  34803  djhcvat42  34889  dihjatcclem1  34892  dihjatcclem4  34895  dvh4dimat  34912  lcfl7lem  34973  lclkrlem2m  34993  lcfrlem1  35016  lcdvsass  35081  baerlem3lem1  35181  baerlem5alem1  35182  baerlem5blem1  35183  mapdh6gN  35216  mapdh6hN  35217  hdmap1l6g  35291  hdmap1l6h  35292  hdmapneg  35323  hdmap14lem8  35352  hgmapadd  35371  hgmapmul  35372  hgmapvvlem1  35400  irrapxlem5  35577  aomclem2  35820  isnumbasgrplem2  35870  mpaaeu  35923  mendring  35965  mendlmod  35966  relexpnul  36177  caofcan  36579  disjiun2  37308  wessf1ornlem  37357  stoweidlem18  37755  stoweidlem41  37779  stoweidlem45  37783  stoweidlem55  37793  fourierdlem25  37871  fourierdlem31  37877  fourierdlem31OLD  37878  fourierdlem37  37884  fourierdlem42  37889  fourierdlem42OLD  37890  etransclem48OLD  38024  etransclem48  38025  sge0iunmptlemfi  38100  hoicvr  38211  hoidmvlelem2  38259  perfectALTVlem1  38650  perfectALTVlem2  38651  rnglz  39469  ssnn0ssfz  39717  zlmodzxzsub  39728  invginvrid  39739  lmodvsmdi  39754  ply1sclrmsm  39762  lincsum  39809  lincscm  39810  lindslinindimp2lem4  39841  lindslinindsimp2lem5  39842  ldepsprlem  39852  lincresunit3lem1  39859  lincresunit3lem2  39860  isldepslvec2  39865  relogbmulbexp  39959
  Copyright terms: Public domain W3C validator